Wouldn't it require a set of business rules instead of a comprehensive design model? It's logic programming. Based on those rules it can determine whether the input I passed in should produce the output I received.
The logic programming suggestion would be much less work but is usually overlooked. Probably because that kind of subtle, concise code is the polar opposite of brute force fuzzing.
> Wouldn't it require a set of business rules instead of a comprehensive design model?
Well, I was imagining something like a library being tested/verified rather than an application or system. But either way, you have to model the features of the code-being-verified and the model must be comprehensive. An incomplete reference model usually will result in false defects.
This (usually) requires a comprehensive reference model of your design whereas asserts can be added very adhoc and phased in as appropriate.
Also, fuzzing doesn't require assertions, it just yields more/better fruit that way.