is a formally verified subset of the Ada programming language
(tagline: <i>"You simply can't write better code"</i>).
-<li> <a href="http://klee.github.io/">KLEE</a> has similarities
- but is not a formal proof system.
+<li> <a href="https://lamport.azurewebsites.net/tla/tla.html">TLA+</a>
+ is useful for proving distributed systems over time.
+
+<li> <a href="http://why3.lri.fr">Why3 / WhyML</a>
+ can be used for constructive proofs.
<li> <a href="http://compcert.inria.fr/">CompCert</a>
is INRIA's verified C compiler (not open source).