alt Hacker NewsHow 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?
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?