talos is already in use by <a href="https://github.com/siderolabs/talos" rel="nofollow">https://github.com/siderolabs/talos</a>, was confused for a second when I saw talos and wasm for a second, got excited about native wasm pod support.
I’m on the Cajal team - not OP, but happy to answer questions.<p>The 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.<p>Super interested in hearing from people working with Lean, compilers or other Wasm verification frameworks (eg Iris-Wasm).
Interesting. Do I have to write specs in Lean against the Wasm semantics or can you annotate Rust directly?
[flagged]