Interoperable and Confident Set-based Proof Assistants – ICSPA

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.