Alt-Ergo, an automatic solver for mathematical formulas, is mainly used in formal program verification.

Development was undertaken by researchers at the Paris-Sud University, Laboratoire de Recherche en Informatique, Inria Saclay Ile-de-France, and CNRS.

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.

The core architecture of Alt-Ergo comprises three main elements: a depth-first search (DFS)-based SAT solver, a quantifiers instantiation engine that uses e-matching, and an assembly of decision procedures for a range of built-in theories.