OptiTrust

Deriving trustworthy high-performance code via programmer-guided, source-to-source transformations.

Description

  • The OptiTrust framework provides programmers with means of optimizing their programs via source-to-source transformations. The framework currently supports array-manipulating programs written in a subset of C syntax.
  • OptiTrust leverages static analyses based on a subset of Separation Logic to justify the that the transformations applied are semantic-preserving.
  • OptiTrust supports source-to-source tranformations that preserve separation logic derivations, allowing to validate the property that the final optimized code satisfies the same specification as the unoptimized input program.

A complete description of OptiTrust as of September 2025 may be found in Guillaume Bertholon's PhD thesis. [PDF]

OptiTrust is work in progress.
OptiTrust is open source, and open to collaboration. Hosted on [Github].

Don't hesitate to get in touch with Arthur Charguéraud or Thomas Kœhler.

Demos

Publications

Contributors

The OptiTrust project has been initiated in 2019 by Arthur Charguéraud (Inria and Université de Strasbourg, currently on sabbatical leave). From 2024 to mid-2026, the project was lead jointly Arthur Charguéraud and Thomas Kœhler (CNRS and Université de Strasbourg). Since mid-2026, the project is lead jointly by Thomas Kœhler, Nicolas Magaud (Université de Strasbourg), and Bérenger Bramas (Inria and Université de Strasbourg).

Students and postdocs

  • Yanni Lefki, PhD student, since 2025, works on extending OptiTrust with support for pattern-matching, and with support for producing assembly code.

Other researchers involved in the ANR project

  • Bérenger Bramas (Inria and Université de Strasbourg) is an expert in HPC, most specifically in vectorization and scheduling techniques.
  • Nicolas Magaud (Université de Strasbourg and Inria) is an expert in formal methods for algorithms and mathematics.
  • Jens Gustedt (Inria and Université de Strasbourg) served for 10 years on the C standardization committee, in particular as co-editor of the C17 standard.
  • Alain Ketterlin (Université de Strasbourg) is an expert in polyhedral transformations, a large class of optimizations for performance-critical loop nests.
  • Yannick Zakowski (Inria and ENS Lyon) works on mechanized semantics for programming languages, program logics, and compiler correctness proofs.
  • François Pottier (Inria) works on semantics and program logics for OCaml and multicore OCaml, and on mechanized proofs of time and space bounds.
  • Xavier Leroy (Collège de France and Inria) is the main architect of the OCaml programming language and of the CompCert formally verified compiler.
  • Loïc Correnson (CEA) leads the development of the Frama-C platform for the analysis of C programs.
  • Allan Blanchard (CEA) is a researcher involved in the development of Frama-C, in particular the EVA and WP plugins.
  • Matthieu Lemerre (CEA) is a researcher expert in abstract interpretation and static analysis.
  • Philippe Helluy (Université de Strasbourg and Inria) works on mathematical and numerical analysis of physical systems, and high-performance implementations of simulations.
  • Victor Michel-Dansac (Inria and Université de Strasbourg) is a researcher in applied mathematics, also working on numerical analysis and high-performance simulations.

Past contributors

  • Ramon Fernandez Mir, M1 intern, 4 months in 2018, studied the formalization in Coq of data layout transformations.
  • Damien Roulhing, postdoc, 11 months in 2019, implemented the core of the OptiTrust framework.
  • Begatim Bytyqi, postdoc, 18 months in 2021-2022, extended the transformation library and completed the particle-in-cell case study.
  • Anton Danilkin, L2 intern, 2 months in 2021, worked on the import of Rust code into OptiTrust.
  • Nicolas Nardino, M2 intern advised by Yannick Zakowski, March-July 2023, worked on a mechanized proof relating the semantics of OptiTrust with that of the CompCert verified compiler.
  • Pauline Bonnet, M2 intern, 3 months in 2025, worked on correctness criteria for the parallelization scheme involved in the particle-in-cell case study.
  • Guillaume Bertholon, PhD student March 2022 - August 2025, implemented the typechecker, worked on correctness criteria, and contributed many other improvements to the framework.
  • Elian Morel, Master intern from ETHZ, May 2025 - December 2025, applied OptiTrust to optimize a LLM inference code, and implemented elaboration of focus operations in the typechecker.
  • Julien François de Castelnau, Master intern from EPFL, September 2025 - Mars 2026, worked on applying OptiTrust to produce GPU code.

Funding

  • ANR OptiTrust: from October 2022 to September 2028, the French National Research Agency (ANR) funds a 2-year postdoc position, a 2-year engineer position, internship positions, contributions by 2 CEA researchers, as well as travel and equipment expenses.
  • ENS PhD Grant: the PhD of Guillaume Bertholon, from September 2022 to September 2025, was funded by a PhD grant "contrat doctoral spécifique normaliens" (CDSN).
  • Inria exploratory action: from September 2019 to August 2022, Inria funded a 11-month postdoc position, a 18-month engineer position, a 2-month internship position, as well as travel and equipment expenses.