Have you seen CakeML[0]? It is verified that the semantics of the x86 machine code it outputs in the end are the same as the SML code it takes as input, up to o

Have you seen CakeML[0]? It is verified that the semantics of the x86 machine code it outputs in the end are the same as the SML code it takes as input, up to out-of-memory errors. [0]: https://cakeml.org/ https://cakeml.org/