BARReL: a modern backend for Atelier B in Lean

Abstract

BARReL is a Lean 4 library bridging Atelier B, an industrial tool for the B method, and the Lean proof assistant by enabling users to conduct their formal B developments---up to machine refinement and implementation---interactively inside Lean, while retaining standard B syntax. B partial operators are encoded with explicit well-definedness conditions, using Lean's dependent types to enforce a well-definedness discipline by construction. That is, proof obligations and proof steps cannot silently rely on ill-typed or ill-defined instantiations. BARReL also provides basic automation for discharging these conditions. The implementation is written entirely using Lean metaprogramming and is designed to be modular: extending the supported B fragment typically requires only adding new syntax and encoding clauses. We compare the resulting workflow with Atelier B on a B refinement development and examine the checks required during interactive proof through two examples.

Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.