Formalising FRI: A Lean Blueprint of Security | Petar Maksimovic - Nevermind

Hi everyone, I'm Peter from Nethermind formal verification. I lead our ZK constraint verification team and I'm here to tell you some things about where the industry is at the moment when it comes to hardcore formal methods and what does it mean to formally verify the basic technologies that underpin Ethereum. This is going to be a slightly more technical talk than the previous ones, but I've tried to not go too deep into the actual mathematics, but anyways, let's see. So I think we're all aware that ZK is making its way slowly onto the blockchain and sort of in doing so what is the main idea? The main idea is to sort of have cryptographic proofs of transaction correctness done on the L2 and then the verifiers on L1 verify these cryptographic proofs.

Why is this good? Because this sort of type of verification is much much faster than what is sort of offered by let's say optimistic roll-ups. allows for a much higher throughput and it would give Ethereum a lot of scalability that it is looking for. Um, however, we do need to remember just how much funds Ethereum um sort of um holds and how important in that context it is to have security and basically the security of all of these assets that Ethereum holds rest on the correctness of these ZK cryptographic properties. provers, verifiers, and how do we guarantee that?

And at Nethermind, we believe that the only way to actually guarantee this is to have these properly formally verified. And sort of this is what we do. And our method of choice is interactive theorem proving in the lean theorem prover. What is lean? Lean is sort of a proof assistant that allows you to mechanize mathematics.

And then you can think of it as sort of a programming language that you can use to generate formally verified programs. It has this small trusted kernel that is often audited and reviewed by world's top mathematicians and computer scientists and it's come it's sort of you can think of it as like a shared standard of truth for mathematics and computer science. It comes with the largest repository of mechanized proofs that we have so far that's called mathlib and we use it sort of as a base to formally verify various web 3 technologies. What have we actually done so far? For example, we have verified several real world ZKVMs with succinct.

We verified SP1 hyper cube. We have recently worked with Axium to verify OpenVM and we're currently working with Brevis. More are in the line. With Matter Labs, we were the first to verify a property of a real world ZK verifier. And thanks to various grants from the Ethereum Foundation, we are currently mechanizing some cryptographic protocols that underpinsk such as Fry, Stir, and WR.

And I'll tell you a little bit more about our work on the Fry protocol. In that context, Fry underpins the a number of ZK proof systems. It effectively secures billions of dollars in transactions. It's used by Starware, risk zero, succinct, etc. Why is it good?

It's transparent. It does not need any sort of trusted setup. Just uses some hash functions. It is postquantum secure. Eventually, it gives you substantially more efficiency in what optimistic roll-ups have to offer and is quite flexible from a sort of a low-level mathematical point of view.

You can fine-tune it to be uh better for CPUs, better for GPUs, etc. So, a slight tour of what Fry actually is and some of the principles of ZK. So, how does ZK actually work? You have computation that you want to prove is valid and ZK through something called arithmetization allows you to take this computation and transform it into polomials and you get a very interesting guarantee. You get a guarantee that sort of if this computation is valid then these polomials that you get are of a low degree and if a prover tries to cheat in any way it will actually get polomials of higher degrees.

And now the Fry protocol gives you a mathematical mechanism for checking that this degree bound is not violated. meaning that that if I tell you if I give the fry protocol some information and it is able to check whether or not this information comes from a low degree polomial and basically when you bring arithmetization together which says that the computation is correct if the degree of the polinomial is low and if you connect it to fry which checks whether the polomial degree is actually low then you get the soundness of the fry protocol meaning that the cheating prover cannot pass the checks of the of the fry and so how it works in a very interesting mathematical way. So what do you do? You have some polomial at the prover and the provers large number of evaluations of this polomial and there is um so then with these large number of evaluations the fry protocol tests if these committed values are actually close to some polomial of a given degree. And what is really interesting there are there are results from coding theory that under certain conditions close is actually good enough.

Meaning that with overwhelming probability if you prove that something is close to something it is actually exactly that thing. And sort of in in a summary of what's going on, you have lowderee polomials that are kind of the language that we now use to encode correct computation. Fry spell checks this for you. It checks that what the prover gives you is sort of written in that language. And thanks to the mathematics and the algebraic structure of the encoding, there is no way for a cheating prover to get close enough without actually having to do the computation.

So what have we done at Nevermind? We have formalized a large sort of a substantial part of the coding theory like the mathematics in the lean proof assistant. We focused on the results that underpin the fry protocol. These are called read Solomon codes and some of the associated algorithms. We have implemented computable polomials in lean which was interesting because for a proof assistant of its maturity it was surprising to us that it wasn't able to sort of effectively compute polomials in real time.

We have given a blueprint from all the results from algebraic geometry that were not present in the in lean's math lib library that were needed for the soundness proof of fry. We blueprinted a number of results on proximity gaps required for the sadness results. These proximity gaps are sort of the things that tell you if I am close then I'm actually exact. We have fully formalized the fry protocol as well as the batched fry protocol in lean. So in theory the fry protocol works for just one polomial.

The batch fry works for a number of polomials. You just do a little something to them to combine them into one. In the beginning, we've blueprinted this batched soundness result and we have also as we were doing this, we have found an issue with the soundness proof of Fry that was currently believed to be true. And this basically is an EF grant that was given to us. And as the outcome of that we have the formalization of this Fry protocol that underpins a number of ZK technologies.

But what is missing are the proofs like the actual proofs. We have a blueprint and sort of the next thing that we do is to probably allow the community maybe through some sort of bounty program to complete these proofs in lean perhaps using AI. And actually there have been some auto formalization results u in the recent weeks that have tried to mechanize sort of this fixed soundness proof that we have. So then we will have in this proof assistant which we in this proof assistant we will have the formalized fry protocol with all the soundness proofs ready to work with it. Uh this should also be integrated soon into arclib which is the uh sort of the ethereum foundation thinks of arlib as the place for formalized cryptography and basically um based on this formalization of the fry protocol based on this future formalizations of the stern were protocols that are sort of advanced variants of fry that we will do in the coming months we can then use this as a base to start with the program analysis tools for example for Rust that we have to start actually formally verifying real world ZK verifiers that will live on the L1 and that would be sort of a it's it would be quite an unprecedented level of security to the ecosystem and with this I realized I have gone quite quickly this is the end of my talk we still have five minutes and thank you for your attention If you're interested in working with us, if you have some questions for us, come to me.

I'll be around. Come talk to us if you want stuff formally verified, you know.