Published results from the prototype NFV reviewer for Z3, LiteBox and NVX.
Conditional MODEL refutations are not confirmed source bugs.
Verification concerns translated models under their stated assumptions; failure to refute is not evidence of correctness.