eventb

A Rust toolchain for Event-B: parser, static checker, CLI and Language Server (LSP) with Rodin round-tripping

Convert Event-B machines and contexts (.bum/.buc) to CamilleX plain-text models

Public part of the Event-B specification of the HIMACF model (formerly MROSL DP-model) — role-based access control for OS security

Agent Skill for writing, validating, and model-checking Event-B formal models with rossi and ProB.

Homebrew tap for the Event-B / B-method ecosystem — Rodin, Atelier B, ProB2-UI, EventBTool

Rodin platform bundle for Event-B — Rodin 3.10 with parallel proving, SMT solvers and the Proof Obligation Cleaner, prebuilt for Windows, Linux and macOS

Rodin plug-in that lets the Rossi Event-B language server drive a running Rodin: register and reveal projects, report unsaved model edits as they are typed, and reload open editors.

Template repository for text-first Event-B projects — Rossi validation, ProB model checking, Rodin round-tripping, vendored agent skill and CI out of the box

GitHub Action to check Event-B models with rossi — validate, format check and static build, with inline annotations and SARIF upload to code scanning

Headless toolchain to build, model-check and prove Rodin Event-B models from the command line — native or via Docker

Scoop bucket (Windows) for the Event-B / B-method tool ecosystem — Rodin, ProB and CLI tools

Command-line tool to animate Event-B models with ProB — random animation, invariant checking, trace replay (no Rodin required)

Fedora COPR RPM packaging for the Event-B / B-method ecosystem — Rodin, Atelier B, ProB and CLI tools

Gentoo ebuild overlay for Event-B / B-method tools — Rodin, ProB and more

APT repository (Debian/Ubuntu) for the Event-B / B-method ecosystem — Rodin, ProB, Atelier B and CLI tools

Command-line validator for Event-B models. Provides GitHub action.

Tree-sitter grammar for the Event-B formal language (.eventb textual syntax), generated from Rossi