Show HN: Talos – Open-source WASM interpreter for Lean (github.com)
AI is now writing tons of the code that gets pushed to production. As code generation gets cheaper, verification becomes the bottleneck. We believe in a future where every piece of software comes with a mathematical proof that it does what its author intended - in doing so, eliminating many classes of exploits. Talos is part of the foundation for that.
Talos provides a Wasm interpreter optimized for reasoning at the binary level, together with a weakest-precondition calculus layer for proving properties about programs. Because we reason directly about WebAssembly, any language with a Wasm backend is in scope: Rust, C++, Go, C, Swift, Kotlin, Zig, C#, and many more.
To make this possible, we use Lean: a programming language and theorem prover that lets you both write software and mathematically prove that it's correct - all in one system. That's what lets Talos double as both an executable interpreter and the formal object Lean reasons about. Lean also integrates with modern AI proving tools, discharging goals automatically via both proof search and direct evaluation.
To see Talos in action check out a proof for Stein's GCD algorithm, implemented in the popular Rust crate num-integer: https://github.com/cajal-technologies/talos/blob/main/progra....
Our roadmap:
- Full Wasm coverage by first passing the official W3C testsuite, then later verifying against SpecTec (formal Wasm spec) - Arbitrary crate verification - any Rust crate that compiles to Wasm should be in scope - Building our proof library codelib, to make verifying increasingly complex programs tractable
We would love to hear the community’s feedback on Talos and comments on the state of formal verification right now. Contributions are also welcome!
19 comments
[ 3.3 ms ] story [ 48.8 ms ] threadThe core bet is that Wasm is a good verification target (close to compiled artifacts, many languages target it), and Lean is the right place to do verification.
Super interested in hearing from people working with Lean, compilers or other Wasm verification frameworks (eg Iris-Wasm).
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.
You can write "annotate" your rust code using asserts. On the wasm side asserts are converted to trap instructions, so the Lean spec will simply be: For every input this code never traps.
Part of our focus is making sure that specs are both easy to write and read, since they are human facing. Eventually you could imagine how writing code will mostly be writing specs, and both the code and the proofs will be handled by AI agents. In this scenario it is very important that humans can easily audit and modify the specs.
https://www.copyright.gov/help/faq/faq-protect.html
> Copyright does not protect names, titles, slogans, or short phrases. In some cases, these things may be protected as trademarks.
I'm also curious -- are you just implementing the Wasm binary and text parsing, validation algorithm, and execution semantics in Lean from scratch by reading the English prose in the spec document, and then checking it against the spec tests and the SpecTec description? Or do you have some sort of automated (classical or LLMy) transformation happening? (One could imagine directly transforming the SpecTec, or the OCaml reference interpreter, into Lean... but it sounds like you're not doing that? I think one needs to be a little careful here because e.g. at this point some of the English prose and reference interpreter implementation, and I think maybe some of the tests, are autogenerated from the SpecTec.) Which parts (if any) are outside the scope of the formalization? E.g. for WasmCert-Isabelle, I believe the binary and definitely the text parsing, and I think some of the arithmetic ops, are not covered.
How are you modeling the explicit sources of nondeterminism in the Wasm execution semantics? E.g. NaN representation, {memory., table.}grow, host calls, stack exhaustion, relaxed SIMD instructions, etc., and that's all before we get to the threads proposal? Because if the goal is to prove programs correct, one risk is that I prove my program correct against your Wasm interpreter (which maybe makes certain choices that aren't determined by the spec), and then I run it against another fully-conforming interpreter in the wild and it behaves incorrectly.
We are heavily using LLMs and agents for writing and verifying all the code. We have some safeguard inplace, such as not breaking the wasm testsuite, and being able to run wasm code and produce the correct results (even if that is not the goal of this interpreter). There is an ongoing effort (not by us) about creating a formal WASM spec in lean, generated from SpecTec, when that lands our plan is to prove that our interpreter follow the specification.
> E.g. are you able to do an "in-place Store" like WasmRef-Isabelle, and can you represent memories and tables as plain vectors of bytes/refs in memory, can you grow them in-place, etc.? Or any other optimizations/lessons learned?
Even if the interpreter can be use to run wasm code, we don't really care about efficiency, it is not intended to run WASM, but instead to be able to verify code, so we are intentionally not building an optimized interpreter, or rather we are optimizing toward ease of demonstration.
> How are you modeling the explicit sources of nondeterminism in the Wasm execution semantics? E.g. NaN representation, {memory., table.}grow, host calls, stack exhaustion, relaxed SIMD instructions, etc.,
Going over your list, some functions that might fail, like {memory., table.}grow and stack exhaustion can't fail on our interpreter, so that transition is not represented here. We need to revisit this hypothesis, but part of the reasoning is that we all properties we prove about the WASM bytecode, are properties held by the original code, and usually (for example in lean) you can prove that a function has some property for all values of a natural number, even if you can't really run the function for all values due to some kind of "system" failure (stack overflow).
NaN, we certainly need to revisit floats, we are delegaing its behaviour to Lean floats. Again part of why we think this might work is because we are not planning to run code with this interpreter, but just to write proofs.
Host calls is properly modeled and being developed as we speak, since we really care about being able to proofs properties of a code that runs on some particular host. When you write a statement about some code, you do it on the presence of some particular host. I'm exploring the possibility of formalizing NEAR smart contracts, which are WASM binaries.
Actually i think it's the "for" in the title that's at fault. The repo title is quite clear, but the submission title is ambiguous to me.