# BARReL: a modern backend for Atelier B in Lean

Preprint · Ghilain Bergeron, Vincent Trélat

- Archive id: arxiv:2606.20121
- Published: 2026-06-18
- arXiv: https://arxiv.org/abs/2606.20121
- Source URL: https://arxiv.org/abs/2606.20121
- PDF: https://arxiv.org/pdf/2606.20121
- Provenance: arxiv

## 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 reproduced under CC0-1.0 (arXiv descriptive metadata)._

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.