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