LeanMachines: State-based Modeling with Refinement (a Lean4 Framework)

We present a framework for the formal modeling of state-based systems in the context of the Lean4 programming language and proof assistant. In this context, the main objective is to support a step-wise refinement methodology inspired conceptually by the Event-B formal method. As a starting point, the LeanMachines framework proposes Lean4 constructions for the main Event-B concepts such as contexts, machines and events. Most importantly, the associated refinement principles are introduced in the form of typeclass constructions inspired by (and in fact built upon) the Mathlib mathematical framework. Beyond the basic concepts and structures, we also experiment with extensions of the framework. First, we develop an algebra of event combinators that allow to compose complex event structures out of simpler ones. These combinators are based on algebraic structures – functors, arrows, etc. – that have been developed and studied in the context of (functional) programming language theory. Our proposed formalization of the Event-B concepts is very shallow in the sense that all the constructions are directly based on the Lean4 logic and abstractions. One benefit is that proof obligations can be discharged using the tactic language of Lean4 with almost no embedding overhead such as an abstraction barrier that would require syntactic conversions, or the necessity to use some dedicated proof tactics. As an important design guideline, we enforce the fundamental principle of correctness-by-construction: machine states, events structures and refinement steps cannot be fully constructed without discharging the prescribed proof obligations.