Formal Land 🌲

@levs57 Yes indeed, including full verification of both options, monolithic EVM should be shorter! An advantage of Rust verification is that it can be reused for other projects.

@FormalLand So, the question is whether it is easier to verify monolithic evm impl in circuits, or an optimizing compiler of Rust? 😅😅😅 Idk, llvm is 10m+ loc, I think verifying monolithic evm is better shot :D

Here is our proposal to make end-to-end formally verified zkEVMs for the next version of Ethereum. Gain Between 2x and 4x more TPS (more at the end), unlocking a huge utility increase. 🏁 Why? End-to-end formal verification is needed as security issues in ZK proofs are hard to track and can be catastrophic given the value at stake (several billion dollars on the Ethereum mainnet). Scope The EVM implementations, like Revm, with a correctness proof down to the RISC-V compiled assembly code of the interpreters. We do not cover the formal verification of the circuits and cryptographic primitives here. What exists For now, there is a verified translation from the core of the Revm implementation to the formal language Rocq through "rocq-of-rust" (our work), and a compilation pipeline, Peregrine, built on top of CompCert, to compile an EVM interpreter in Rocq to RISC-V in a formally verified way. These projects are either done or in active progress. Limitations The main limitations of relying on an EVM written in Rocq (or any formal language) are: - Speed. This is hard to beat an imperative language like Rust with a mature optimizing toolchain like LLVM. - Diversity. Leveraging existing EVM interpreters brings battle-tested solutions and enhances security through implementation diversity. Proposition Making a pipeline to compile (a subset of) Rust programs down to assembly code. This is a huge project. We also need to be able to reason on the semantics of Rust that we compile to show it is equivalent to other EVM implementations (something that "rocq-of-rust" provides for some parts). There are some ingredients to make it manageable, including AI, certifying compilation rather than certified compilation, and using a simpler Rust backend than LLVM to start with, such as CompCert. Computing the gains We estimate that, compared to an EVM implementation in a formal language (Rocq or Lean), switching to a language with explicit memory management, such as Rust, should yield a 2x performance improvement. Going all the way with LLVM verification, we get an additional 2x compared to using optimization in the formally verified C compiler CompCert. So, there is between 2x and 4x improvement based on these estimates. We assume there needs to be at least one zkVM that is formally verified end-to-end to validate each block. Thanks for reading through. Happy to discuss or collaborate on this project! 🚀

@thisvishalsingh Thanks.

@FormalLand Great work 👏

@TechLayoffLover This will require increased testing and security so that the system does not fall apart.

Atlassian just confirmed 1,600 layoffs with 900+ coming from engineering But I'm hearing the real story from inside Sources say they've been running "knowledge extraction sprints" for 6 months - recording every senior engineer's screen, logging their prompts, documenting their debugging workflows One architect told me they made him walk through his entire microservices decision tree while they filmed it. Called it "knowledge transfer for the transition team" The transition team? 47 contractors in Bangalore with access to his recorded sessions and a Claude Enterprise subscription Same architect just found out his replacement starts Monday. Guy makes $28k annually and ships code 40% faster using the exact prompt libraries they extracted They're not just cutting headcount - they're systematizing 15 years of engineering expertise into training data The "strategic AI focus" isn't about building AI products It's about replacing their entire engineering culture with agents trained on their senior engineers' knowledge Word is the CTO replacement already has the playbook: extract, document, offshore, automate If you're still there and they ask you to "document your processes for the team" - RUN The knowledge extraction is complete

Most of these tools tend to be moving targets/WIP, so a definite answer is difficult. In theory, RefinedRust should be the simplest to use and less expressive, and "rocq-of-rust" the most expressive, especially with respect to code coverage, but also more complex. Note that we are a service company, so if you can pay for a corresponding bill, everything will be done by our side, making "rocq-of-rust" more or less automated!

im still not sure what the difference between rocq-of-rust, RefinedRust, and Aeneas is -- or which one I should devote my time to if I had to pick one and only one

The links to the slides: formal.land/slides/rocq-of… Happy for any remarks!

In this new video 📽️, we show how the "rocq-of-rust" transpiler is implemented in Rust, with: - A high-level view of the Rust compiler's APIs and intermediate languages, in particular THIR. - The small transformations + pretty-printing for a readable output.

The TG group link: t.me/+DIZFX3D0SAM1M…

"Code is Law" only works if the code is correct. ⚖️✨ We are launching our Telegram group to discuss Formal Verification techniques for Web3 security and beyond! To discuss, the link is below 👇

We build formal verification solutions for: - Rust: used for the implementation of many building blocks of Ethereum, - ZK circuits: to be used for Lean Ethereum, - Solidity: as used by most smart contracts. Our latest project: a formalization of the core of Revm: formal.land/reports/2026-0… , with the aim of providing a very precise specification of the EVM and bringing greater safety to Revm.

