Viewing profile — mfornet

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 a…

AI has been great so far filling in most of the proofs, and I'm trying to avoid SMT-style proofs early on, to make sure we have a solid API that can be scaled to arbitrary complex …

> Doesn't that put the Rust compiler (and its assert lowering) in the trusted base? Yes, but I would argue the are already in the trusted base before this project, we are not remov…

> Is the plan to build a new separation logic framework, or use e.g. iris-lean or splean as a base? We plan to build our own, though we are currently evaluating what is the current…

Both. 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…

Initially we considered formalizing rust code, aeneas is a very promising project that would unlock a lot of features right way by transpiling to lean. However, we didn't want to l…

> what if I want to reason about larger programs that dynamically allocate, where the addresses may not be known statically? How can I make sure these do not overlap? We are active…

At Cajal (YC W26) we’re excited to share Talos ( https://github.com/cajal-technologies/talos ), an open source framework for formal verification of WebAssembly modules in Lean. AI …

As I see it, this model will be able to predict “easy” to derive tokens but will no chance on “hard” tokens. For example doing a sum of random numbers. If the token you are trying …

off topic: Regarding Figure 8: "a graph with 10 nodes, each having 4 neighbors and no two shards requiring more than 2 hops for cross-shard communication". This can be achieved wit…