pith. sign in

arxiv: 2606.20121 · v1 · pith:4EQKBPBKnew · submitted 2026-06-18 · 💻 cs.LO

BARReL: a modern backend for Atelier B in Lean

Ghilain Bergeron , Vincent Tr\'elat This is my paper

Pith reviewed 2026-06-26 15:20 UTC · model grok-4.3

classification 💻 cs.LO
keywords B methodLean proof assistantformal verificationpartial operatorswell-definednessAtelier Brefinementinteractive theorem proving
0
0 comments X

The pith

BARReL encodes B developments inside Lean so that interactive proofs up to implementation keep standard B syntax and cannot rely on ill-defined operator uses.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces BARReL as a Lean 4 library that lets users carry out formal developments in the B method interactively inside Lean while preserving the usual B syntax. Partial operators from B are translated so that every use generates an explicit well-definedness condition enforced by Lean's dependent types. This prevents proof steps or obligations from depending on terms that are not properly defined. Basic automation is supplied to discharge many of those conditions, and the design is modular so that new B constructs can be added with only syntax and encoding rules. The work is presented as a bridge that could support a more reliable Atelier B toolchain built on Lean.

Core claim

BARReL provides an encoding of B syntax and semantics inside Lean 4 that supports full developments through machine refinement and implementation; partial operators are represented so that dependent types automatically produce well-definedness conditions, ensuring that neither proof obligations nor individual proof steps can proceed from ill-defined instantiations, with the entire implementation done via Lean meta-programming.

What carries the argument

Encoding of B partial operators that generates explicit well-definedness conditions from Lean's dependent types.

If this is right

  • B users can perform interactive proofs and refinements inside Lean without leaving the standard B syntax.
  • Proof obligations and steps are forced to respect well-definedness by construction rather than by later checking.
  • Extending the supported B fragment requires only new syntax declarations and encoding clauses.
  • The library supplies initial automation for discharging the generated well-definedness conditions.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same dependent-type discipline could be applied to embed other specification languages that contain partial functions.
  • If the encoding scales, it opens the possibility of reusing Lean libraries for tactics or automation directly on B developments.
  • A mismatch between the supported B fragment and real industrial models would limit the approach to small case studies only.

Load-bearing premise

The mapping from B partial operators to Lean expressions with generated well-definedness conditions remains faithful to B semantics across the fragment required for complete developments.

What would settle it

A concrete B machine or refinement that Atelier B accepts but BARReL rejects because its well-definedness condition is not discharged or is generated incorrectly.

read the original 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 carefully encoded by generating explicit well-definedness conditions, leveraging 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 features basic automation to try to discharge such well-definedness conditions automatically. The implementation is written entirely using Lean meta-programming and is designed to be modular: extending the supported B fragment typically requires only adding new syntax and encoding clauses. We illustrate the approach on a small but representative case study, and argue that BARReL can act as a stepping stone towards a strongly reliable Atelier B toolchain grounded in the Lean proof assistant.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

3 major / 2 minor

Summary. The paper presents BARReL, a Lean 4 library that acts as a backend for Atelier B. It enables users to perform B-method developments interactively inside Lean up to machine refinement and implementation while retaining standard B syntax. Partial operators are encoded via explicit well-definedness conditions generated from Lean's dependent types, with the goal of preventing proof steps from silently depending on ill-defined terms. The implementation relies on Lean meta-programming, is designed to be modular, includes basic automation for discharging well-definedness conditions, and is illustrated via a small case study. The authors argue that BARReL can serve as a stepping stone toward a more reliable Atelier B toolchain grounded in Lean.

Significance. If the encoding of B partial operators is faithful to Atelier B semantics and the implementation scales, the work would provide a concrete bridge between an industrial formal-methods tool and a modern interactive theorem prover. This could improve the reliability of B developments by leveraging Lean's kernel for well-definedness discipline. The modular meta-programming design and automation for well-definedness conditions are practical strengths that could facilitate extensions.

