Rodin is an open tool platform for the cost effective rigorous development of dependable complex software systems and services. This platform is based on the event-B formal method and provides natural support for refinement and mathematical proof.
This platform contributes to the Eclipse framework and is extensible using the Eclipse plug-in mechanism.
Rodin development has been partly funded by the European Commission through two RTD projects:
More information about this platform can be found on the Event-B.org web site, including user and developer documentation available as a Wiki.
The development of this platform is hosted by SourceForge.
To improve your proof experience, please install the third-party provers from Atelier B. This is only a few mouse-clicks away. Please proceed as follow: