Alt-Ergo 2.6 Release: Boosting Formal Verification with New Features

We are thrilled to share that Alt-Ergo 2.6 has officially been released!

Alt-Ergo is an automated prover developped by OCamlPro widely used in formal verification, it plays a key role in static analysis frameworks like the TIS Analyzer, SPARK and Frama-C.

This latest version introduces a series of improvements and new features, particularly in bit-vector reasoning, model generation, and optimization.

The updates in Alt-Ergo 2.6 are directly tied to the progress made in the DéCySif joint research project between AdaCore, Inria, OCamlPro, and TrustInSoft.

What’s New?

  • Enhanced support for bit-vectors and algebraic data types.
  • New optimization capabilities to guide solver behavior.
  • Model generation for a broader range of theories, including bit-vectors.

These updates are particularly valuable for those working on low-level code verification, cryptography, or complex system debugging.

For a deeper dive into the release, including performance comparisons and additional features, visit the full release notes over on OCamlPro’s Blog.

Don’t miss out on this powerful upgrade to Alt-Ergo!