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. Rossi lets you author Event-B as plain text and work with it from the command line and your editor.
Background: Event-B · wiki.event-b.org · ProB
pest-based parser and typed AST. Text ↔ native Rodin .buc / .bum / .zip XML, Unicode or ASCII operators, with a configurable pretty-printer.
Type inference with unification, well-formedness checks, cross-reference resolution, EB0xx diagnostics, and advisory lints — emits Rodin .bcc / .bcm.
validate, import, export, fmt, and build subcommands. Text, JSON, and SARIF 2.1.0 output for CI and code-scanning.
A full Language Server: diagnostics, completion, hover, go-to-definition, rename, formatting, and semantic highlighting.
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 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. Prebuilt packages for every major platform — or build from crates.io with Cargo.
scoop bucket add eventb https://github.com/eventb-rossi/scoop-eventb scoop install eventb/rossi brew tap eventb-rossi/tap brew install rossi # Ubuntu 26.04 "Resolute" or later curl -fsSL https://eventb-rossi.github.io/apt/KEY.gpg \ | sudo gpg --dearmor -o /etc/apt/keyrings/eventb.gpg echo "deb [signed-by=/etc/apt/keyrings/eventb.gpg] https://eventb-rossi.github.io/apt resolute main" \ | sudo tee /etc/apt/sources.list.d/eventb.list sudo apt update sudo apt install rossi sudo dnf copr enable @eventb-rossi/eventb-copr sudo dnf install rossi eselect repository eventb-rossi emaint sync -r eventb-rossi emerge -av rossi # 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 What Rossi is, how it reads and writes Event-B, and how to get it running.
More in the README →Rossi is an open-source Rust toolchain for the Event-B formal modeling language. It bundles a pest-based parser, a static checker with type inference, a command-line tool, and a full language server — letting you author Event-B as plain .eventb text and round-trip it through the Rodin platform.
Event-B is a formal method for system-level modeling and analysis. You describe a system as machines and contexts with invariants, then refine them step by step while discharging proof obligations. Rossi lets you write Event-B as plain text and work with it from the command line and your editor.
Rossi reads and writes .eventb, a plain-text format covering the full Event-B syntax — contexts, machines, events, refinement, and witnesses — in Unicode or ASCII operators. It parses the text into a typed AST, pretty-prints it back with configurable indentation, and converts to and from native Rodin .buc / .bum / .zip XML.
Yes. Rossi round-trips between .eventb text and native Rodin XML (.buc, .bum, and zipped projects). Import an existing Rodin project to text, edit it in any editor, then export it back to a Rodin .zip archive — so Rossi fits alongside the Rodin platform rather than replacing it.
Prebuilt packages are available for Windows (Scoop), macOS and Linux (Homebrew), Ubuntu (APT), Fedora (COPR), and Gentoo. On any platform with a recent Rust toolchain you can build from crates.io: run `cargo install rossi-cli` for the command-line tool and `cargo install eventb-lsp` for the language server.
Rossi ships eventb-lsp, a full Language Server providing diagnostics, completion, hover, go-to-definition, rename, formatting, and semantic highlighting. Any LSP-capable editor can use it; VS Code and Sublime Text are supported directly. One server powers every editor, so you get consistent Event-B tooling everywhere.
Yes. Rossi is free and open source, dual-licensed under MIT OR Apache-2.0, with development on GitHub at github.com/eventb-rossi/rossi. There is no paid tier — the parser, static checker, command-line tool, and language server are all available at no cost.