💻 computer science

BARReL: a modern backend for Atelier B in Lean

BARReL is a modular Lean 4 library that bridges the industrial Atelier B tool with the Lean proof assistant by encoding B's partial operators with explicit well-definedness conditions, thereby enabling interactive, syntax-preserving formal development and verification of machine refinements within a strongly reliable framework.

Original authors: Ghilain Bergeron, Vincent Trélat

Published 2026-06-19

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Ghilain Bergeron, Vincent Trélat

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are building a skyscraper using a very old, specialized blueprint system called Atelier B. This system is famous in the construction industry because it's incredibly strict: it checks every beam and bolt to ensure the building won't collapse. However, the tools to check these blueprints are a bit like a rigid, old-fashioned calculator. They do the job, but they can't "think" creatively, and if you make a tiny mistake in how you define a part, the calculator might just ignore it or give you a confusing error message.

Now, imagine a new, super-smart construction assistant called Lean. Lean is like a genius architect who can not only check blueprints but also write complex proofs, solve puzzles, and learn from a massive library of math knowledge. But Lean speaks a different language and doesn't understand the old Atelier B blueprints directly.

BARReL is the translator and bridge built by Ghilain Bergeron and Vincent Trélat to connect these two worlds. Here is how it works, using simple analogies:

1. The "Translator" Role

Think of BARReL as a universal translator that sits between the old blueprint system (Atelier B) and the smart assistant (Lean).

When you feed an Atelier B blueprint to BARReL, it doesn't just copy-paste the text. It reads the blueprint, understands the rules, and rewrites the "proof obligations" (the tasks that need to be checked) into a language Lean understands.
Crucially, it keeps the original look and feel of the B language so that the original engineers don't get lost. It's like translating a book into a new language but keeping the original font and layout.

2. The "Safety Guard" for Missing Pieces

The biggest challenge in the old system is partial operators. Imagine a tool in your toolbox that only works if you have a specific type of screw. If you try to use it on a nail, the old system might just say "Okay" and hope for the best, or it might generate a separate, tiny note saying "By the way, make sure you have a screw."

In the old Atelier B system, these "safety notes" (called Well-Definedness conditions) could sometimes get separated from the main task. If a builder forgot to check the note, the building could theoretically be unsafe, but the system wouldn't catch it until much later.

BARReL changes the rules:

It treats these safety notes as mandatory parts of the main task.
Using Lean's "dependent types" (a fancy way of saying "smart rules"), BARReL forces the builder to prove they have the "screw" before they are even allowed to use the tool.
Analogy: It's like a video game where you cannot pick up a key unless you have already proven you have the lock. You can't even try to use the key if the lock doesn't exist. This prevents "silent" mistakes where the system assumes something is true when it isn't.

3. The "Auto-Checker"

While BARReL forces you to prove the hard safety rules, it also has a smart auto-checker.

Many of the "safety notes" are very simple (e.g., "This set of numbers is not empty").
BARReL has a built-in robot that automatically checks these simple notes for you. In the case study they tested, this robot handled 146 out of 190 safety checks automatically.
This leaves the human engineer to focus only on the complex, creative parts of the proof that the robot can't solve yet.

4. The "Refinement" Journey

The paper tested BARReL on a project to find the minimum number in a list. They started with a simple idea and slowly refined it into a complex, step-by-step computer program.

Level 1: A simple idea.
Level 2: A slightly more detailed plan.
Level 3: A specific, step-by-step recipe using a table.
Result: BARReL successfully translated every step of this journey into Lean. It generated hundreds of proof tasks, automatically solved the boring safety checks, and let the human prove the logic. It showed that you can take a complex industrial design and verify it inside the smart Lean environment without losing the original design's structure.

Why This Matters

The authors argue that BARReL is a stepping stone.

Currently, the "translator" (BARReL) relies on the old Atelier B machine to generate the initial list of tasks.
The goal is to eventually build a version where the entire process happens inside the smart Lean environment, removing the need for the old machine entirely. This would create a "fully verified" chain where every single step, from the first blueprint to the final code, is checked by the smart assistant.

In summary: BARReL is a modern, safety-first bridge that lets engineers use the powerful, smart tools of the Lean proof assistant to verify their industrial designs, ensuring that no "missing screws" (undefined operations) are ever ignored.

Technical Summary: BARReL - A Modern Backend for Atelier B in Lean

Problem Statement

The B method and its industrial toolset, Atelier B, have long been the standard for developing safety-critical systems requiring strong assurance arguments. However, the ecosystem relies heavily on the internal provers of Atelier B, which, while effective, operate within a "black box" regarding their trusted computing base (TCB). Although previous efforts have attempted to connect B to modern interactive theorem provers (ITPs) like Isabelle, PVS, or Rocq, these approaches often focus on formalizing the semantics of B rather than providing a practical, integrated backend for existing industrial workflows. Furthermore, existing tools often lack robust handling of partial operators (e.g., min, function application on partial domains), which are central to the B method but require careful well-definedness (WD) checks to ensure logical soundness. In Atelier B's interactive mode, users can inadvertently instantiate terms that are ill-defined (e.g., min(∅)), leading to unsound proofs if the tool fails to enforce typing constraints during manual rule application.

Methodology