What are you building to make Ethereum safer? Share it in the comments ↓

Here is a video that presents how formal verification works in more detail for the Rust language. The first step is to translate into a formal language using the tool "rocq-of-rust" that we built. We will continue publishing more videos to make it more approachable. 📽️

It is often good to repeat goals so as not to forget about them. Our two goals for the year: - Formally verify one large open-source project. - Have the technology to verify large-scale vibe-coded software, for functional code and simple properties at least.

The link to the article: formal.land/blog/2026/02/2…

A new blog post where we summarize our work to verify a formal specification of Revm, the main Rust virtual machine for EVM (smart contracts) in Rocq (link below 👇) In short: - This is a first step to bring more security to EVM implementations with interactive theorem provers. - We do not need to modify the Revm source code, showing that this is applicable to a large variety of Rust code, preserving all optimizations. - We cover 94% of the instructions. - The translation techniques are not very specific to Rust and can be applied to any imperative programming language. - As in most software projects today, AI use was critical to reach completion.

In this video 📹, we show how the translation from the Rust language to the proof system Rocq works, applied to an example from Revm. This is important to help ensure Rust programs are correctly implemented using formal verification.

1/ Exploring Lean Ethereum: A vision for a future-proof, post-quantum L1. In a recent @zeroknowledgefm episode by @nico_mnbl, @drakefjustin outlines the C-D-E framework (Consensus, Data, Execution) to streamline Ethereum’s core using enshrine ZK and post-quantum crypto.🧵

@toly The link to the report: formal.land/reports/2026-0…

Yes. This is not us telling it, this is @toly Fortunately, we now have made "rocq-of-rust" to formally verify large Rust programs with interactive theorem provers like Rocq and Lean. We have a verified functional specification on about 4,000 lines of Rust for the EVM 👇

@ysu_ChatData Thanks. For unsafe blocks, for now we assume that it is memory safe! And then handle it in the same way as safe blocks. For FFI, we make a functional specification of the external functional and assume it to be correct.

Very cool direction. Deep embedding from THIR plus an equivalence proof to a shallow embedding sounds like a practical bridge between fidelity and ergonomics. How do you handle modeling of unsafe blocks and external FFI boundaries, and do you have a plan to integrate the translation and proof obligations into CI for large crates?

Today, translating general Rust code to formal languages such as Rocq or Lean is practically working with "rocq-of-rust". By general Rust code, we mean arbitrary safe Rust, or "safe" unsafe Rust (for now). This means that one can take a Rust program and translate it into a formal language, preserving the source code as is, along with all the optimizations, which are often critical in Rust projects. As a result, you can formally verify any security properties and business rules, including for complex cryptographic libraries or programs with many external dependencies, for example. One example is our ongoing verification project for Revm, a Rust implementation of the Ethereum virtual machine designed, among other things, to run on future zkVMs where security is critical. How is the "rocq-of-rust" approach unique? We do a 𝒅𝒆𝒆𝒑 𝒆𝒎𝒃𝒆𝒅𝒅𝒊𝒏𝒈 of the Rust language in Rocq (from THIR level). This means taking the syntax tree type from the Rust compiler and implementing it on the Rocq side (without extra information like line numbers), with semantic rules to evaluate each node. As this translation is very "one-to-one", it can import a large amount of Rust code, like the "core" library or most programs we tried it on. For formal verification, the simplest representation is 𝒔𝒉𝒂𝒍𝒍𝒐𝒘 𝒆𝒎𝒃𝒆𝒅𝒅𝒊𝒏𝒈. So here comes the second step: we provide a proof framework to show the equivalence between the deep embedding and a shallow embedding. This step heavily relies on automation and AI and is safe because formally verified. As of today, the translation speed to shallow embedding is about "one file per day" (very rough estimate), which we think is acceptable compared to the time spent verifying each file to prove typical specifications. As a bonus, we do not rely on the borrow checker, even if it helps to have structured Rust programs as inputs. So this means this approach should work as well for C or Go code. We believe the use of a "deep-embedding + automation with AI to a shallow-embedding" is an interesting new combination for translating complex imperative code into formal languages, with both wide support for inputs and high-level outputs for complex verifications. Note that this work is still in progress, and we welcome any remarks/fixes. For Lean users, the last translation step from Rocq to Lean can be done through an extraction mechanism, given that the two languages are very similar on the computational part (straightforward, but to be implemented), or using "rocq-lean-import", which works much better than its humble README suggests, especially for computations. We are happy to discuss with you if you have large Rust code that you want to secure with the largest possible scope. Below is a link to the work on Revm 👇