The most developed one I know of is Atelier B [0], which uses the B-Method and has a C code generator. I believe this was the tool used to develop several drive

The most developed one I know of is Atelier B [0], which uses the B-Method and has a C code generator. I believe this was the tool used to develop several driverless train control systems in the Paris Metro and other subways. There is a free version but unfortunately it is not open source. [0] https://www.atelierb.eu/en/ https://www.atelierb.eu/en/