mfornet

6 ms·

1.
by mfornet 3mo ago
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 was
2.
by mfornet 3mo ago
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 code without increasing too much the cost of the verifi
3.
by mfornet 3mo ago
> 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 removing that. We want instead remove "your code&quo
4.
by mfornet 3mo ago
> 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 state of iris-lean. Thanks for pointing to splean, I was
5.
by mfornet 3mo ago
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 never traps. Part of our focus is making sure tha
6.
by mfornet 3mo ago
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 lock ourselves to rust, so we decided to use a lower lev
7.
by mfornet 3mo ago
> 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 actively working on this, as it is a pre-condition :P to reason
8.
Show HN: Talos – Open-source WASM interpreter for Lean(github.com)
106 points by mfornet 3mo ago|28 comments
9.
by mfornet 2y ago
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 to predict is not in the training data, even if similar patt
10.
by mfornet 7y ago
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 with only 3 neighbors (Petersen graph) https:/&