Comment by mfornet

Initially we considered formalizing rust code, aeneas is a very promising project that would unlock a lot of features right way by transpiling to lean. However, we didn't want to lock ourselves to rust, so we decided to use a lower level target such that we could verify code from "any" language.

We considered LLVM-IR, and RISC-V.

Ultimately WASM felt like the right decisions. More importantly WASM spec is very well done in details, and it is written with formal verification in mind early on, and there are are plans from to include Lean as one of the targets for generating the spec automatically from SpecTec. Once this exist, we will formalize that our interpreter is correct under the definition generated from the official Wasm-Lean-Spec so we remove it from the Trusted-Base going forward.