Alt-Ergo

Alt-Ergo is an automatic solver of mathematical formulas based on Satisfiability Modulo Theories (SMT), designed for program verification. It is used as a back-end prover by verification tools such as Why3, Frama-C, the SPARK toolset, Caveat, EasyCrypt and Cubicle, and to prove formulas from B models (Atelier B). Its built-in theories include equality with uninterpreted symbols, linear arithmetic, arrays, enumerated and record datatypes and fixed-size bit-vectors.

Alt-Ergo originates from research at LRI, Inria and CNRS started in 2006 and has been maintained by OCamlPro since 2013. It is installed through OPAM or from binaries on GitHub, is used from the command line, and a JavaScript version (Try-Alt-Ergo) runs in a web browser. The latest version is released under the OCamlPro Non-Commercial License, while an older version (Alt-Ergo-Free) is available under the Apache License 2.0. Version 2.6.3 was released in April 2026.