Ghilain Bergeron

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.

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.

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.

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.

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.