This project uses one-way translation of Rust code into WhyML through Creusot. This translation is not formally guaranteed to be correct or semantics-preserving.

Ideally, the code produced by Creusot should be translated back to Rust by a tool from Creusot or someone else. This way it is possible to use fixed point iteration, just like AST pretty-printer and parser for programming language syntax.

This is more or less an approach taken by verification team of Buran (USSR's space shuttle) software. They took Fortran code and compiled it into executable code. The executable code was then manually translated back into Fortran and discrepancies analyzed. This way they found several errors in Fortran compiler. Buran made fully automatic landing in late 80-s.

Contemporary verifiers should do the same automatically.