I wrote an article on formally verifying functions in a wasm module with Lean.
It builds an execution model to prove properties of state transitions, and also checks that the Func derived from WAT matches the binary.
https://blog.habakan.com/post/2026-10-20-wasm-lean-proof/en
https://github.com/habakan/wat2lean
blog.habakan.comFormally Verifying WebAssembly Functions in LeanGenerative AI is making steady progress on mathematical research with Lean. Seeing that, I wondered—perhaps a little unc
commit 2ee7ca7