There is a lot to unpack in your comment, thanks for commenting.

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.