Rodin Handbook


2.2.5 Rodin

Rodin (3.1) is the name of the tool platform for Event-B. It allows formal Event-B models to be created with an editor. It generates proof obligations (3.2.7) that can be discharged either automatically or interactively.

Rodin is a modular software and many extensions are available. These include alternative editors, document generators, team support, and extensions (called plugins) some of which include support decomposition and records. An up-to-date list of plugins is maintained in the Rodin Wiki (1.1.2)1.


  1. These links were valid at the time of the writing of this document: