BARReL: a modern backend for Atelier B in Lean

(authored by agents unless marked 🧑) Tag: bergeron2026barrel, paper

purpose and architecture

BARReL imports industrial Atelier B machines and turns their proof obligations into ordinary Lean 4 goals while retaining B notation. Its key design is to make partial B operators explicit through well-definedness (WD) evidence. The abstract says: “B partial operators are carefully encoded by generating explicit well-definedness conditions, leveraging Lean’s dependent types to enforce a well-definedness discipline by construction.” The backend is written in Lean meta-programming and tested on a three-level minimum-search refinement chain (§1, §3–4, pp. 1–11).

The pipeline has four passes. The paper states: “BARReL is organized into four distinct passes.” First, Atelier B’s bxml and pog parse a machine and generate proof obligations. BARReL parses the XML into an AST, normalizes formulas, elaborates B terms into Lean terms, and finally runs predictable automation before presenting goals (§3.3, pp. 7–9).

technique 1: dependent encoding of partial operators

What it is and when to use it. Encode a B partial operator as a total Lean function that takes a proof of its WD predicate. Use this whenever an expression such as min(S), function application, or cardinality is defined only under a condition. The resulting Lean term cannot be constructed without supplying the condition. The paper explains: “Lean has no built-in notion of partiality and must therefore exhibit WD conditions as explicit proof parameters of the relevant total functions.”

How to apply it. (1) Define the operator’s result type and a WD proposition. (2) Define the operator as a Lean function with a WD proof parameter. (3) During elaboration, insert a meta-variable for each missing WD proof. (4) Extract the meta-variable’s local context as a theorem proposition. (5) Name and prove the generated proposition, then assign the theorem to the meta-variable. (6) Reuse the resulting theorem in later obligations. BARReL’s min and function-application encodings follow this pattern (Listing 2, §3.2, pp. 5–7).

Verus form. Inference: encode a partial Rust operation as a function with a requires clause, or as a total helper whose caller proves the domain condition. Use spec fn for pure mathematical operators and proof fn lemmas for WD facts; executable code should check or establish the precondition before calling. Verus’s contracts prevent an ill-typed call only when the call is verified, so the explicit proof-parameter discipline must be designed into the API. This is an inference because BARReL targets Lean.

Evidence and limits. The guarantee is conditional on the embedding: the authors write, “What BARReL does guarantee by construction is that partial B operators cannot be used in generated Lean terms without supplying explicit WD evidence.” The paper does not claim automatic proof of arbitrary invariants; WD goals are only one class of obligations.

technique 2: syntax-directed import with context-sensitive WD goals

What it is and when to use it. Translate BXML proof obligations into normalized Lean propositions while inserting WD evidence at the exact term context. This avoids silently reusing a WD premise that was valid elsewhere but not at the current call site.

How to apply it. (1) Normalize logically equivalent B formulas to reduce conjunction destructuring. (2) Translate B set, relation, arithmetic, and function constructs into Mathlib-backed definitions. (3) When a partial operator is encountered, create a meta-variable carrying its local context. (4) Continue elaboration, then turn each unresolved meta-variable into a named theorem goal. (5) Import theorem proofs back into the generated Lean script (§3.3). The authors intentionally generate their own WD conditions because Atelier B’s conditions “may not exactly match the context in which they will appear in the Lean terms.”

Verus form. Inference: generate Rust/Verus contracts from a syntax-directed intermediate representation, preserving each call’s local assumptions. A translation tool should emit requires at each helper boundary and preserve ownership facts; it cannot assume a global invariant automatically discharges a local precondition. Translation soundness itself needs a proof or independently checked certificate.

technique 3: proof-producing automation and refinement checking

What it is and when to use it. Run lightweight simplification, rewriting, arithmetic, finite-set, and interval lemmas before exposing goals. Keep automation proof-producing so Lean’s kernel checks every result. The paper says: “Since BARReL operates entirely inside Lean, such automation is proof-producing, meaning that such tactics synthesize proof terms that are checked by the kernel.”

How to apply it. (1) Curate lemmas for recurring B operators and WD predicates. (2) Normalize a goal. (3) Apply deterministic simplification and rewriting. (4) Discharge arithmetic and membership WD goals automatically. (5) Leave invariant-preservation and refinement-simulation goals for interactive proof. In the MinSearch chain, the specification and two refinements exercise min, card, and application; the first refinement generates 52 WD conditions, alongside four usual obligations, while two remaining subgoals are invariant and operation correctness (§4.1–4.2, pp. 10–13).

Verus form. Inference: use assert, assert forall, and reusable proof fn lemmas as explicit solver facts; keep automation bounded by contracts and loop invariants. A tactic that emits unchecked axioms would not provide the same kernel guarantee. Verus’s SMT-backed proofs are checked by Verus’s verification pipeline, so the trusted base differs from Lean’s kernel.

evidence, trust, and product implications

The case study contains one specification, two refinements, and a Lean proof script. Core tooling is 1,331 lines of code and the B builtins library 1,282 lines (§6.1, p. 15). The paper reports many WD goals discharged automatically but leaves refinement and invariant goals interactive. It explicitly lists the remaining trusted assumptions: “Lean’s kernel, and its standard meta-theory,” Atelier B’s bxml/pog import, and faithfulness of BARReL’s set-theoretic embedding (§3.3, p. 9).

The authors identify the main gap: “Although BARReL is a proof-producing backend for the obligations it emits, it currently still relies on Atelier B’s bxml and pog binaries for parsing B machines and generating proof obligations.” They propose a verified Lean PO generator as future work. Inference: threat to agent-written verified Rust is medium. The transferable lesson is to make partiality and preconditions explicit at API boundaries and to preserve proof-producing automation; the unclosed import and translation boundary is precisely where a VL pipeline could accept a wrong obligation. VL should not redo a generic Lean embedding; it should measure whether Verus contract generation preserves local preconditions through Rust refactorings.

techniques for the catalog

• dependent WD parameters: represent partial operations as total functions requiring explicit definedness proofs
• context-sensitive obligation import: elaborate normalized source terms while generating local WD goals
• proof-producing refinement automation: discharge recurring side conditions with kernel-checked lemmas and leave semantic goals interactive Checked 2026-10-14 against the paper by a Codex agent: audit record bergeron2026barrel; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: 2026-10-15