EB2ALL

EB2ALL is a translation tool that automatically generates efficient target programming language code (C, C++, Java, C# and Solidity) from Event-B formal specification related to the analysis of complex problems. This tool is a collection of plug-ins named EB2C, EB2C++, EB2J, EB2C#, EB2Sol. The goal of EB2ALL is to be able to generate a verified source code that satisfies behavioral properties of the develop formal system. The translator checks syntax and type consistency before generating the target programming language code. The EB2ALL tool is developed as a set of plugins for RODIN development tool under the Eclipse framework. For downloading this tool, please visit [http://singh.perso.enseeiht.fr/eb2all/]. 

B2HLL 

Automatic translation of B models into High Level Language (HLL) (To be technology transfer by RATP)

TX2EB

Automatic translation of tabular expressions into Event-B models. Web Site : https://groke.cas.mcmaster.ca/gitlab/tables/jtet

EB2Algo

Correct-by-Construction Synthesis of Sequential Algorithms: EB2Algo

EB2Py

Correct-by-Construction Code Generation from Event-B to Python: EB2Py