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").
- TLA+
is useful for proving distributed systems over time.
- Why3 / WhyML
can be used for constructive proofs.
- CompCert
is INRIA's verified C compiler (not open source).
- RefinedC