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.
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.