The first version of Alt-Ergo was released in 2006. Its architecture was shaped by deductive program verification tools, and it uses a native input language for polymorphic first-order logic that is not compliant with SMT-LIB. OCamlPro announced its support and distribution of the solver in September 2013.
Notable releases include:
2.1.0 (2018): a conflict-driven clause learning (CDCL) SAT solver became the default Boolean reasoner, replacing the earlier tableaux-like approach.
2.2.0 (2018): a new experimental front-end supporting SMT-LIB 2 with a conservative extension for prenex polymorphism.
2.4.0 (2021): support for the incremental commands push and pop from the SMT-LIB standard, and the .ae file extension for the native syntax.
2.5.0 (2022–2023): generation of counterexample models, on a best-effort basis and initially limited to linear arithmetic and enumerated types.
2.6.0 (September 2024): a new relational theory for bit vectors, improvements to the floating-point theory, and the Dolmen library as the default front-end. The release followed an acceleration of development under the DéCySif research project, a collaboration of AdaCore, Inria, OCamlPro and TrustInSoft.
As of October 2026 the project website lists version 2.6.3 (14 April 2026) as the latest release.
Technologies
Design choices
Alt-Ergo employs a specialized input language with prenex polymorphism, designed to reduce the number of axioms requiring quantification and to simplify the complexity of problems. While Alt-Ergo offers partial support for the SMT-LIB 2 language, its efficiency with SMT files is comparatively limited.
Main components
The core architecture of Alt-Ergo comprises three main elements: a depth-first search (DFS)-based SAT solver, a quantifier's instantiation engine that uses e-matching, and an assembly of decision procedures for a range of built-in theories. These components collectively enable Alt-Ergo's abilities in automatic formula solving.
Alt-Ergo's native language is a polymorphic first-order logic in the style of ML, and the solver also accepts SMT-LIB v2 input. Since version 2.1.0 its Boolean reasoning has been performed by a CDCL-based SAT solver by default.
Built-in theories
Alt-Ergo implements (semi-)decision procedures for the following theories:
Alt-Ergo's current releases are distributed under the OCamlPro Non-Commercial License, intended for research and evaluation. Releases are made available under an open-source license after a delay of a few years, published as the alt-ergo-free package, while the current version is the alt-ergo package on opam. OCamlPro offers commercial support to industrial users and funds development partly through the Alt-Ergo Users' Club, a group of supporting organisations. A JavaScript version, Try-Alt-Ergo, runs directly in a web browser.
Industrial uses
Several verification platforms are built on Alt-Ergo:
Why3, a platform for deductive program verification, uses Alt-Ergo as main prover
CAVEAT, a C-verifier developed by CEA and used by Airbus. Alt-Ergo was involved in a DO-178C qualification process led by Airbus, during which a qualification kit was produced.
Frama-C, a framework to analyse C-code, uses Alt-Ergo in the Jessie and WP plugins (dedicated to deductive program verification)
SPARK, uses Alt-Ergo (behind GNATprove) to automate the verification of some assertions in Spark 2014
.svg){kind=logo}