Alternatives and related programs
- Ada SPARK Pro
is a formally verified subset of the Ada programming language
(tagline: "You simply can't write better code").
- KLEE has similarities
but is not a formal proof system.
- CompCert
is INRIA's verified C compiler (not open source).