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.6) 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.
Footnotes