The age old problem of verification vs. validation. Verification is about whether or not you built something right. Validation is about whether or not you built the right thing. This article is about using Z3 to pursue the former, the latter is an entirely different issue.

This is, basically, an unsolvable philosophical problem. You are the only one who can bridge the infinite lacuna between the idea in your head and its properties encoded in an actual model. There are all sorts of validity tests you can add to ensure it matches your vision, of course, but any attempt at solving this problem would just look like an even higher-level language.

This is called validation, and it's much harder epistemically than verification.

Is it possible to check at runtime that the model is accurate?

Do you have a sensible thing to do if the model isn't accurate (e.g., fallback into "failsafe" mode, let an on-call engineer know that an assumption was violated, etc.)?

If yes & yes, well, there's your answer :)

Do the opposite: generate the program from the model

Which, in turn, requires trusting or proving the soundness of your program generator and only proves that your incorrect original program is exactly as incorrect as the model that verifies it.

Automating the stronger proof (that the model is exactly as correct as the original program, and that the model is correct) hasn't been solved in the general case, to the best of my knowledge.

That's not a dumb question! The accuracy of one's underlying models is an outstanding problem in verification.

Let me ask another question,

how do we evaluate the accuracy of a model?

Thank you for your time.

Evaluating the accuracy of a model is an unsolved problem with both formal and informal approaches.

Formally: we could ask multiple separate model/proof assistants to generate separate models from the same underlying specification, and then attempt to find discrepancies between their predicted results. This really just punts the responsibility: now we're relying on the accuracy of the abstract specification, rather than the model(s) automatically or manually produced from it. It's also not sound; it just allows us to feel more confident.

Informally: we can have a lot of different people look at the model very closely, and produce test vectors for the model based on human predictions of behavior.

Thank you. Is there any way to statistically evaluate a model? Something like testing a model.

You could generate a set of random vectors that span the entire input space, exercise the system with those vectors, and publish some sort of "accuracy" (e.g. generate random vectors through i.i.d. uniform R.V.s over the input space, evaluate f(input), and use the successes in a hierarchical binomial distribution). Remember that most of the time we try to verify programs by building a model to model _edge cases_; after all the "happy path" of the program is simple to test. Edge cases are, by their nature, rare occurrences. As a trivial example, think of a boolean function f(x, y) = x & y. f evaluates to 0 for every value of (x, y) except (1, 1). If we were to create a model of this function, f_model = 0, f_model would appear to evaluate similarly to f 75% of the time. With a sufficiently large input state space, it would be quite feasible to hide essential edge cases in very small tail probabilities (e.g. < 99.5%).