major comments (3)
  1. [Abstract / encoding section] Abstract and § on encoding of partial operators: the central claim that well-definedness conditions are generated 'by construction' so that 'proof obligations and proof steps cannot silently rely on ill-defined instantiations' is presented without a formal equivalence argument, semantic preservation proof, or side-by-side comparison of generated obligations against Atelier B. Only a small case study is supplied, leaving open the possibility of mismatches in substitutions, quantifiers, or refinement steps.
  2. [Case study] Case study section: the illustration is described as 'small but representative' and covering developments 'up to machine refinement and implementation,' yet no quantitative data, obligation counts, or direct comparison with Atelier B output is reported. This makes it impossible to assess whether the supported fragment is sufficient for the claimed scope.
  3. [Implementation] Implementation and automation sections: while the use of Lean meta-programming for modularity is noted, there is no description of how the generated well-definedness conditions interact with Lean's type checker in refinement or implementation phases, nor any discussion of potential gaps in coverage for B's full operator set.
minor comments (2)
  1. [Abstract] The abstract and introduction could more clearly distinguish between the implemented fragment and the full B method, and should include a brief statement on the current limitations of the supported syntax.
  2. [Introduction] References to prior work on B encodings in other provers (e.g., Why3, Coq) are mentioned only in passing; a short related-work paragraph would help situate the contribution.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the thoughtful and detailed report. We address each major comment below, indicating planned revisions where appropriate. Our responses focus on clarifying the paper's scope as an implementation and design contribution rather than a full semantic verification effort.

read point-by-point responses

  1. Referee: [Abstract / encoding section] Abstract and § on encoding of partial operators: the central claim that well-definedness conditions are generated 'by construction' so that 'proof obligations and proof steps cannot silently rely on ill-defined instantiations' is presented without a formal equivalence argument, semantic preservation proof, or side-by-side comparison of generated obligations against Atelier B. Only a small case study is supplied, leaving open the possibility of mismatches in substitutions, quantifiers, or refinement steps.

    Authors: We acknowledge that the manuscript does not contain a formal semantic equivalence argument or side-by-side obligation comparison with Atelier B. The central claim is grounded in the design choice to encode partial operators using Lean's dependent types so that ill-defined terms are rejected at the type level rather than during proof. This is presented as a practical mechanism rather than a proven semantic preservation result. The paper's emphasis is on the implementation approach and modularity via meta-programming. We will revise the abstract and encoding section to explicitly state the intended correspondence with Atelier B semantics, note the absence of a full proof, and clarify that the case study is illustrative rather than exhaustive. revision: partial

  2. Referee: [Case study] Case study section: the illustration is described as 'small but representative' and covering developments 'up to machine refinement and implementation,' yet no quantitative data, obligation counts, or direct comparison with Atelier B output is reported. This makes it impossible to assess whether the supported fragment is sufficient for the claimed scope.

    Authors: The case study is described as small because its purpose is to demonstrate the encoding of partial operators and the overall workflow up to refinement, not to provide a performance benchmark. We agree that including concrete metrics such as the number of well-definedness obligations generated and discharged would help readers evaluate the supported fragment. We will add these details from the existing case study to the revised manuscript. revision: yes

  3. Referee: [Implementation] Implementation and automation sections: while the use of Lean meta-programming for modularity is noted, there is no description of how the generated well-definedness conditions interact with Lean's type checker in refinement or implementation phases, nor any discussion of potential gaps in coverage for B's full operator set.

    Authors: We agree that the implementation section would benefit from additional detail on how well-definedness conditions are checked by Lean's kernel during refinement and implementation steps, as well as an explicit discussion of coverage limitations for the full B operator set. The current text highlights the meta-programming design for extensibility but does not elaborate on these interactions. We will expand the relevant sections to include this information and note any known gaps. revision: yes

Circularity Check

0 steps flagged

No circularity: implementation description with no derived quantities

full rationale

