Why3 is used as a back-end prover in SafeCap. We also make available a Rodin plug in translating Event-B mathematical language to the Why3 notation. This experimental release contains support for Event-B mathematical language extensions, specifically for axiomatically defined operators.

Source code:uk.ac.ncl.eventb.why3

Update site (download and unzip locally, then choose “add local site” in installation dialog): uk.ac.ncl.eventb.why3-updatesite