CE25 - Sciences et génie du logiciel - Réseaux de communication multi-usages, infrastructures de hautes performances

Interoperable and Confident Set-based Proof Assistants – ICSPA

Submission summary

Formal deductive methods aim at improving the quality of software by relying on tools based on strong mathematical grounds, like set theory. Those tools allow the user to prove the properties that ensure the correctness of a software with respect to its specification. When human safety is at stake, confidence in proofs is crucial, however the implementation of a prover is a complex, error-prone, and sometimes buggy task.

ICSPA focuses on the set-based specification formalisms B, Event-B, and TLA+ that have been adopted for industrial development projects, for applications where correctness is critical. It aims at reinforcing the confidence in proofs carried out mechanically using them. Our project also aims at designing and implementing an exchange framework, through which those three systems can share their proofs and theories, making them effectively interoperable.

The strategy we adopt is to verify these proofs formally and independently with Dedukti, a proof checker simple enough to be audited manually or even re-implemented. Through the versatility offered by Dedukti as a common foundation, safe-software programmers will be able to exchange artefacts between B, Event-B and TLA+ developments, within their respective IDEs Atelier B, Rodin and TLAPS. This approach is inspired from the one successfully instigated by Logipedia, a small library of mathematical results that can be exported to, and verified by, a wide range of formal systems, including Coq and HOL.

To reach our goals, we will express the set theories underlying the three specification languages in Dedukti and then export their proof traces, in order to verify them independently using Dedukti. This will be the core mechanism for a more ambitious export of complete models used for the development of real software for safety-critical systems, with a particular focus on Labelled Transitions Systems. With this data, we will define translations between systems at the Dedukti level and import functionalities into the tools Atelier B, Rodin, and TLAPS. This will allow for importing in one system what has been exported from another system.

This backbone architecture will be supported by proof reconstruction features provided by automated theorem provers, that will enable explicit completion of high- and middle-level, often incomplete, proof traces. It will be backed up with additional anchors, obtained by horizontally matching definitions and statements across tools.

The impact of this methodology will be assessed on a very large body of proof obligations provided by our industrial partner. Moreover, case studies for interoperability will be elaborated. Lastly, beyond academic and educational/training dissemination, the export/import, completion by an automated theorem prover, and verification by Dedukti features will be integrated into Atelier B and exploited at an industrial scale.

Project coordination

Catherine Dubois (Télécom SudParis)

The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.


Inria Saclay - Ile de France - Equipe DEDUCTEAM Centre de Recherche Inria Saclay - Île-de-France
TSP Télécom SudParis
IRIT/ Université Toulouse Institut de Recherche en Informatique de Toulouse
Inria Nancy Grand Est Centre de Recherche Inria Nancy - Grand Est
UM-LIRMM Laboratoire d'Informatique, de Robotique et de Microélectronique de Montpellier

Help of the ANR 624,014 euros
Beginning and duration of the scientific project: December 2021 - 48 Months

Useful links

Explorez notre base de projets financés



ANR makes available its datasets on funded projects, click here to find more.

Sign up for the latest news:
Subscribe to our newsletter