Ghilain Bergeron

Ghilain Bergeron, Horatiu Cirstea, Stephan Merz

To appear in: Journal of Logical and Algebraic Methods in Programming (2026)

Formal verification techniques are frequently used to ensure correctness properties of distributed systems and algorithms. However, languages used for formal modeling and verification are often substantially different from languages used in software development, and verifying an abstract representation of an algorithm does not ensure that its handwritten implementation will be correct. This paper presents work in progress on a verified compiler for an extension of Lamport's PlusCal with threads and communication channels. Its syntax and semantics are formalized in the Lean 4 proof assistant and the passes compiling PlusCal algorithms into Go code are implemented in the underlying Lean 4 programming language. This paper gives formal semantics for the first pass of the compiler and outlines its mechanically verified correctness proof.

Ghilain Bergeron, Vincent Trélat

Submitted

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.

Ghilain Bergeron, Vincent Trélat

In: Approches Formelles pour l’Assistance au Développement de Logiciels (AFADL) (2026)

BARReL est une bibliothèque Lean 4 qui fait le lien entre Atelier B, un outil industriel pour la méthode B, et l'assistant à la preuve Lean, en permettant aux utilisateurs de mener leurs développements formels en B---du raffinement des machines jusqu'à l'implémentation---de manière interactive dans Lean, tout en conservant la syntaxe standard de B. Les opérateurs partiels de B sont encodés soigneusement en générant des conditions explicites de bonne définition, en tirant parti des types dépendants de Lean pour imposer, par construction, une discipline de bonne définition. Autrement dit, les obligations de preuve et les étapes de preuve ne peuvent pas reposer implicitement sur des objets mal typés ou mal définis. BARReL propose aussi une automatisation de base pour tenter de décharger automatiquement de telles conditions de bonne définition. L'implémentation utilise les fonctionnalités de métaprogrammation de Lean et est conçue pour être modulaire : étendre le fragment de B pris en charge revient généralement à ajouter de la nouvelle syntaxe et des clauses d'encodage. Nous illustrons l'approche sur une étude de cas représentative et affirmons que BARReL peut constituer une première étape vers une chaîne d'outils fiables pour la méthode B.

Ghilain Bergeron

In: Approches Formelles pour l’Assistance au Développement de Logiciels (AFADL) (2026)

We present a compilation scheme from Network PlusCal, a dialect of PlusCal equipped with explicit network communication primitives, to the Join Calculus. This scheme maps each Network PlusCal process to a Join Calculus program that encodes local variables as local state atoms and control flow as a family of guarded reactions. Mutual exclusion among non-deterministic branches of atomic blocks is enforced by a per-block nullary atom that is consumed once a branch succeeds. We illustrate this scheme on a Ping-Pong example involving a server and multiple client processes.

Ghilain Bergeron, Florent Krasnopol, Sophie Tourret

In: 16th International Conference on Interactive Theorem Proving (ITP) (2025)

We describe the formalization in Isabelle/HOL of a framework for splitting, a theorem proving technique that extends saturation-based calculi with branching abilities. The framework preserves the completeness of the original calculus. We focus here on the simplest splitting model and provide an extension of the ordered resolution calculus with a variant of splitting called Lightweight AVATAR.

Ghilain Bergeron, Horatiu Cirstea, Stephan Merz

In: 11th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE) (2025)

Formal verification techniques are frequently used to ensure correctness properties of distributed systems and algorithms. However, languages used for formal modeling and verification are often substantially different from languages used in software development, and verifying an abstract representation of an algorithm does not ensure that its handwritten implementation will be correct. This paper presents work in progress on a verified compiler for an extension of Lamport's PlusCal with threads and communication channels. Its syntax and semantics are formalized in the Lean 4 proof assistant and the passes compiling PlusCal algorithms into Go code are implemented in the underlying Lean 4 programming language. This paper gives formal semantics for the first pass of the compiler and outlines its mechanically verified correctness proof.

Ghilain Bergeron, Stéphane Glondu, Sophie Tourret

In: Isabelle Workshop (2024)

This paper is a report on the use of a ten-year-old proof translation technique from HOL Light to Isabelle/HOL. We demonstrate the reusability of the technique and provide a detailed account of the steps needed to adapt the code both to a newer version of the HOL Light kernel and to the translation of specific HOL Light theorems. Thus, in addition to the proof of reusability, this paper provides a guideline for anyone wishing to use HOL Light theorems in Isabelle/HOL.