Comment by nickpsecurity

This is interesting work that I was just looking at by following-up on who funds CakeML: a mathematically-verified ML implementation. Led to Cerberus, ISA's models (including RISC-V), concurrency analysis, POSIX API models/testing... all sorts of stuff. One of those rare programs doing something at every layer of stack with theoretical and practical contributions. Check them out here:

https://www.cl.cam.ac.uk/~pes20/rems/

Cerberus main page and links are here:

https://www.cl.cam.ac.uk/~pes20/cerberus/

Work like this will eventually, if not already, be applied to other projects along the lines of CompCert, seL4, and static analysis. The models of real-world assembly and C come first. Then, other tools map C to assembly or specs to C. So, this is pretty fundamental stuff they're working on. That they try not to abstract away the dark corners is the real advance here as many try to cheat. :)

Note to ingve: One of those Jung-style coincidences that you submitted this around exact time I wrote up same project for Schneier's blog. I've only looked at it twice in its existence. Odds were slim we think & write around same time. Always find it interesting when that happens.