Alt-Ergo

This article needs more citations. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed. Find sources: "Alt-Ergo" – news · newspapers · books · scholar · JSTOR (July 2023) (Learn how and when to remove this message)

Alt-Ergo
Developer	OCamlPro
Written in	OCaml
Available in	English
Type	Mathematical solver, program verifier
Website	alt-ergo.ocamlpro.com
Repository	github.com/OCamlPro/alt-ergo

Alt-Ergo, an automatic solver for mathematical formulas, is mainly used in formal program verification. It operates on the principle of satisfiability modulo theories (SMT). Development began in 2006 at the Laboratoire de Recherche en Informatique (LRI), a joint CNRS/Inria unit, at what is now Paris-Saclay University. Since 2013 it has been maintained, developed and distributed by the Formal Methods team at OCamlPro. It is released under the free and open-source software CeCILL-C license.

History

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

Licensing and support

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
• Atelier-B can use Alt-Ergo instead of its main prover (raising success from 84% to 98% on ANR Bware project benchmarks)
• Rodin, a B-method framework developed by Systerel, can use Alt-Ergo as a back-end
• Cubicle, an open source model checker to verify safety properties of array-based transition systems
• EasyCrypt, a toolset for reasoning about relational properties of probabilistic computations with adversarial code
• BWARE
• Cafein
• FUI Hi-Lite
• Decert
• ADT Alt-Ergo
• A3PAT
• TrustInSoft Analyzer, a static analysis tool, and Frama-C use Alt-Ergo as one of their solvers.

See also

• Formal verification
• Z3 Theorem Prover