Alt-Ergo: An SMT Solver for Software Verification

Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools such as Frama-C, SPARK, Why3, Atelier-B and Caveat.

Alt-Ergo website Try Alt-Ergo

Research project

Key features

Supported by both research and industry
Seamless integration with existing tools
Core formally proved with the Rocq proof assistant
Supports a comprehensive set of theories

How it works

Alt-Ergo is based on SMT (Satisfiability Modulo Theories), a powerful reasoning technology used to check the consistency of complex logical formulas. In practice, it acts as a trusted mathematical engine inside verification tools, ensuring that software behaves exactly as intended, from critical systems to cryptographic protocols.

Turn your problem of

hardware design

software verification

formal testing

hardware design

into mathematical formulas

solved by Alt-Ergo

Alt-Ergo is widely used as a backend in various tools, notably via Why3. For example, Frama-C uses it to verify C code, SPARK for Ada programs, and it is also applied to B modelizations and cryptographic protocol verification.

The Alt-Ergo Users' Club

The Alt-Ergo Users' Club was launched in 2019, as a way for the Alt-Ergo team to get closer to their users, collect their needs, integrate them in the Alt-Ergo roadmap, and ensure sustainable funding for this project's long-term development.

The benefits you get

Access to the latest version for commercial use
Dedicated support in case of critical problems
Voting rights on important decisions

Join the club

They work with us!

Features

A large support of theories

Free Theory of Equality with Uninterpreted Symbols

Linear Arithmetic over Integers and Rationals

Fragments of Non-Linear Arithmetic

Polymorphic Functional Arrays with Extensionality

Enumerated Datatypes

Record Datatypes

Associative and Commutative (AC) Symbols

Fixed-Size Bit-Vectors with Concatenation and Extraction Operators

Success Stories

See how Alt-Ergo is being used in industry

Driving SMT-Based Program Verification for Industry

Discover how Alt-Ergo evolved from a research prototype into an industrial-strength SMT solver, reaching 98% automatic proof success for critical systems.