Thanks!

I tried several approaches to support both C and Rust. I tried using LLVM bytecode, but that ended up being way too low-level. The proofs ended up being gargantuan.

I also tried converting CBMC's intermediate representation, "GOTO Programs" to Lean. This seemed worth a shot because CMBC supports C and Kani adds support for Rust. Unfortunately, Kani's Rust-to-GOTO conversion caused a massive blow-up in code size.

What I ended up doing was converting both GOTO Programs and MIR (Rust's IR) to my own custom IR. The IR is low-level enough to convert both languages, but high-level enough to keep the code relatively concise. I then run simplification passes over the IR and compile it to Lean.