Event-B models, formulas, proof obligations, refinement semantics, and Rodin comparison tools in
Lean 4. The reader accepts Rossi .eventb files and Rodin .tuf theories; the native DSL provides
the same proof-obligation generator and checker.
Event-B tooling is often tied to Rodin and separate analysis tools; this project brings its reader, checker, proof obligations, and refinement semantics into Lean 4.
This project is maintained by its author with AI-assisted development tools. Changes are reviewed, tested, and remain the maintainer's responsibility. Event-B support is under active development; APIs, corpus coverage, and trust boundaries may change. Email prieto.jona@gmail.com if you are interested in trying it or contributing.
lake build
lake exe eventb --help
lake exe eventb check test/rossi-fixtures/witnesses.eventb
lake exe gatesA native model uses the Event-B commands directly:
eventb_machine M where
variables sched
invariant inv1 : sched ⊆ AIRPLANES
event Add where
any a
guard grd1 : "a ∈ AIRPLANES ∖ sched"
action act1 : sched := sched ∪ {a}
#eventb_pog MThe CLI reports parsed models, generated obligations, proof status, trust mode, formulas, and
fingerprints. eventb diff compares generated obligations with Rodin artifacts; eventb report
provides machine-readable output.
The current pinned-corpus snapshot is 38/38 reader, 1102/1102 formula, 940/940 typing,
1133/1133 obligation-name, 1132/1325 derived-statement, and 73/1133 external-declared
baseline checks. Remaining obligations stay visibly unproved; imported Rodin status is accepted
only after supplied-artifact POG regeneration and canonical BPO comparison.
EventB.Semantics provides proof-carrying invariant/refinement contracts, including
frame, gluing, merged-event, witness, and variant contracts. EventB.POGSoundness
provides explicit translated-sequent validity; formula interpretations remain
caller-supplied and are never guessed.
lake build EventB Examples
lake exe gates
lake exe gates --statusThe corpus gate is pinned by corpus/MANIFEST.tsv. The checked-in Rossi fixtures cover parser
boundaries and a typecheckable witness project. Optional ProofWidgets views are built with the
examples target.
For the manual editor gate, open examples/WidgetDemo.lean and examples/LspDemo.lean in VS
Code with the Lean server restarted. Confirm the Infoview model/PO sections, derived goals,
explicit trust badges, Go to Definition, and an unknown-identifier diagnostic; discard any
temporary diagnostic edit before closing the files.
lean-grip supplies byte parsing;
lean-argus supplies CLI parsing; and
termcolor-diagnostics supplies
source-aware diagnostics.
Apache-2.0.