Alt-Ergo Users’ Club Annual Meeting (2021)

The third annual meeting of the Alt-Ergo Users’ Club took place on April 1! Our annual meeting is the ideal place to review the needs of each partner regarding Alt-Ergo. We were pleased to welcome our partners to discuss the roadmap for future Alt-Ergo developments and improvements.

Alt-Ergo is an automatic prover of mathematical formulas, jointly developed by LRI and OCamlPro (since 2014). To learn more or join the Club, visit

Our Club has several goals. Its main objective is to ensure the sustainability of Alt-Ergo by fostering collaboration between Club members and by building links with users of formal methods, such as the Why3 community. One of our priorities is to define the needs of users of constraint solvers by extending Alt-Ergo to new domains such as Model Checking, while competing with other state-of-the-art solvers in international competitions. Finally, the Club aims to find new projects or contracts for the development of long term functionalities.

We would like to thank all our members for their support: Mitsubishi Electric R&D Centre Europe, AdaCore and CEA List. We would also like to acknowledge the help of the Why3 development team with whom we work to improve our tools.

This year, new points of interest were raised by our members. Firstly, model generation, which was added to Alt-Ergo in the last edition, has been useful to the majority of our club members. Firstly, we will now focus on refining the constraints and studying how to propagate them. Secondly, we presented Dolmen: the parser/typer that will allow to type only once SMT2 files and to be ready for SMT3. Its integration to Alt-Ergo is in progress. The opinion of the club members is warm about the future contributions of the Dolmen tool to the SMT solver community!

These features are now our main priorities. You can see the boards presented at the 2021 Club meeting. To follow our progress on the new features, follow the articles on our blog!

About OCamlPro:

OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from state-of-the art programming languages like OCaml and Rust. We design, create and implement custom ad-hoc software for our clients. We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam, TryOCaml, ocp-indent, ocp-index and ocp-browser, and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch. Another area of expertise is that of Formal Methods, with tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users’ Club). We also provide vocational trainings in OCaml and Rust, and we can build courses on formal methods on-demand. Do not hesitate to reach out by email:

Leave a Reply

Your email address will not be published. Required fields are marked *