Cool. I've been working on a compiler for a subset of Lean that targets WASM. The compiler is implemented in Lean.

https://github.com/jsmorph/leanexe

I think I managed to use Talos to prove the WAT generated from an example LeanExe program is correct. ?

https://gist.github.com/jsmorph/275a15dc21af037e1d02a1b433be...

Fun.