> 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.
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.