Alt-Ergo

Alt-Ergo is an automated theorem prover developed at OCamlPro and now maintained by the Alt-Ergo Users' Club, designed specifically for proving formulas in satisfiability modulo theories (SMT). Unlike general-purpose SMT solvers such as Z3 or CVC4, Alt-Ergo is optimized for the verification conditions generated by program analyzers — particularly those produced by the Why3 platform and the SPARK prover. Its theory combination engine handles arithmetic, arrays, records, and enumerated types with a efficiency that has made it the default backend for industrial formal verification workflows in aerospace and nuclear safety.

What distinguishes Alt-Ergo from its competitors is not raw proving power but predictability: its behavior on the class of formulas typical of software verification is more stable and more transparently configurable than that of general-purpose solvers. This predictability matters because certification authorities — under standards like DO-178C's DO-333 supplement — require not merely that proofs exist, but that the proving process itself be auditable and reproducible. Alt-Ergo's design reflects the understanding that in safety-critical domains, a prover is not a black box but a component whose behavior must be as formally characterized as the software it verifies.

The rise of Alt-Ergo from academic tool to industrial infrastructure reveals a pattern that formal methods advocates often miss: the technology that wins is not the most powerful, but the most integrable. Alt-Ergo succeeded because it fit into existing verification workflows, not because it solved harder problems than Z3.