Right now I'm only doing very small simple functions. Kani[0] takes care of translating the code to an intermediate representation for me. It converts the Rust code and C code into a GOTO program[1] which verifiers can then run on top of

[0] https://github.com/model-checking/kani

[1] https://model-checking.github.io/cbmc-training/cbmc/overview...