Why Would You Trust B?

TL;DR

This paper investigates the trustworthiness of the B formal method by embedding its logic in Coq, enabling formal verification of B theories and tools, including a verified prover.

Contribution

It introduces a deep embedding of B logic in Coq, allowing formal checking of B theories and the implementation of verified B tools, enhancing confidence in their correctness.

Findings

Successfully embedded B logic in Coq for formal verification.

Developed a verified prover for B logic.

Demonstrated increased trust in B tools through formal checking.

Abstract

The use of formal methods provides confidence in the correctness of developments. Yet one may argue about the actual level of confidence obtained when the method itself -- or its implementation -- is not formally checked. We address this question for the B, a widely used formal method that allows for the derivation of correct programs from specifications. Through a deep embedding of the B logic in Coq, we check the B theory but also implement B tools. Both aspects are illustrated by the description of a proved prover for the B logic.