Talos - Open-source WASM interpreter for Lean

Talos 是一个用 Lean 做 WebAssembly 模块形式化验证的开源框架。项目方把背景放在 AI 生成代码越来越多的场景里，认为代码生成变便宜后，verification 会成为瓶颈。它把 WASM interpreter 和证明环境放在一起，使模块行为可以在形式化系统中分析，而不是只依赖测试或沙箱隔离。