You can send your emails of amazement and gratitude to Jared Davis and Magnus Myreen for that one. :)

https://www.cs.utexas.edu/~jared/milawa/Web/

They and their associates' work covers verified runtimes, HOL, extraction mechanisms, etc.

https://www.cl.cam.ac.uk/~mom22/research.html

Just port Milawa to run on multiple architectures with separate CPU's or implementations from multiple vendors. Include verified, VAMP processor on two FPGA's. Check Milawa itself then check the software in FOL until HOL is done. I have a paper somewhere on HOL-to-FOL converter, too. :)

Note: I've seen a bunch of things implemented in Prolog. I figure it could be modified to execute the program and produce an execution trace of its logic that could be run through Milawa. Not specialist enough to say. A prior, certified compiler for Pascal-like language was specified in Z shown equivalent to Prolog functions. So, there's potential here.