Transpiles Rust code to a functional program in Lean (demoura:cade:2015) to allow verification of Rust programs in Lean. Demonstrated on a binary search implementation.
The implementation is here.
Papers related to Simple verification of Rust programs via functional purification
- RustHorn: CHC-based verification for Rust programs [matsushita:esop:2020]