&gt; Is there a good language with the simplicity, portability, and control of C together with theorem-proving features?<p>Yes: C ;-) The Frama-C system allows you to write functional specifications of C code and verify them. Trivial example: <a href="http:&#x2F;&#x2F;frama-c.com&#x2F;wp.html" rel="nofollow">http:&#x2F;&#x2F;frama-c.com&#x2F;wp.html</a><p>It interfaces with the Why3 platform, which means that it can talk to dozens of automated provers out of the box. AFAIK it doesn&#x27;t yet handle some things like dynamic allocation and free (the semantics of free in C is hard!), but it may be something you might want to play with.