[IshKebab]

How do you actually prove it though? I understand if it's fully automated SMT-style proof, but doesn't Lean require tediously explicit proofs? If it doesn't prove automatically do you have to write out Lean helper proofs about the compiled WASM?

[mfornet]

AI has been great so far filling in most of the proofs, and I'm trying to avoid SMT-style proofs early on, to make sure we have a solid API that can be scaled to arbitrary complex code without increasing too much the cost of the verification. I'm sure nonetheless that SMT solvers will play a role going forward in filling up some proofs.

The reason AI has been so good at filling most of the proofs in my opinion, is that proofs are actually "simple", but very tedious and long. Part of our work right now is make sure that the tedious part can be solved mechanically as easy and efficient as possible, so both human or AI can focus on the interesting parts.