Earlier quoted context omitted.
Model checking is a pretty cool idea, except you really need to have it built into the language rather than as an annotation or seperate system. Maintaining a seperate model just gives you two places to make typos.
Conversely, it gives two opportunities to avoid not only typos, but "thinkos". Simple declarative definitions can often define the results of complicated algorithms. Algebraic topology is actually a nice example. Presumably a surface has no holes if and only if any loop on the surface can be contracted to a point (given appropriate definitions of all these terms, of course). While this equivalence is easy to verify,…
It's actually quite simple: A surface has no holes if its Euler Characteristic is 2. Since 3D objects are already expressed in a triangulated form, this is quite easy to check.