The paper introduces BARReL (B Automated tRanslation for Reasoning in Lean), a Lean 4 library designed to bridge Atelier B and the Lean proof assistant. The methodology relies on a modular translation pipeline that converts B proof obligations (POs) into Lean theorems, leveraging Lean's dependent type system to enforce well-definedness by construction.

Core Architecture

The workflow, illustrated in Figure 1 of the paper, proceeds through four distinct passes:

Parsing and PO Generation: BARReL accepts B machines (.mch), refinements, or existing Proof Obligation Generator (POG) files. It invokes Atelier B's bxml and pog tools to generate proof obligations in XML format.
AST Normalization: The XML POs are parsed into an Abstract Syntax Tree (AST) and normalized (e.g., converting P ∧ Q ⇒ R to P ⇒ Q ⇒ R) to simplify subsequent encoding.
Encoding and Meta-Programming: The normalized B formulas are transcribed into Lean terms using Lean's meta-programming framework. Crucially, this layer maps B's set-theoretic constructs to Mathlib's typed set and relation primitives.
Well-Definedness (WD) Handling: This is the central technical innovation. Instead of relying on Atelier B's implicit handling of partial operators, BARReL generates explicit WD conditions for every partial operator usage.

Handling Partial Operators

In B, operators like min(S) or function application f(x) are partial. Atelier B generates WD side goals but assumes the main goal holds if these are satisfied. BARReL differs by encoding partial operators as total Lean functions that require a proof of well-definedness as an explicit argument.

Mechanism: Using Classical.choose (Hilbert's $\epsilon$ operator), BARReL defines partial operators such that their type signature includes a proof parameter (e.g., min.WD S).
Enforcement: To use min(S) in a Lean term, the user must provide a proof that S satisfies the WD condition (e.g., S is non-empty and bounded below).
Automation: BARReL generates these WD proofs as side theorems or subgoals. A lightweight automation tactic layer, tagged with categories like wd_min or wd_app, attempts to discharge these routine WD goals automatically using Mathlib's rewriting rules and set-theoretic lemmas.

Trust Boundary

The system is designed as a proof-producing backend. Once a user discharges a goal in Lean, the resulting theorem is checked by Lean's small, auditable kernel. The trusted components are reduced to:

Lean's kernel and meta-theory.
The correctness of Atelier B's external PO generation (the bxml/pog step).
The faithfulness of BARReL's encoding of B semantics into Lean.
The paper explicitly notes that the interactive layer of Atelier B (where users manually instantiate variables) is not proof-producing and can lead to inconsistencies; BARReL eliminates this risk by enforcing type-correctness and well-definedness via Lean's type checker.

Key Contributions

BARReL Library: An open-source, modular Lean 4 backend that translates B developments (machines, refinements, implementations) into Lean theorems while preserving B syntax and notation as closely as possible.
Explicit Well-Definedness Discipline: A translation pipeline that converts B's implicit partiality into explicit, provable well-definedness conditions. This prevents the silent reliance on ill-typed or ill-defined instantiations, a known pitfall in Atelier B's interactive prover.
Evaluation and Workflow: A demonstration of an end-to-end refinement chain (a minimum search algorithm) within Lean. The study shows that while BARReL generates a higher volume of WD goals than Atelier B, the vast majority are discharged automatically, leaving the user to focus on the core refinement logic.

Results

The authors evaluated BARReL on a three-level refinement chain for a "minimum search" specification:

Scale: The case study generated a total of 190 goals across three levels (specification, two refinements).
Well-Definedness Overhead: Of these, 146 goals were WD conditions.
Automation Success: BARReL's automation successfully discharged 100% of the generated WD conditions automatically.
Comparison:
- Atelier B: Generated fewer WD goals (e.g., 2 for the second refinement) because it shares conditions across sub-goals. However, its interactive prover allows unsound instantiations (e.g., min(∅)) if the user is not careful.
- BARReL: Generated more WD goals (e.g., 100 for the second refinement) because it reifies conditions per occurrence. However, all were automatically discharged, and the remaining 21 standard POs were proved interactively in Lean.
Implementation Metrics: The core tooling consists of 1,331 lines of code (LoC), with an additional 1,282 LoC for the supporting lemma library and automation tactics.

Significance and Claims

The paper positions BARReL as a stepping stone toward a strongly reliable Atelier B toolchain grounded in Lean.

Reliability: By moving the proof obligations into Lean, BARReL ensures that all proofs are checked by a small, verified kernel, eliminating the risk of unsound interactive proofs found in Atelier B's GUI.
Usability: The system retains the familiar B syntax and structure, minimizing the learning curve for industrial B developers.
Extensibility: The modular design allows for the incremental addition of new B constructs and encoding rules.
Future Directions: The authors identify three main avenues for future work:
1. Extending the supported fragment of the B language (e.g., sequences, trees, advanced quantifiers).
2. Reducing redundancy in WD goals via subsumption (to address the higher goal count compared to Atelier B).
3. Developing a verified PO generator within Lean itself, which would eventually remove Atelier B's pog from the trusted computing base and enable an embedded DSL for writing B directly in Lean.

The paper concludes that BARReL successfully demonstrates that industrial B developments can be migrated to a modern, type-theoretic backend without sacrificing the structural integrity of the original specifications, while significantly enhancing the soundness guarantees of the verification process.