The paper describes a Lean library implementation that encodes B operators via dependent types to generate well-definedness conditions 'by construction.' No equations, predictions, fitted parameters, or derivation chains appear. The central claim is an engineering artifact (syntax retention + type-enforced discipline) rather than a result obtained from prior inputs. No self-citations or ansatzes are invoked as load-bearing steps. The faithfulness question raised by the skeptic is a correctness/verification issue, not a circularity reduction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on the assumption that Lean’s dependent types can faithfully capture B’s well-definedness discipline; no free parameters or new entities are introduced in the abstract.

axioms (1)
  • domain assumption Lean's dependent types can enforce a well-definedness discipline by construction for B partial operators
    Invoked to guarantee that proof steps cannot silently rely on ill-defined instantiations.

pith-pipeline@v0.9.1-grok · 5692 in / 1171 out tokens · 22561 ms · 2026-06-26T15:20:19.733070+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

15 extracted references · 6 canonical work pages

  1. [1]

    1996 , isbn =

    Abrial, Jean-Raymond , title =. 1996 , isbn =

    1996

  2. [2]

    Cambridge University Press (2010).https://doi.org/10.1017/CBO9781139195881

    Abrial, Jean-Raymond , year =. doi:10.1017/CBO9781139195881 , publisher =

    work page doi:10.1017/cbo9781139195881

  3. [3]

    International Journal on Software Tools for Technology Transfer , author =

    Rodin: an open toolset for modelling and reasoning in. International Journal on Software Tools for Technology Transfer , author =. 2010 , pages =. doi:10.1007/s10009-010-0145-y , abstract =

    work page doi:10.1007/s10009-010-0145-y 2010

  4. [4]

    doi:10.1007/978-3-031-94533-5\_4 , editor =

    Trélat, Vincent , booktitle =. doi:10.1007/978-3-031-94533-5\_4 , editor =

    work page doi:10.1007/978-3-031-94533-5

  5. [5]

    Abrial, J. -R. and Lee, M. K. O. and Neilson, D. S. and Scharbach, P. N. and S. The. VDM '91 Formal Software Development Methods , year =

  6. [6]

    Type Synthesis in

    Bodeveix, Jean-Paul and Filali, Mamoun , editor =. Type Synthesis in. ZB 2002:Formal Specification and Development in Z and B , year =

    2002

  7. [7]

    doi:10.5281/zenodo.17473943 , url =

    The Rocq Development Team , title =. doi:10.5281/zenodo.17473943 , url =

    work page doi:10.5281/zenodo.17473943

  8. [8]

    Haniel Barbosa and others , editor =. cvc5:. Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference,. 2022 , url =. doi:10.1007/978-3-030-99524-9\_24 , timestamp =

    work page doi:10.1007/978-3-030-99524-9 2022

  9. [9]

    Science of Computer Programming , doi =

    D. Science of Computer Programming , doi =. 2013 , month =

    2013

  10. [10]

    2002 , publisher =

    Nipkow, Tobias and Paulson, Lawrence C and Wenzel, Markus , volume =. 2002 , publisher =

    2002

  11. [11]

    de Moura, S

    The Lean 4 Theorem Prover and Programming Language , author =. 2021 , isbn =. doi:10.1007/978-3-030-79876-5_37 , booktitle =

    work page doi:10.1007/978-3-030-79876-5_37 2021

  12. [12]

    Baanen, Anne and Ballard, Matthew Robert and Commelin, Johan and Chen, Bryan Gin--ge and Rothgang, Michael and Testa, Damiano , editor =. Growing. Intelligent Computer Mathematics , year =

  13. [13]

    2012 , url =

    Matthias Schmalz , title =. 2012 , url =

    2012

  14. [14]

    Rigorous State-Based Methods - 10th International Conference,

    Beno. Rigorous State-Based Methods - 10th International Conference,. 2024 , url =

    2024

  15. [15]

    Z3: an efficient SMT solver , year =

    De Moura, Leonardo and Bj. Z3: an efficient SMT solver , year =. Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages =