Alt-Ergo: Driving SMT-based Program Verification for Industry

Overview

Alt-Ergo is an open-source SMT solver specialized in deductive program verification. Originally developed around 2006 at LRI (Université Paris-Saclay, Inria Saclay, CNRS) for the Why/Why3 verification platform, it was designed to handle complex verification conditions in software with reliability and precision.

In 2013, Titagone's Formal Methods team took over maintenance, steering Alt-Ergo's development through continual innovation, support, and industrial integration.

The Challenge

The challenge was ambitious: to provide a solver capable of handling rich logical theories, quantified formulas, and real-world software constructs, from arrays and records to bit-vectors and floating-point arithmetic, while remaining open, modular, and performant. Titagone had to ensure that Alt-Ergo could serve as a robust backend for a wide range of verification tools, including Why3, Frama-C, SPARK, Atelier-B, and cryptographic proof environments, meeting industrial standards in avionics, defense, and critical software.

Why They Chose Us

The academic community and industrial partners entrusted Titagone with Alt-Ergo's stewardship because of our unique position bridging research and industry. Our team combines deep expertise in formal methods, SMT solving, and verification with a proven track record of maintaining critical open-source infrastructure. Our research background and close collaboration with academic institutions like Inria ensured we could continue Alt-Ergo's innovation while meeting the demanding requirements of industrial certification standards.

Our Approach

Starting with its formally inspired architecture, a DPLL-style SAT engine, E-matching for quantifiers, and specialized decision procedures. Titagone extended and refined Alt-Ergo to improve completeness, automation, and efficiency.

Key innovations included a native bit-vector theory, model generation for all supported theories, optimization objectives, and improved floating-point support. These developments allowed Alt-Ergo to tackle real industrial verification problems that combine arithmetic, data structures, and low-level manipulations.

Results

• 98% automatic proof success in Atelier-B (up from ~84%)
• DO-178C avionics qualification compliance enabled
• Adopted by Airbus, CEA, Thales, AdaCore, and TrustInSoft
• Thriving ecosystem with active user and R&D community

Impact

Through open-source distribution, regular releases, and active engagement with a user and R&D community, Titagone has cultivated a thriving ecosystem around Alt-Ergo. By combining rigorous software engineering, formal-methods expertise, and collaborative innovation, Alt-Ergo evolved from a research prototype into a widely adopted, high-assurance tool, bridging academic insights and real-world industrial needs.