Regarding the "formal semantics", you are correct that different implementations of Statecharts have had different formal semantics, however some effort has bee

Regarding the "formal semantics", you are correct that different implementations of Statecharts have had different formal semantics, however some effort has been put toward standardization, the main one probably being the W3C SCXML standard, which specifies a pseudocode algorithm for execution of Statecharts: https://www.w3.org/TR/scxml/#AlgorithmforSCXMLInterpretation https://www.w3.org/TR/scxml/#AlgorithmforSCXMLInterpretation It also provides a test suite that implementations can use to check compliance: https://www.w3.org/Voice/2013/scxml-irp/ https://www.w3.org/Voice/2013/scxml-irp/ There are a number of conforming implementations in various programming languages.