You want to discuss about formal verification or ZK? Book a one hour call in my calendar. Open to anyone. The booking link: 👇

Wow! The College de France classes of Xavier Leroy (one of the fathers of formal verification) are about FHE, MPC, and ZK! Free, but only in French. The link: 👇

For example, a division that also gives you the remainder, forcing you to give it to someone, in particular, the admin. It seems a bit too simple, though.

Solving once and for all the rounding issues in smart contracts appears to have significant value, given recent exploits that have captured millions due to these "small" calculation errors. 💰 Can a better division simply solve the issue?

In Rust, there are two ways to do safe arithmetic: - Checked operations, returning `None` in case of an overflow - Saturating operations, returning the maximal value on overflow Checked operations are always correct, saturating operations never get stuck.

From "sorry my code is compiling" to "my agent is working"

Nice to see the new grants program, which was quickly updated since the last pause! ✨👀 Now, applications rely on RFPs, which is probably a result of a more mature ecosystem, and similar to the evolutions in other projects. An interesting RFP is "𝐈𝐧𝐭𝐞𝐠𝐫𝐚𝐭𝐢𝐧𝐠 𝐋𝐋𝐌𝐬 𝐢𝐧𝐭𝐨 𝐄𝐭𝐡𝐞𝐫𝐞𝐮𝐦 𝐏𝐫𝐨𝐭𝐨𝐜𝐨𝐥 𝐒𝐞𝐜𝐮𝐫𝐢𝐭𝐲 𝐑𝐞𝐬𝐞𝐚𝐫𝐜𝐡" which is about using the latest AI advances to audit and maintain the coherence of all the Ethereum proposals and implementations. As the complexity of a system grows over time, and since Ethereum has a policy of having multiple implementations for each component, it is becoming increasingly challenging to maintain coherence using standard approaches. One thing that interests us is the combination of code/spec translation with LLMs, combined with formal methods and testing, finding the right balance between precision and automation. We were discussing such a project today with @marc_lelarge for the case of Rust (ubiquitous now in Web3), but it could also work for Go or Python!

Here is one thing we like to formally verify on software: 𝒃𝒂𝒄𝒌𝒘𝒂𝒓𝒅 𝒄𝒐𝒎𝒑𝒂𝒕𝒊𝒃𝒊𝒍𝒊𝒕𝒚. What? This is about demonstrating that for any inputs, the new release of a system will behave exactly the same as the previous one (i.e., the same replies, same data stored in the database, etc.). Of course, depending on the case, there may be a list of exceptions, such as endpoints that have been changed or newly available features. Why? It is often very challenging to obtain an unambiguous specification of what a system is intended to do. Very often, apart from documents that give the general idea, the most precise answer is "it is supposed to do what it already does." In that sense, when we verify a new release of a product, we check that it does not break any existing user workflow that was possible with the current version. It also enables more aggressive optimizations, as even if the code becomes difficult to track, we are sure not to introduce any bugs. How? Generally, this verification is relatively straightforward, as most of the code remains unchanged once the software matures. Theorem provers are very good at checking equalities for parts that are identical and at highlighting all the points of difference. For these, we have to do the actual verification work, but we are sure not to miss any change. If the data model changes, we also need to write morphisms (aka migrations) to state that the code behaves the same, up to the data model changes. => If you are interested in ensuring the security of your blockchain system, talk to us! 📢

Making "coq-of-rust" much more usable is one of our big goals right now. 🦀 For now, handing each new code sample feels too much of a challenge. To be fair, most Rust code uses quite advanced features under the hood, even if not purposely.

Formal verification of zkVMs is crucial for trust in the Ethereum L1. But how can you make it scale to complex pre-compiles like Keccak? We are pleased to be completing our formal verification of the Keccak implementation in Plonky3. Here is our it works: 👇

On each major chain, DeFi protocols are often redeveloped from scratch, whereas their designs have already been battle-tested, rather than porting the code 1:1 (UniSwap port on Solana or Sui, for example). Do you know why?

Two reasons security audits might drastically change with AI: - AI can also do some (basic) auditing - It gets much easier to develop tooling to make some checks systematic ✅

With formal verification, you can design models/specifications to capture any known vulnerability kinds. But security researchers are the only explorers able to find new kinds of attacks.

Yesterday, there were two big milestones on zkVMs: - @ziskvm is verifying Eth blocks in real-time on 24 GPUs at a very low cost ($0.008) - @zksync is verifying at an even lower cost ($0.003), 3x slower but still very fast These benchmarks are hosted on @eth_proofs !

For smart contracts, the security focus seems to be on "my funds should not disappear without explicit request", like a transfer. 💸 This is still hard to specify. For more typical systems, having no runtime errors and backward compatibility with new releases seems good enough!

Formal verification is still much more time-consuming for a single audit, even with AI advancements. But where it really shines is for repeated audits, or when the code relies on subtle third-parties ✨️

From a discussion with someone specialized in automated theorem proving, SMTs are already a stack of various automated verification methods, ultimately with some SAT procedures at the base layer. There are many projects to connect them to interactive theorem provers. But the ultimate goal would be to integrate their algorithms directly in Rocq/Lean, as this would be much faster (discussions heard around Vampire and Z3). This might also mean that the demand for formal verification is increasing, at least the demand to verify more complex properties or to scale, with interactive theorem proving.

If you can show all your integers grow linearly with respect to the execution time, even for a very large constant, 2 to 1024 is so large that you are still always safe. With constant-size integers, you also keep real-time. Is something like that already done?

In critical embedded software, people spend a lot of time verifying for integer overflows and call it "safety", with formal verification methods such as abstract interpretation. What about using 1Ko integers, and heavy bounds given by the maximal execution time? 👇

A realization of being old: people asking how I could get the login "clarus" on GitHub 😀 (2010)