More on this - LLVM-IR has no official formal semantics and it's riddled with UB. RISC-V has a formal model in Sail, but it's an ISA so you throw away the structured control flow and types which we want for proving.…
I’m on the Cajal team - not OP, but happy to answer questions. The core bet is that Wasm is a good verification target (close to compiled artifacts, many languages target it), and Lean is the right place to do…
More on this - LLVM-IR has no official formal semantics and it's riddled with UB. RISC-V has a formal model in Sail, but it's an ISA so you throw away the structured control flow and types which we want for proving.…
I’m on the Cajal team - not OP, but happy to answer questions. The core bet is that Wasm is a good verification target (close to compiled artifacts, many languages target it), and Lean is the right place to do…