👉 We secure your critical code using Formal Verification, to make sure even recent AI attacks cannot get through 👉 We educate around FV to make this technology available to everyone (presentations, posts) 👉 We verify code at the source level (most precise) using interactive provers (Rocq, most expressive) Projects made: - "rocq-of-rust" to verify optimized Rust code; Revm verification (grant from @ethereumfndn) - "rocq-of-solidity" to verify Solidity code, at the Yul level - "Garden" framework to verify ZK circuits (grant from @ethereumfndn) - FV of part of the Tezos nodes (100,000 lines of OCaml, around 20% covered) - "Excalead" for lightweight verification of Solana code with AI

The ban of Fable is a strong reminder that, in software, the moat is security.

Formal verification is spreading like fire 🔥 both in the Ethereum and Solana communities!

How is AI changing formal verification? It drastically reduces the cost of writing specifications, and proving them correct.

👀 There is always one more way to find bugs.

We at Protocol Snarkification - me and @alexanderlhicks, plus about 30 or so external collaborators - are working hard with formal verification to ship the highest-assurance zkVMs possible. (see end of thread for collaborators) (1/n)

Formal verification is a critical tool to protect protocols from vulnerabilities. The recent Zcash vulnerability with honest disclosure is a reminder of that. FV is the technology we focus on at @FormalLand to secure protocols. Being 💯 focused enables us to create unique capabilities, some that we keep closed-source: - FV on arbitrary circuit languages, without having to change one's implementation, using our Garden 🍀 framework. Verifying the code as it is very important to keep stacking security layers on the same code without having to re-implement things. Example: verification the optimized Keccak circuit in Plonky3, the main hash function of Ethereum. - FV on Rust code 🦀 at the implementation level, without modifying the Rust code and for arbitrarily large properties. This is still something that open tooling struggle with, constraining the way the Rust code should be written. We believe code should be verified as it is, otherwise optimizations are lost and it becomes harder to combine tooling. We have a demo of that for Revm an EVM interpreter in Rust. - FV for the Ethereum infra and Soldity smart contracts: this is ongoing development and behind closed doors. - General belief of combining different approaches to not depend on a unique stack and take different angles. We bet heavily on the Rocq prover for that, with some work in Lean as well like a recent verification of polynomial algorithms for ZK with it. The two provers can in addition be connected. Happy to chat more about that 🤝 to help teams secure their code even more, covering the whole stack with FV! 🛡️

We continue building more tooling for the formal verification of Solidity code, as: - Most smart contracts are in this language - Not much tooling exist yet in the domain of interactive theorem provers, like Rocq or Lean A lot of the code is not public. DM to test!

Our mission: making sure your Web3 stack is secure against the next Mythos model. Thanks formal methods.

A main reason why it is better to approach security from different angles: because the attacker will do, and each angle reveal different vulnerabilities. => Make sure to formally verify your code, down to the assembly level, before others do.

OpenZeppelin has never been going that far on the formal verification side. But this is the asymmetry favoring the defender, as math cover infinite amount of cases.

We continue building our tooling to provide more extensive formal verification for EVM smart contracts. Of course there are many moving parts, but extending the scope is a way to capture more subtle bugs, and sooner!

We have been advertising formal verification as a strong solution for Web3 security since 2021, focusing at 100%. It is finally going mainstream!

The kind of message I like to receive!

Vitalik: "After all, a computer program is a mathematical object, and so proving that a computer program behaves in a certain way is a mathematical theorem." This is the key insight of formal verification to enable verifying code for any inputs.