Alt-Ergo
An automatic SMT solver for software verification. Alt-Ergo proves mathematical formulas generated by tools like Frama-C, SPARK, Why3, Atelier-B, and Caveat, ensuring critical software behaves exactly as intended.
SMT-powered verification
Alt-Ergo is based on Satisfiability Modulo Theories (SMT), a powerful reasoning technology that checks the consistency of complex logical formulas. It acts as a trusted mathematical engine inside verification tools, from critical systems to cryptographic protocols.
Automatic Theorem Proving
Alt-Ergo automatically proves mathematical formulas generated by software verification tools, with no manual proof effort required for the vast majority of verification conditions.
Rich Theory Support
Supports linear and non-linear arithmetic, polymorphic arrays, enumerated and record datatypes, bit-vectors, and AC symbols, covering the theories needed by real-world verification.
Seamless Integration
Works as a backend for Frama-C, SPARK, Why3, Atelier-B, and Caveat. Drop Alt-Ergo into your existing verification workflow with zero friction.
Formally Verified Core
Key components of Alt-Ergo have been formally proved correct using the Rocq proof assistant, so you can trust it to give sound answers.
Comprehensive theory support
Join the Alt-Ergo community
The Alt-Ergo Users' Club was launched in 2019 to bring our team closer to users, collect their needs, and ensure sustainable funding for long-term development.
Commercial License
Access to the latest version of Alt-Ergo for commercial use in your verification workflows.
Dedicated Support
Priority support from the Alt-Ergo development team in case of critical issues or integration questions.
Roadmap Influence
Voting rights on important decisions shaping the future development of Alt-Ergo.
Trusted by industry leaders
Alt-Ergo in production
Frequently asked questions
What is an SMT solver?
An SMT (Satisfiability Modulo Theories) solver is a tool that automatically determines whether mathematical formulas are satisfiable. Alt-Ergo is used as a backend by verification tools to prove that software behaves correctly, without requiring manual proof effort.
Which verification tools work with Alt-Ergo?
Alt-Ergo integrates with Frama-C, SPARK, Why3, Atelier-B, and Caveat. It acts as a trusted mathematical engine inside these verification workflows with zero friction.
What is the Alt-Ergo Users' Club?
The Users' Club provides a commercial license, dedicated support from the development team, and voting rights on the Alt-Ergo roadmap. It was launched in 2019 to ensure sustainable long-term development.
Is Alt-Ergo open source?
Yes, Alt-Ergo is open source and available on GitHub. The Users' Club offers a commercial license for organizations that need professional support and want to influence the project's direction.
What theories does Alt-Ergo support?
Alt-Ergo supports 8 theories including linear and non-linear arithmetic, polymorphic arrays, enumerated and record datatypes, bit-vectors, and associative-commutative symbols.