A Rust toolchain for Event-B.
Rossi provides a parser, static checker, command-line tool, and language server for
the Event-B modeling language. Author .eventb as text
and round-trip it through Rodin.
Event-B is a formal method for system-level modeling and analysis, developed around the Rodin Platform. Rossi lets you author Event-B as plain text and work with it from the command line and your editor — alongside Rodin, not in place of it.
Background: Event-B · wiki.event-b.org · ProB
Four crates covering the full author-to-Rodin path.
Parse & round-trip
pest-based parser and typed AST. Text ↔ native Rodin .buc / .bum / .zip XML, Unicode or ASCII operators, with a configurable pretty-printer.
Static checking
Type inference with unification, well-formedness checks, cross-reference resolution, EB0xx diagnostics, and advisory lints — emits Rodin .bcc / .bcm.
Command-line workflows
validate, import, export, fmt, and build subcommands. Text, JSON, and SARIF 2.1.0 output for CI and code-scanning.
Editor integration
A full Language Server: diagnostics, completion, hover, go-to-definition, rename, formatting, and semantic highlighting.
The .eventb text format.
Full syntax — contexts, machines, events, refinement, witnesses — in Unicode or ASCII. Pretty-print with configurable indentation; parse, transform, and print back to native Rodin XML.
MACHINE scheduler SEES scheduler_ctx VARIABLES waiting_tasks, running_tasks, completed_tasks INVARIANTS @inv2 running_tasks ∈ PROCESSORS ⇸ TASKS @inv4 waiting_tasks ∩ ran(running_tasks) = ∅ @inv7 card(dom(running_tasks)) ≤ card(PROCESSORS) EVENTS EVENT schedule_task ANY processor, task WHERE @grd1 processor ∈ PROCESSORS @grd3 task ∈ waiting_tasks @grd4 ∀t·t ∈ waiting_tasks ⇒ task_priority(task) ≥ task_priority(t) THEN waiting_tasks ≔ waiting_tasks ∖ {task} running_tasks(processor) ≔ task END END One tool, six subcommands.
rossi validate Validate .eventb files, Rodin .zip archives, or unzipped project dirs. rossi import Import Rodin .zip / .buc / .bum / dir into .eventb text. rossi export Export .eventb / .txt / dir into a Rodin .zip archive. rossi fmt Reformat in place — operator convention and indentation. rossi build Static-check a project and emit .bcc / .bcm checked XML. rossi lsp Run the language server over stdio. Install from crates.io.
Rossi is published to crates.io and installs with Cargo. A recent Rust toolchain is required.
# Command-line tool — installs the rossi binary cargo install rossi-cli # Language server — installs eventb-language-server cargo install eventb-lsp # Use the parser as a library cargo add rossi