[cyberclimb]

I just came across this project recently https://github.com/AeneasVerif/eurydice/ from Microsoft Azure Research (referenced here https://www.microsoft.com/en-us/research/blog/rewriting-symc...)

[rbanffy]

Fascinating. I wonder why they didn’t make it a LLVM backend, but, then, I guess it’s important for the C code to be readable as well.