Ethproofs Call #9: Formal Verification

Transcript

Okay, let's get started. Hello and welcome everyone to E Proof call number nine. Uh the topic of today's call is formal verification. This is a long overdue call um and it's going to be uh led for the most part by Alex Hicks um who will be taking over very very soon. But I do have a a few slides that I want to share uh super quickly. >> [snorts] >> Just going to mute a few people uh to prevent the echo.

Um so one is that I'm very excited about formal verification since uh a few weeks, not only for security but also for for performance. Um we have projects like EVM ASM where once we have the end-to-end formal verification, we can really start grinding on on performance. Uh we have something like the proximity gas results where you know, we have an initial result, we have conjectures, and we can incrementally work towards uh better performance. And just generally speaking, it seems like auto research is is taking over the world and uh formal verification is a uh match made in in heaven.

If you are new to the E Proof calls, there is a Telegram group. This is the link eproofs_community. Uh and there's also a uh a QR code uh just to make it uh slightly easier for for you to join. Uh there's about 600 people there and you know, we try to to keep it relatively uh high signal in that group. Um so this is uh the the historical calendar of E Proof calls. Uh we've had 11 of them, like two B calls. and the next call will be on uh August 15th uh dedicated to binary fields. So if you've been on Twitter uh recently,

there's this new proof system uh called Flock, which is based on binary fields. It's really, really exciting because it has similar performance on proving hashes relative to prime fields that use ZK-friendly hashes like Poseidon. So, it would be potentially a way to use a traditional hash function like Blake or SHA-2 or SHA-3 and have higher security overall. So, that's going to be the topic of the next call. And yeah, I just want to hand it over to Alex X.

>> Yeah, thank you. I think we'll get straight into the talks because we have many of them and because these calls always overrun. But yeah, we'll basically cover a couple different topics. Most of these are ZK-EVM related and people will be aware of the kind of verified ZK-EVM effort. So, this will cover ZK-EVM circuits and verification, cryptography, compilers, the EVM, and work on verifying EVM. But then we'll have a bit at the end that's all about smart contracts since there's been some exciting work there. And I think we can basically try to start the talks as soon as possible. So, Shoki, if you're ready, the floor is yours.

>> Sure. Let me share my screen. Oops. Okay. Everyone, here's a Shoki from Mix Foundation. So, today I'm going to be talking about our formally verified Ring Constant Client. So, our goal is to eliminate drift between specification and implementations. We're using the Ring as a back end, which formally verifies the consensus logic. This design is inspired by Cardano. They have a Haskell client, which back end is implemented in Agda.

So, here is a sketchy uh architecture. We prove the kind of state transition and the fork choices. And here is the consensus logic. You may know it's so important part. And as you may know, we can run the compiler in Lean, uh which introduce uh C program. So, we can binding with any other C API languages like Rust or Go. So, we using the Rust as a runtime, uh which has a bunch of side effects uh like a networking or uh storages as well.

So, here is a state transition benchmark. Uh we can benchmark the assuming 4,096 validator defined in Lean spec. As you can see, uh the result are lower than SOL in Lean spec. I'm sorry. I guess this 200 ms is uh not uh not correct. It's I guess 800. Anyway, uh so we believe that means that this suitable for practice use. However, we should concern about FFI in top of the performance. So, in real case, we should assume the uh total

number of validator would be 1 million. So, this uh this number is not enough, I guess. Also, Lean and the Rust has their own memory system uh memory system or interfaces. So, we should concern about these topics. So, uh however, uh so our goal is not implement just basic client, but also uh commit for uh Lean consensus and any other client team. Currently, Lean spec is implemented in Python. However, we should re-implement water and translation between auto link constant respect in ring.

And we can use our assets for implemented is any other CV clients. Uh yeah. That's and we have a lot of works. One thing is a formal inspect. As I mentioned before, this link constant respect part. Also, we tried to formal verification to prove safety and liveness for goldfish or Simplex, you know, which is a part of the couple consensuses. And we here is a POC for running a DGB and PS program in ring.

If you interact with our client team, you can scan this QR code. Yeah, thank you. That's it. >> Thank you very much. Do we have any quick single question maybe whilst we switch over to Julian next? And then Julian, if you want to start sharing. >> Uh it's Peter actually giving this >> Julian because >> Yeah, yeah, the Peter is actually giving this talk. Sorry, please. >> Yes, so I think well, I will send a request for sharing because >> Um can you try again?

>> It is fine, yes. Now it is fine. And now you should be able to see this. And now it might even be full screen. >> Yes. >> It is. All right. Off to you. >> Okay. So, Peter from from yeah, hi. Hi everyone, I'm Peter from 9 Mile Security and I'm going to talk to you briefly about our work on formal verification of various Plonky3 based risk five ZKVMs. So, what have we actually done? We have verified upcode soundness for a number of risk 5 ZKVMs against the official risk 5 specification that has been

extracted to lean as part of an EF-funded effort by Galois and the labs, people in Cambridge, etc. And so, sort of the statements that we prove are of the form if the extracted constraints hold, then the chip that represents a specific risk 5 upcode actually models this upcode behavior correctly. And we prove that there is an equivalence between this upcode behavior as per the ZKVM and the upcode behavior as per the risk 5 specification.

We have done this initially for SP1 Hypercube together with Succinct, and I think there will be more to work on more work on that uh later on where we verified 64-bit SP1 Hypercube. And then we've continued on around to verify the 32-bit version of OpenVM per Axiom. And our latest project is the verification of both 32-bit and 64-bit Pico for Brevis. the Succinct Labs and Axiom verifications are open source. The Brevis one will be open source the moment Alex says it is okay.

>> It's okay. I proved it yesterday. >> Then it will be open source very >> [laughter] >> very shortly. And sort of as as a bonus of all of this um uh development, we have built sort of on top of the official risk 5 specification a very simple characterization of the behavior of risk 5 upcodes in terms of only a few basic operations, and that means that uh for like future proofs against of of correctness against the risk five spec, all that one needs to show is that basically whatever it is they are doing behaves sort of emits an equivalent like version of these operations. And these

operations are very simple like read register, write register, read memory, write memory. And that's it abstracts the uh a lot of the gory detail of the risk five spec. And sort of not quite separately from that, but kind of in parallel, we were developing with the help of another EF grant uh CertiPlonk, which is which was meant to be a framework for general reasoning about Plonky3 circuits, where we've created some sort of reusable infrastructure that allows us to extract constraint systems from Plonky3, and we are still working towards figuring out what would be a unifying interface for sort of

extracting information about lookup, permutation, memory arguments. So, and some of the work done in CertiPlonk is kind of in the verification of ZKVMs that we have done and vice versa as these projects were kind of intertwined. But uh yes, so this is sort of what I have. >> Thank you. Great. Thank you very much. Uh and yet there's a There's a hour-long talk about the Axiom and previous work that people can find on YouTube. I'll put a link to the YouTube channel past this uh towards the end of the session or someone can put it in the chat now.

>> Excellent. >> And then yeah, after this we've got uh James uh from O(1) Labs who will talk a bit about ZK-LIM. >> Mark, still sharing? Can y'all see this? >> Okay.

Um yeah, so I'll be talking about ZK-Lean. Uh this is joint work with some of my colleagues at Galois um as well as Lisa and Pearl. Um there's a link to the repo, so it's open source. Uh if you want to check it out. So um yeah, I guess the goal of ZK-Lean is that we want to formally verify the correctness of ZK statements. So that the approach we took is uh building ZK-Lean, which is a Lean 4 library and that allows you to uh easily uh and nicely encode ZK statements.

So the language uh as supports many ZK features that you would want, such as a Groth16, arithmetic constraints, lookup tables, MLE-based [clears throat] lookup tables, and RAM. So like uh there's like a very simple example of like what a circuit looks like in ZK-Lean. So here you you know, you have a Lean function that's uh witnessing a new uh circuit variable. And then it constrains it to be 0 or 1 by uh having this uh expression x * x - 1 = 0. yeah, and we we we put in a lot of work to make it composable, so you can say that we have this like ZK builder monad.

It's also abstract over the field. Um and um yeah, it's also agnostic to the back end uh proving system. So we have uh a lot of integration built into ZK-Lean to integrate it with other projects that you might want to actually uh verify properties about. Um so one thing we did is we built a custom extraction from Jolt. So we have uh we have a system that automatically extracts all the lookup tables in Jolt. It will uh extract it into ZK-Lean. And then from there we're actually able to like verify all the lookup tables. So basically like all the instructions and all the opcodes for the 32 uh uh risk five instructions in total.

the other thing we've done, which is more automated and hopefully will be more useful for other uh projects if they want to use it, is uh we've we've built a LZ K back end. So, on the right-hand side, you can kind of see this diagram of of what the architecture of LZ K looks like. So, you have a bunch of front ends that produce uh ZK statements. And then you have a bunch of back ends that consume uh ZK statements and do different things like witness generation. So, we've implemented a front end, so that means like if you have your circuit written in ZK lean, you can give it to LZ K, and then LZ K will output all these different representations.

And then we've also implemented a back end where you can take your say your circuit's written in Circom or SP1, give it to LZ K, and then just look then uh LZ K will output the ZK lean itself, and then you can uh start doing your verification on your statements. So, uh I'll just go over a quick case study that we did. So, this is verifying uh Keccak. So, on the left-hand side, you can see kind of uh a short excerpt of what the Keccak implementation looks like in ZK lean.

You have your state at the top where you have all your lanes, and they're all uh field expressions. And then at the bottom, you can see you have this monadic uh round function, which is one round of Keccak, where first you and then you call the sub functions of theta, rho, pi, and iota, which are all the pieces of a Keccak round. And then on the right-hand side, this is the actual statement of soundness for for this function. Uh basically, you have these four triples, which allow you to define pre-conditions and post-conditions. And basically, this is saying that um the the circuit implementation over field elements matches the bit vector representation.

and then you can see the proof is uh pretty nice and compositional. All you need to do is you can call um basically sub lemmas for each of the the sub components. So, you can see we're calling uh the statement on this uh lemma to uh to uh do this proof. Um yeah, so that's it. Happy to take questions. >> Thank you. And so, Lisa is going to follow up with some work that's related to this. Uh so, while she's setting up before that, I have a question for James. Uh feel free. And then, obviously, ZK will have its own little talk later on.

Uh and if not, then you can go ahead, Lisa. >> Right. Uh I can you see my slides? >> Yep. All right. So, I'm Lisa. I'm a fourth-year PhD student at Stanford University, and today I'll be talking about Bit Mod Q, which is a tactic in Lean for automating verification of zero-knowledge proof arithmetizations in Lean, and is a tactic that we built while I was an internship at Galois. So, um as James talked about like ZK Lean, we want to verify ZK VMs. And one of the issues when we go to verify the arithmetizations is that we really struggle to verify that the bit vector and finite field encodings actually match. So, what I mean by this is when we look at the Joel polynomial polynomial encoding of a bitwise or over a finite field, we might have something like this where we have a BVR of two bit

vectors. And then, we want to show that the field representation using bits uh that using elements in the field that represent bits actually matches. And so, the issue is existing automation both in Lean and SMT fails. In Lean, it fails cuz there's a lot a lot of tactics that reason about two types. And then, in SMT, we have theory combination, which doesn't one not all of the decision procedures produce proofs. And then, two in theory combination, the encodings are so tightly coupled, but it's hard to solve the problem. And so, the insights that we had by looking at arithmetizations is that they don't often contain finite field reasoning. So, there's no inverses or zero divisors, which means we can actually translate to bit vectors and then use existing bit vector procedures.

And additionally, if we have a good range analysis module, we can give smaller bit widths, which means that our decision procedures for bit vectors will be more efficient. So, we did exactly this. We designed a pipeline to translate from finite fields and bit vectors to bit vectors and our own custom analysis range module. So, we have a two-end pipeline that uses range analysis to apply different rules and that translates to natural number and bit vectors with natural numbers as an intermediary representation in Lean. And then we translate it to bit vectors and then we bit blast. And this tells us if our mathematization is sound or not sound.

So, we analyzed on both Jolt and SerC. And what we saw is that one in Lean, there's absolutely like there's not even anything to compare to. But for SMT, we do a lot better than them on more complex mathematizations, which are the ones used in practice. And so this project, we also found two bugs. One was in the Jolt Lean extractor and the other one was in the SerC compiler itself, which had some issues with rust overflow semantics. And further, this project has been integrated into ZK Lean and was also accepted as a paper to CAV 2026. So, if you're dealing with a lot of bit vectors and finite fields, potentially this tactic could be helpful for you.

That is all I have, if anyone has any >> All right. >> Thank you very much. Uh congrats on the paper. Uh so, I'll switch over. I guess I'll screen share for Kroger's presentation. If anyone wants to quickly unmute and ask a question whilst I do that, feel free. >> Jonathan, very nice work. Uh do you have a connection to uh SMT SMT Lean? I don't know what the status of the project is, but it's a yeah. >> Yeah, it's produced by my lab and we just actually submitted a paper with finite fields proofs, so now it should support finite fields, which is kind of cool.

>> Nice. All right, so I've got my screen share. I've got Google slides and so the floor is yours, Gregor. >> Boom. Um yeah, hey. Hello everyone. I'm I'm Gregor from Cega Security. Um I'll be presenting Clean, which is our framework for verifying circuits in Lean, which I was supported for a long time by by an EF grant. and now it's developing um it's developing on its on its own on various fronts.

Um so I think the best way to to convey what it is and how it's useful is is uh is this uh code snippet. So so Clean is is in the to trying to do something um similar to maybe a CegaLena and CertiK that we heard about earlier. So it's um it has a DSL in Lean to express circuits. So if you if you look at the at the code, there there is a definition is zero and it has this main field, which is the actual circuit implementation.

so it's it's a classical circuit is that computes the uh Boolean that says whether whether an element is zero. So you you have a witness command >> [clears throat] >> that that creates this um inverse of X, then you have this constrain uh equal command that creates B, which is the Boolean return value, and then the final constraint. So in in total you have two arithmetic like constraints here.

or two two arithmetic constraints. And then below that you have a spec and that spec says what this circuit is supposed to to do. So, what the meaning of the circuit is or you can also call it a post condition of of calling this circuit. So, the spec says that B is um one if X is zero or zero otherwise. Um and then there are two proofs which are soundness and completeness and both proofs uh complete in one line in this example because um we I want to stay on this slide a bit um because the the proof is very simple and we have some auto automation that's designed to

make simple things quite easy to prove. one thing to note here is that we're um we're currently um changing our witnessing approach. So, it it used to be you could witness an arbitrary lean. Uh your witness generator was an arbitrary lean function which gives a lot of uh flexibility, but it's not very good for exporting. Um so, we we are switching to a to a sort of IR deep embedded in lean to create the witness generation code and you can see that in the this dot ITE if then else it's a sort of if then else.

Yeah. So, there is a little There's two basically two DSLs. You can see here it's one for the witness generation code and the other top level DSL for the constraint constraint definition. Um so, the nice thing about this is that we have a completely symbolic representation of both the the constraints and witness generation code and we can from this definition we can export to a fast implementation, possibly a TPU implementation or or a Rust implementation. And it's very easy to to write this printer that takes our takes our constraints, the witness

generation AST, and some work steps to, for example, Rust code. So, so the goal here is to have something have sort of give you give you a framework to um to write circuits that are sound and complete by design. So, it's it's more I think of it more as a front end um as then as a as a formal verification back end that you extract stuff to. So, maybe one one one step back uh to to make another point.

Alex, can you go can you go back? >> Um So, I think one one other point that I want to make here is the there's a soundness and completeness theorem, and it's the same for every circuit. So, in in a lot of the extraction pipelines you see basically, you prove ad hoc theorems. And Cleanne really tries to be a framework that gives you that gives you a single definition that says what it means for a circuit to be sound. So, everything you do has to fit in that framework. And so, basically, you never have to uh you only have to check that statement once. And then you And once you're convinced that this is a good

definition of soundness, you will never have to think hard about what is actually proved and for every individual circuit. So, the only thing we really have to look at is the spec um here uh to convince ourselves that this is this is doing uh the right thing. And some circuits have additional additionally have assumptions on the inputs. So, you would you would look at the assumptions and and on and on the spec. And here a spec is often really really simple. So, you have often have huge circuits um with thousands of witnesses and in the end they just do a scalar multiplication and the scalar multiplication spec is is

like just one line. So, you're reducing a huge bunch of a huge amount of uh complexity to just verifying the um Yeah, some some words. okay, next slide. Um yeah, so summarize the the goals that we have here. So, we wanted to look pretty. So, we wanted to compete with with the existing front ends like Circom. So, I want Kim to be a drop-in replacement of Circom, for example.

Um with the with the difference that the circuit circuits are already formally verified from the from the start. the whole all of the trouble we have with auditing circuits is is just going away. Then, we we really tried to make the the proving UX good. So, that's what I call PX. So, it should be um once you're dropped into your soundness proof, you call our technique that starts the proof and that's should do most of the get [clears throat] rid of most of the boilerplate uh of our framework and give you the the actual mathematical statement proof.

That's really the strong goal. There's still there's still more to do on this, but I think and always scale to pretty complex circuits um and that the choice is pretty feasible. So, we implement that. We have implementations of stuff like Keccak, SHA-2, Blake, our latest also small VMs. And so so they show that that pretty much scales. Um the proofs proofs don't get too complicated.

Um Also, we found that elements are pretty good in some >> Yes, and? >> Just planning it. I'm aware. >> Thanks for muting. All right. Um yeah, then uh Lean feels very much supposed to be exposing the raw constraints and the non-determinism, so it should be on par with with other low-level circuit DSLs.

and because it's it's just embedded in Lean, you get the you have a real real powerful general-purpose language to do abstractions. Um so for example, you can you can create higher-level types like um I don't know, curve point curve point or a multi-integer and stuff like that. You you can create your own abstractions because you're in in the end you're just writing Lean and not any custom language. So yeah, that's um that's our goals and our ongoing um efforts where we are right now.

the the latest example of work was um that we start modeling entire CKBMs in Lean. So what you saw before was one circuit but one formalized circuit. And what a VM would be it defines multiple air components and it also defines um cross uh cross-table interaction channels. and then can you still hear hear me? Okay. Um And then you will define the a whole system of of of errors that gives that implements the CKB-VM and then you prove that sound global in a global view.

Um so we have like a proof of concept of this. We recently added um adding so added interaction so it's it's becoming more and more um like uh modeling real real world systems. Um so I think in the end we will be in a place where you can define your entire CKB-VM in clean um that is not behind on any metric behind like the production CKB-VMs that that are often written in Rust.

And it's completely end-to-end formally verified both the soundness and completeness statement. Or I mean I should be careful when I say end-to-end but talking about the the error and circuit statement that will be completely end-to-end verified. despite uh like not not verifying the the proving back end. Um then other efforts. So we we're currently standing formalizing the Zcash Iron Wood circuit which is probably the largest project we've done so far and we we already have a a complete proof of concept so and this is this was like written in a

rush to to help the current Zcash efforts for verification and it was written like in two weeks with heavily LNM assisted. And this was really a confirmation that this this whole idea kind of works. Um because yeah I I didn't have to read thousands of lines of proofs um to convince myself that this is actually formalizing um the correct spec of the of the Zcash circuit of the actual circuit.

Um so and we will continue this effort right now it's sort of approximating um the Plonk arithmetization and in the coming weeks we will make that um like a proper model of Plonk that that can really match um the verification key on the Rust side one-to-one. So um it it has to it has model like the custom gates and the and the column layout and everything. Um so we will in in in this effort we will kind of channelize Lean.

Currently it's more designed for Aires and R1CS. But I really want in the end I want wanted to be sort of a circuit DSL for everything. Um generally enough to to to cover everything. Um and we will very soon Tian release a uh a circuit optimization challenge. So which which will be called CK Golf. So look out for that. Um this is sort of an experiment because we found so some some of our engineers have been playing with with Lean without knowing much about Lean and like my my my co-founder just um told Claude to write like the most optimized SHA-2 implementation

in R1CS and it did it and it's created something which is much more efficient than than any of the production circuit libraries and it's already formally verified so you know all those optimizations work. So that's why we call fearless optimization. And we want to create a bit of a game around that um put up a website where there there are different challenges for circuits to optimize and and people can submit them. It's it's it's it's it's going to be a little bit like ecdsa.fail.

For um improving the the Google post-quantum circuit. So, yeah. Um that would be fun. Go from there. Yeah, so that's it for me. So, I think yes, so this covered the kind of regular slots because we didn't get confirmation from Zcash fork, but then we can follow up straight away with Devin, I'll open your slides as well, uh who's also has some clean-related work to talk about. Uh so, after you, Devin. >> Yeah. So, sorry. I don't know if the thing is the the best format for this, Yeah, so uh I guess Gregor just talked about clean and um

yeah, we basically we had already an existing sort of soundness uh verification of SP1 that Gregor had not Gregor, but Pierre had talked about. Um And so, we have this uh soundness, but it's it's sort of a mess, and it's not exactly very modular or or easy to sort of keep track of everything that's happening. So, um I guess for for quite a number of reasons, we switched the actual DSL to clean. Um And so, on the top here, I have just sort of the general pipeline we're using for this. Uh like Gregor said, the the clean sort of functions better, I think, as as a front end. So, what we actually do is extract

the constraints and the interactions from the Rust and prove faithfulness, so some equivalence between the interactions and constraints in uh reimplementations of all the circuits in clean. Um This lets us sort of change the circuits in slight ways that make proofs easier without uh affecting the Rust and still still knowing that things are you know, actually modeling the proper code. And then instead of bridging directly to sale, the the big complicated monadic model of sale, um we write specs for each clean circuit in terms of uh pure RV64 specifications. So, it's

just making pure statements about arithmetic uh or or a number of interactions and things like this. Um and then on top of the soundness proofs, that was reused as much as we could from the the work that was done with Nethermind. we also now have completeness for each chip in the other direction from these specs. And then we show this this pure RV64 specification gives us most of this bridging to sale already, but we do need to sort of tie and wire a bunch of things in to eventually show then that also on the monadic sale, we we also preserve the constraints.

So, in the end we get uh stronger guarantees than we had before. It's a lot easier to read the proofs. I think total size of the code base went down, I think still, uh depending how you measure some of the tests. Um and it it compiles a lot faster. I I think there's been I would say mainly just upsides to this. Um I I would strongly recommend not rolling your own DSL at this point. Um There's also some in-progress work on doing full trace level things, um the full ensemble soundness and completeness. The soundness is mostly

done, the completeness much less so. Um and then uh having a full end-to-end theorem. And then on the on the left down there, I guess I have kind of just what the circuits generally look like. Um we have just a number of assertions, usually some witnesses. We're still using this old version of witnesses. Uh I know whenever, you know, Gregor gets the new version and we'll have to change all that, but uh we're verifying it correct relative to those and then uh for each thing we have an assumption in the spec that looks something vaguely like this.

yeah. Very cool. Uh and I can confirm it does actually build quite a lot faster by an order of magnitude. Uh probably. Uh all right, so then we have uh Albert's talks. I think Albert, you wanted to share if it works. So, if you want to try and share, I'll let you share and then if it doesn't, uh I'll uh I'll switch over to sharing again. >> Uh can you see my screen? >> Yeah. Okay. So, it is Albert from from the Costa group.

>> Uh so, your volume is a bit low. I don't know if you can up your microphone volume or speak louder. >> Uh is it better now? >> Yeah, it does sound better. >> Yeah. So, it is Albert from the Costa group, but uh Costa the Complutense University from Madrid and this is research funded by the Ethereum Foundation. So, our aim is to develop the Averser tool, uh fully automated tool to to help uh developers to easily find bugs or or to have a first good level of confidence on the correctness of their ZK virtual machines. And this is done uh by using SMT solvers.

Okay, so the the first key mm point [clears throat] is that besides determinism, uh Averser can uh focus on proving semantic equivalence, which means this uh to check the equivalence between the witness competition code given in L L C K and the arithmetization the constraint system. So, the the first important thing in our tool is that the transformation from the witness competition to an SMT formula is done by using Lean and then provide a certified transformation. So, we don't lose anything when going from the L L C K to to SMT too. I mean, don't lose anything

regarding the correctness. And and then the second important point is that we have developed our own open source SMT solver which focus on ZK verification properties. So, this this solver use several light check light checkers to avoid the the heavy reasoning on finite fields, but also includes ring check reasoning natively, which has turned out to be very useful when proving properties of ZK virtual machines. In particular, although we have a portfolio of solvers

and other tools, it's almost the case that our solver is the one that solves the the SMT problem. So, regarding the evaluation, we we have evaluated our tool verifying task as our case study, but we can apply to any other tool. In fact, if they can provide L L C K, we can we can apply our tool. And >> we have done it for recursion circuits and for state machines. And for recursion circuits, we have proved termination and we found two two bugs and once they are fixed, we were able to verify it automatically up to 90% of the of the circuits, there were some that reasoning was beyond what

an SMT solver can do, but this was really tiny. And then for these machines, we have considered the thermistor. We have verified all binary machines and we are working on the arith and then we will go to the to the memory. And for semantic equivalence, we have applied the the full pipeline to prove to prove fully automatically the equivalence of the binary add and now we are with the rest of the of the binary machines. And also we have applied this to to to prove equivalent semantic equivalence of circuits from the Circ lib. So all this can be found in this git. It's all open and if you have any problem to install it or or you want to know

anything else about it, just tell us. Thank you. >> Thank you very much. Uh if there are any questions, you can quickly ask one and then I'll share for Cody. Oh yes, and there's a timer button. Perfect. All right, over to you Cody. >> Uh I still see Albert's slides. >> Oh, sorry. Sorry. Sorry. >> I'm not sharing. That's better. Okay, over to you.

>> But now Okay, yeah. Um yeah, thanks. So yeah, we can go to the next slide. There's I'll share a link after I finish speaking. So my goal was to do um a RISC-V for spec verification effort for a Zisk, which hadn't been done. Um I had a good starting point from the work of Petter and others at Nethermind in France. So um I thought I would begin as a sort of passive experiment and then if it started to take form, take it more seriously and that's that's what we have here. Um, I think it's in decent shape now. Uh, we could I guess you could just advance all the bullet points, Alex.

Thanks. Let's go sharing. Yeah. Um, so [clears throat] yeah, I mean the goal is to uh, initially show oh show soundness. So to show that the uh, state transitions accepted by um, by Zisk are spec valid and well, we've we've heard these terms already so maybe I can go on. Um, I wanted good reproducibility of everything including the extractions and good CI turnaround. Um, that's all in a good place. I wanted to use standard tools like Enneas and Clean and to be explicit about the verification boundary and claims and uh, to implement testing to cover those gaps. So we can go on to the next slide.

Thank you and maybe just go through all the bullet points there, too. Um, right. So the goal was to sort of build it end-to-end allow the AI's to axiomatize and then remove axioms. And uh, yeah, that I could tell that it was working cuz I found bugs. I found three bugs in Zisk doing this. Um, so two of which were new to them and uh, one that they had between the time of me starting the work on version 0.17 and them um, uh, and then a couple of upgrades later they had found that other bug. Um, so now I'm in the process of like cleaning it up, making it more legible and then I'll audit um, it a bit with Hector from Zisk and then perform some upgrades to

test maintainability, think about maybe the structure of the FV library in those terms and then work on completeness and uh, expanding testing. So that's all for me. Thanks. >> Uh, thank you. And then I think next we have Kwong who I think is going to share. Give me one one m- All right. So, Okay. So, my slide is on the It's on the Google Drive, but I also share it here.

Oh. Can you see this? >> All right. Cool. So, I will be doing double duty here and talk about both VC VIO and ArqLib. So, these are two lean libraries. Oh, let me see. Cool. So, so these are two lean libraries for the efforts of formally verified proof systems, aka the STARKs that we know and love. In order to do that, we first need to have a base layer for reasoning about cryptography. And that is VC VIO.

The job of VC VIO is to define this this base layer based on the notion of oracle computations or algebraic effects. We give it the semantics that is probabilistic. We give it a program logic that can reason about both a single program or a coupling of two programs. We also have a bunch of examples and including the NIST standardized lattice and hash-based signatures. These are ongoing works. Some other works like the forking lemma has been finished.

And we we have downstream usage now beyond just ArqLib. There's a project using ours to do symbolic cryptography in Lean. There's another ongoing project called Signal Shot that's trying to formally verify the whole of Signal Protocol and they use VisiVao to to scaffold their definitions. Now, let me come to Arq Lib, which is the main library that I think people care about here about formally verifying our starts. At the core of Arq Lib is the notion of interactive Oracle reductions, so IORs.

We define what they are and we define how they can be composed. The the main motivation here is that STARKs are fairly complicated and so we should be breaking them down into modular components, specify them, prove the security, and then compose them together. And the composition theorems will say, "If your components are secure and the glue is secure, then the whole thing is secure." Roughly speaking. We're also starting to really ramp up the work on the Fiat-Shamir transform. This is not just a theoretical kind of transform, it is the actual transformation that is used in the Sponge phase library and that is

also going to be set as an IETF draft. I think there will be a later talk here that will talk more about this. We're also starting to have links to other libraries, say for the front-end verification or for verifying Rust code bases. And we have ongoing examples including the Sum Check protocols, a bunch of polynomial commitment schemes that are both hash-based and more recently also lattice-based schemes. one very exciting news that just happened, I think, a day ago, is that Arq Lib is now featured as one of Lean's use cases alongside Mathlib, CS Lib,

ADS, and so on. So, it's a very exciting time and if you're interested in contributing to either either of these libraries, they're open source, you're free to give us PRs. We would greatly appreciate them. Thank you. >> Thank you. And yeah, and we get I should say we do get quite a lot of PRs and a lot of first-time contributors. So, thanks to everyone who has submitted PRs, that we've merged or not merged. We appreciate all PRs. Okay, so next we're going to have Bas and then Derek. I will share for both in the interest of keeping myself muted.

I'll let Derek chime in as soon as Bas is finished, and I'll just start sharing now. >> Yeah, thank you. I want to present Cat Crypt. So, this paper's been online for for a bit. So, it's a large library of in in Lean about cryptography in the computational inspired and and partially started as a point of port of the the SS proof library that we have in in Rock, which is a big library based on state separating proofs.

which are very appropriate for protocols that share actually share state. So, this is the methodology behind for example the Joy of Cryptography book. And it's also that that actually carries over very nicely. It's called Cat Crypts because there's a big categorical treatment behind it. So, we have a categorical treatment of universal composability and of the state separating proofs, and they're nicely combined in the in the library. Um it's all built on We also have a a bridge to um the high assurance primitives. So, we have a huge library of elliptic curves.

So, that's in Rock, but I can translate them to Lean via a shared Rust subset. Uh so that code is uh is online. Um it it also contains quite a bit of the dialect library that already includes Fiat crypto backends, but now we verified much more in Rock, but I can translate it to to Lean. I've translated most of that to Lean. Um so so that has a full suite of of elliptic curves. Some of them are the the first implementation. Um it's connected to our Hex tooling. So we have two embeddings, both in the imperative and the direct functional embedding.

Uh so for all of the protocols, most of the protocols in Cat Crypt actually have a uh reference implementation in Hex. I can also target some of the other Um and part of the Hex library I verified in in Lean. Basically the last third. Uh so one once you're at the C level, you do some transformations. And then you end up in a fairly well understood subset. And that that subset I verified in Lean.

It it's tightly integrated into the the Lean ecosystem. It's connected to MathLib, to ArithLib, to CompCert, that's the next talk I think, and to VZV. and yeah, the the preprint is online. I'll soon also release the the other parts. >> Uh and I'll let you >> Yes, one of the quite impressive things about this is the amount of content that was generated for Cat Crypt, which is it's a review bottleneck, but in terms of generating a lot of content very quickly, uh it was super impressive. And then I guess we can switch over to Derek to tell us about CompCert.

>> Great. Yep. See, I will present on CompCert. Could I get to the Uh what is CompPoli? CompPoli is a library of computable polynomials in Lean. So, it started with just univariate, bivariate, multivariate, and uh multilinear polynomials. We also have a field I guess field specification we have implementations of fields and um and other kind of algebraic foundations of uh SNARKs. And so, why do we have CompPoli?

CompPoli is the computable core of Arclib. That's kind of where it started. And it mirrors a lot of the um constructions in algebraic constructions in Mathlib, but with computable uh so, everything everything CompPoli is computable and then proved equivalent to that's counterpart in Mathlib. So, you can still do all your proofs in uh Mathlib by transporting over the isomorphisms. Um and then there are just lots of applications of computable polynomials outside of uh Arclib. And uh and so, this library is kind of it's it's dream is to be useful all over the place. Um uh next slide.

So, uh we've been working on a roadmap with CompPoli since the beginning of this year. We finished up with the theoretical foundations uh phase one um in March of this year, and that was mostly theoretical and API completeness. Phase two is very close to being finished. So, I've uh said I've put the check mark for July. Um we're just finishing up with some of the fast field uh arithmetic and implementations. And phase two is focused mostly on optimizations, benchmarking, and making these uh not only computable, but kind of interestingly computable and uh and reasonably fast within Lean. And uh phase three is what we'll be working on

uh over the next several months is further optimizations and then kind of make getting it integrated in the community hopefully upstream into CS Live at some point. Next slide. So, we've had a lot of recent contributions. I just wanted to highlight some of the some of the recent work that's been done by various contributors. So, we have interpolation, we have barycentric interpolation, we have several root finding algorithms that are specialized in different different places. We have bivariate operations, division, factorization. We have a computable Goswami Sadan, which is actually pretty cool. Goswami himself reached out to Formal Land, who did this

work, and made use of it with his students. We have various optimizations, evaluation, error correction, fast fields, etc. Next next slide. So, there's the link if you want to learn more, and these phase two contributors, I've listed them here. So, yeah, thank you all for all your help. This is very much a community effort. And that's all I have. >> Thank you very much. Let me just check the chat quickly.

Not too many questions. And yes, so this was really nice work. Okay, so now I guess it's for me and Giacomo, so I'll keep sharing, and I'll let Giacomo introduce things a bit. >> Perfect. Hey guys. So, good. So, I want to give you like a little tiny bit about proximity price, and how formal verification we think will be a very important tool for like the proximity price verification we're going to do. So, just as a very quick refresher, proximity price is a set of challenges related to the security of large space marks, which go and find the roots into coding theory.

We have a website, we have like the statement, and we have a companion paper, which is this ABF 26 paper, which formalized the what are the conjectures that we believe, and we would people to invest their time onto. Within this paper, one of the things that we introduce is this toy protocol, which is a toy, you know, as in the name, a toy protocol, in which there's the analysis closely mirrors that of existing hash-based proof systems. And throughout the paper, we analyze both the the the the knowledge soundness and attacks on this toy protocol.

as a target that we want both for like our research formalization and for like the proximity price, we would like people to figure out what is the actual soundness that this very simple protocol can provide. And what I'm really happy to say that Alice will talk more about this is that now most of this paper has been formalized into Lean. So, now we have theorems and we have like actually verifiable theorems about what is the the content of the paper, which we hope can be useful for both like for, you know, the sanity of the judges to figuring out which results are actually correct, and also for like enabling like the wider community to contribute and have confidence in their contribution.

So, on this note, I'll let Alice tell you a bit more on the Lean side of what has been done for this for the opportunity price. Uh uh I didn't have to unmute myself for that. Uh yeah, so as as Jack's mom said, basically I've been spending a bit of time formalizing the contents of this paper on top of Alkebri. Alkebri for background as you already had a large body of coding theory uh proofs because we have uh uh proximity gaps for Reed-Solomon codes, for example, is proven in Alkebri and and so on. Uh so, we already had a lot of preliminary material. There was a bit of more material to add, uh but this PR here basically contains everything. I think I have uh three small stories that I need to go and

address, uh and this will be done soon. Uh it covers the entirety uh or pretty much all of the paper and everything that you need to state the actual conjectures and the grand challenge. And so as of right before this call, we have a new repository. It's currently private. It will be public and upstream as soon as I have spent a bit more time reviewing my PR and checking that the statements are actually correct. But we have a standalone repository that pulls in archive as a dependency. And if ever you think that you've cracked the conjectures, you can open a PR and CI will check it. And we should be able to make progress. Um there is built-in support or it's intended to support auto research.

We've seen a lot of progress on this with the obviously the quantum circuits and clean is going to have some auto research. Everyone is doing auto research. We should do auto research for this as well. it's formulated in a way to support and facilitate auto research. It'll be public very soon. Looking forward to everyone contributing. Yeah, that's basically it. And I guess I should say the formalization efforts did find at least some things that led to changes in the paper. I think it was lemma 612 that changed.

And so it wasn't it was useful or at least it's been useful already to some extent. And hopefully it'll be useful in helping us sort out solutions to the conjectures. And I think that's it for me and then we're off to Fiascherino so I can stop screen sharing. And then yep, Chung is ready. Off to you, Chung. Hi, you're muted, Chung.

>> Okay, can you hear me? today I present our project formalizing the classical theory of transformation in Lean 4 and in the Uplink library. And our team consists of me, Trung Nguyen, Michele Aurou, and Quang Dao. so, the Fiat-Shamir transformation is a critical component in the Uplink library. And it uh transform the the non-interactive protocols uh the it transform the interactive protocols into the non-interactive protocols. And uh in the theoretical model, it let the prover query my queries to the random oracles to get the verifier challenges.

And in practice, um uh people usually instantiate it with uh sponge construction. And in the paper CO25, uh a Fiat-Shamir transformation from duplex sponge uh uh the SFS the authors uh provided rigorous analysis uh security analysis uh for uh the Fiat-Shamir uh uh variant based on duplex sponges. And um so, simply put, uh each round in the SFS construction, the prover um uh absorb the the the encoded ver- pro- uh prover messages into the sponge and

the squeeze out the verifier challenges. and uh these two operation, they uh figure close to the uh uh a single office size uh permutation oracle, and which is uh consistent across the rounds. And uh this is uh close to what practitioner do. And uh when uh since we started working on this project, we are about 30% done. We have finished all the construction and the the soundness proofs. Uh and um there are things that turn out to be uh different when we bring the pen and pen and paper proofs uh into uh the theorem prover.

For example, when we work on formalizing the the data structure for looking up the trace entry, instead of following the paper and uh implementing a certain specific uh data structure that is highly efficient, we decided to design an abstract specification class that contains uh the allowed operation as well as the mathematical constraint for the operation. And this way we can plug in any implementation of without exposing the internal logic of the data trace of the data structure

in into the proof layer. And we can like delay the implementation of the complex and efficient data structure and without blocking the progress. And in in conclusion, in this project we do from the formal verification of the the best bonds via similar transformation. And the the source code would will be available in the repository and you you can check it on there.

that's all for me. Uh and so next we're going to have Matthias. He's going to talk about XMSS which is and verifying these. >> Hi everyone. Okay, can you hear me? And see my screen? >> Okay, perfect. So uh hi everyone. My name is Matthias. Um and like others here, I don't have yet any cool amazing results uh, show.

So this is more like a quick introduction to a new project that I, um, am working on. That we are working on. Oh. Does it work? Yeah. So, uh, quickly some sort of background relevant background, um, related background on me. Um, I have recently finished my PhD where I mostly did, uh, formal verification of post-quantum cryptography using the EasyCrypt and Jasmine sort of Formosa tool chain. Uh, maybe you've heard of those. Um. Yeah. And so, particularly I did, uh, the hash-based signature schemes, uh, XMSS and SPHINCS+ both, uh, their security proofs as well as their, uh, their functional correctness to their then there is this, um,

uh, proposal to move Ethereum to, uh, post-quantum um, by replacing BLS by a, uh, multi-signature, uh, variant of XMSS, um, as a replacement to the, uh, aggregate setting signatures. And so, to sort of, um, make use of my experience with the hash-based signature, uh, security proof side of things, um, we decided to, well, try and have a look at, um, formalizing this and formally proving, um, the security proof of this, uh, proposal in Lean.

as I said, there's not many, um, Google results yet, but um, the overview of the overall proof and scheme looks as follows. So, we have the uh, the the final scheme which can be decomposed in like a generalized XMSS variant of XMSS, as well as an aggregation, uh, scheme for signatures which is just, um, in this case going to be a PQ Shrag Snark which is, um, left abstract for this scheme. So, the focus is mainly really on the hash-based, uh, XMSS here. And the XMSS in turn can be decomposed in these components. Um, you have the Merkle tree, of course.

Um, the function change for the one-time signatures, as well as the encoding scheme. That has to be incomparable. right. So, these are the components of the XMSS. And then, at the bottom, of course, you have the hash functions, on which everything is uh based. and yeah, and so, in also in this sort of decomposition, I'm planning to sort of tackle this. And starting from bottom up, of course. And so, currently, I am still looking at these uh well, these foundations here. And some of some of it has already been been done, like the basics. But, uh yeah, as I said, no no impressive results yet. So, uh hopefully, next time, in the next um

uh call, I will be able to actually uh give some cool results here on this uh project. Yeah. And that's uh that's it for me. Yeah. let's see if we have any if you have any other questions. And then, otherwise, I think next up is uh Nadeem or Hussein or Lorenzo, who will talk to us about Sound Calculus. >> Okay. Can you see my screen?

>> Perfect. Hi, everyone. Thanks for the introduction. So, uh a couple of weeks ago, uh we started formalizing Sound Calculus in Lean. We actually started porting it. And very rough, again, Sound Calculus is this tool that currently allows uh ZKVM devs to have a quick and efficient way to compare, let's say, different configurations uh some ZKVM may have. What happens if with which fields are on? How does this affect soundness? And whether, again, the overall soundness that one gets is still is within some provable bound. Yeah. Uh so, why bother doing that in Lean?

Well, crucially, because, again, the current implementation is in Python there could very well be uh implementation errors saying hand trust grabbing formulas. There could be bugs in the formulas that may not be linked to the underlying cryptographic assumptions. And also it could very well be the case that some Python artifacts may lead to some loss in accuracy say whenever we're dealing evaluating exact arithmetic so reasoning about rational numbers for instance. And indeed here you can see a couple of examples of you know semantic uh let say mistakes that were done in an inaccuracy rather that were done in the current sound calc for instance. We have a rate that was weakly cast to an

integer as opposed to a float. And on the right that side you can see that this list size parameter which should increase the error is actually decreasing it in a specific ZK-VM configuration. So with Lean basically we are aiming at providing a sound calc on steroids that at the bare minimum matches the current sound calc evaluation so that we get a one-to-one match with respect to the reports that are currently being produced by the current project but also having a verified calculation on top so that yeah if there is any issue any discrepancy between the two we can actually figure out whether we were wrong in formalizing it in Lean or whether there was an inaccuracy in the original sound calc. And once we have

this foundational building block this whole building block we're planning on actually building useful tools on top of that. We are aiming at providing also a way for developers to prove theorems that could be stated in a way like I mean if I switch a field with another field in a specific configuration I'm not going to lose security and I can prove that. And we're aiming at the bare minimum to have A plus B by the end of the internship. And then there is Sepsi which is much more open-ended which aims also to have some kind of integration with the current ecosystem with Darkle and the latter so that indeed all the formulas that we have in Lean, can actually come with a combined theorem and that uh could allow us to say for instance that the specific uh item, a specific component of the ZKBM,

soundness error is indeed bounded by a formula uh under some uh small and shrinkable trusted ledge. That's that. So, stay tuned. >> Thank you very much. I think this is uh pretty cool and in general like being able to do some statements over uh some composed proof systems. This is what ZKBM is used as something we've been after for some very much looking forward to this. And then next up we have uh Raul who's going to talk to us about the work on uh translating Veil which is Succinct's kind of compiler to make proof ZK uh and obviously doing some proofs about this in Lean.

>> Okay. Um so, everyone can hear me and see the screen. Perfect. Okay, so let me begin. Uh thanks to everyone for uh coming to this and listening. Um so, first of all as uh you heard um I'm talking about formally verifying a particular practical protocol. So, this is a Succinct's Veil compiler which is basically a compiler that you feed in an example of sort of a broad class of cryptographic protocols and uh it adds hash-based so plausibly post-quantum zero knowledge to this protocol.

Um so, Veil is optimized to have uh low engineering and performance overhead. So, if you've coded up your protocol already, it shouldn't take that much more code to convert it into Veil and uh the prover for the new protocol should be negligibly slower than the prover for the old protocol. Um so, we're trying to uh we're actually going to be using this. We're trying to convert SP1 into the Veil format so that we can have sort of a post-quantum zero knowledge added to SP1. So, Veil has a big problem and uh the big problem is that the proofs of soundness and ZK-ness depend on 30 pages of dense and very finicky mathematics.

And uh in particular, ZK-ness is notorious for being very easy to make mistakes with. Um particularly for practical protocols that have all the fiddly details that you need for uh to to handle all the use cases. So, because of this, um we felt that we needed a better guarantee of protocol correctness than just maybe human-written proofs in the paper. So, how did we get this? Well, miraculously, it turned out that modern LLMs, uh with them, it's very effective and practical to actually prove ZK-ness or to to verify protocols.

So, we were able to use Lean uh to use Claude Opus 4.6 4.7, which used human-written proofs as a reference to generate a formal verification in Lean. Um this did not take any sophisticated harnessing, just the Claude that I'm doing that kept a running record of common writing pitfalls that we found while that we found the AI doing and things like that. And the total human time was basically the equivalent of just one to two person-weeks of full-time work. And frankly, it was only that much because of maybe like my lack of Lean experience before this project and some stupid mistakes. So, this was very efficient.

Um so, the key difficulty of this is that it was very hard to get a correct sort of trusted base. You have to make sure that you're actually verifying the correct thing when you're working with Lean. So, this took dozens of iterations of human-directed edits for correctness and readability. And um it required very careful human auditing. So, it was very important that we had a good interface to audit these protocols, to audit the formal base of formal statements properly. And uh once this was done, um the proofs were very straightforward. They were basically one-shot. And uh as everyone else has been pointing out, um a test of usefulness is that we actually caught a ZK bug. So, in conclusion, I think this is like a very effective way to sort of add more guarantees that a new protocol can be correct and I think

this is the thing that sort of more people should try to do. Thanks. And [clears throat] then I think so that finishes the I guess cryptography section and so next up we have I guess a bit of an interlude with auto research that Bonner is going to talk to us about then then we'll go into copartners for cryptography. So over to you Bonner. >> Hey. >> Can you hear me Bonner? >> Perfect.

So for the past three months I have been applying auto research as a methodology for zero knowledge code bases. On the left you can see there's a bit of my hardness that I have been using with many supporting personals to enable the auto researcher personal to work. On the right side I brought a little practical example. I believe smaller models are the perfect sandbox environment for building these up because you run into issues that also exist in a larger model but they are abstracted away. So this specific example was research discipline which was a big issue on Opus.

I implemented some hooks to enforce the behavior and then it produced quite outstanding quality directly on favor for the few days that it was up. In terms of results this was mainly targeted at the building VR code base. The coolest PR I think is the ZK unlock PR that I highlighted. This was a bump reset or in our locator pre-using like a technique from the 90s that it that produced the 27% speed up for warm groups on the native prover side.

And what's actually really cool is that the previous PR before that was about eliminating unlock contention which already produced the 10% speed up on the native prover side but there was still overhead to find. Next to that, we also contributed with this to uh Plonky3, Glad Crypto, and Vortex with smaller amount of PRs. And the missing piece was essentially quite obvious during the ECDSA dot field initiative, where the ZK proof that was published for Google's Quantum Circuit acted as the perfect invariant to essentially let the agents uh perform really, really well. And the equivalent is for ZK codebases, it's obviously formal verification. Beside

that, I have been experimenting in the last weeks with automated auditing processes in loop and out of loop. And you can check out the work on my GitHub. The repo is open source. >> Yep, thank you. And uh and yeah, there's been some already some interesting lean results that have come out of this, which is very, very cool. Uh so, we can go into compilers, starting with compilers for circuits with LLZK. Uh I'll let Veridise go on. >> All right, thank you very much.

All right, so we are working to bring formal verification tooling to the LLZKIR, which is our shared common intermediate representation for ZK circuits, which is implemented using the LL the MLIR compiler framework. So, one problem that we've recently been working to tackle is that of circuit inconsistencies between witness computation and constraint generation that can lead to security vulnerabilities that are hard to uncover during audits. Our goal then was to build a verification tool that could automatically verify the consistency between the witness computation and the constraint generation. This led us to develop a tool that we call LLEQ, um which is uh uses a combination of lightweight static analysis and deductive

verification to verify if witness uh logic and constraint generation logic are equivalent. And we have planned to have a dedicated talk about LLEQ this coming Monday on June 29th. Uh another problem that we've tackled recently is that of encoding formal semantics in ZK circuits, which is currently challenging as developers must write custom libraries for general-purpose proving languages to encode ZK specific properties. Our goal then was to allow developers to specify formal properties of ZK circuits independently of the target proving languages low-level details, while also integrating seamlessly with the rest of the ZK ecosystem.

And this has led us to develop uh LL LZK spec, which is a high-level specification language targeting compiled LL ZKIR circuits, and then the Verif MLIR dialect that LZK spec compiles into and can be further lowered uh into SMT for verification tasks. We actually recently had a talk a dedicated talk about this project uh this past Monday, and you should be able to find the recording for this on the Verified ZK EVM uh YouTube channel at least at some point. Um the LZK ecosystem has already supported production-level verification tooling as well, as Veridise has updated our in-house determinism verifier Pykus to use the LZKIR stack and has recently found seven

real-world soundness bugs uh over one weekend of verification effort. And so you can find these suite of projects uh and more under the open-source project LZK organization, and we look forward to engaging with you as we continue our mission to formally verify ZK systems. Uh thanks, and I'll take any questions that you have. >> Uh yeah, so if anyone has some questions whilst we switch over, feel free. Uh and yeah, the the talk uh Ian mentioned will get up on YouTube probably later today. Uh I need to go and fetch it from the the Google Drive.

and so next up we've got uh Gary on who's also going to talk about uh I guess constraints, but in the context of Auto Precompilers this time. >> Hello. Um yeah, so this is I'm I'm Golem. I'm talking about translation validation for Powder Auto Precompilers. This joint work with Ari and Alex. Um Ari and I are working at Cetara. Alex just started at Google Tech. So, as we weren't quite sure how familiar people are with Powder, I'll just take half a minute to talk about that. So, Powder uh takes basically the the KVM semantic, so uh and for example,

Open Open VM program and compiles it into a big program the the K uh VM program for the the Open VM program. And this first step is just basically structurally meshing together pre-built gadgets. And this is I mean, I think we already heard a bit about how to prove correctness for these gadgets, so for single instructions, uh but then the step is pretty much correct by construction. And then the idea in Powder is that uh we're doing a big uh optimization pipeline to make the uh the knowledge proof in the end of the constraint system much smaller.

And this is actually yeah, a lot of individual rewrites more or less complex and in principle, a lot can go wrong there as we know from regular compilers, and so we want to uh the the goal of our project is to figure out whether we can uh formally verify what happens in this Auto Precompile um pipeline. And so, what we do is we take a concrete program with Powder and then we verify that uh the equivalence for each individual optimization step. So, So uh we we don't directly verify the the pipeline in linear anything, but we do translation validation for particular inputs.

Um so what we did is we first formally defined notion of IO equivalence with both interactions. Then implemented that. It reduces to SMT and we we eventually solve that with an off-the-shelf SMT solvers. Currently Z3, but yeah, whatever performs best obviously. In the between that we do a bunch of domain-specific simplifications where the domain can be just the domain of Z3, but also what exactly the powder optimizations are doing and also how exactly our notion of equivalent works.

Um and then we're evaluating that on the three benchmarks the powder team told us to be most relevant to them. So that would be catch up pairing and wrath. we found a few minor issues um that the powder team already knew about and we kind of then told them yeah, how about you you actually prioritize that. Um so we didn't really found anything big. So this is probably a testament to the good code quality of the powder code base.

To note here that verifies the correctness of the auto pre-compiled optimizations. It does not say anything about the programs that actually go into powder. So if you give powder an incorrect input, then the output will be incorrect as well just as for the compilers. So the future work is we want to emit proofs because in the current model essentially our old all of our tooling is part of the trusted code base. So, if we tell yeah, it's correct, you need to trust us. So, we want to make that proof-producing so that you can then feed that into Lean, and we basically just provide a witness that you can verify.

yeah, and currently it's more or less in a prototype stage, so we want to scale that up to bigger examples. So, on the right-hand side, we have the current state of the Kestrel benchmark. Uh as you can see, we have like over 90% of the of the steps come verified. over 70% of the basic blocks in the whole program are fully verified. Um but you can see in the graph there are a couple of blocks that are just huge, and we just currently die in our initial encoding just because it's a prototype Python implementation.

Uh we're currently working on that. And just to get a feeling on how long that takes, uh so the average verify time from start to finish is 31 seconds. So, that's not just SMT solving time in the end, it's complete us loading the dumps, analyzing them, creating the the encoding, simplifying it, and solving it. That's it for me. Thanks for the time. >> Yeah, thank you very much. And I think what you can use to see by is open VM and [clears throat] LSP what are the basic things and using it, so there's some nice immediate applications to this. Uh okay, and then next up we've got Manuel

from Lambda Class uh who gave a fantastic talk about AMLin, which is an optimizing compiler for constraints uh a while back, and he's now going to talk about SuperH which is the more recent work. >> Hi, everybody. Do you see the screen? >> Hi, thank you for having us. My name is Manuel. I work at Lambda Class in Buenos Aires, Argentina. We're going to talk about our progress in TRC. TRC is an idea of applying E-graphs to the design of hash functions.

the basic idea for people that haven't heard the previous talk is that hash functions can be thought as compositions of atomic functions. In a more maybe computer science way, you can model a a hash function as an AST. And at this point, we're working in a very restricted vocabulary. That is that we are using S-boxes and linear layers to compose and design hashes.

And one of the things that we've been doing now is uh we're trying to tie that design to an executable hash. That means that we need to transform the abstract design to something that actually runs. And for that, we have a theorem that we're actually running the the correct design. The E-graph that we'll work with the with the design is something that works in a mathematical way.

So, in that sense, all the designs are actually equivalence classes of designs. And the saturation part in which we can pick an optimal design is is is a mathematical extraction. Since we're restricting to a small classes of hash functions, we have built this pipeline end-to-end for um reference hashes. This is a very small set. And um we can actually run this for three uh specific hashes, but not for all the designs. Uh that's a work in progress.

We have like the building blocks, and we're going to wire um those blocks uh in the future. Then we start to work in the comparison of the designs. And since a design has an associated uh parameter vector, um we need to be very careful on how we see each of those parameters, mainly because different families of hash functions uh mean different things when they say active S-boxes or solving degree. So, what we need to have is a fair comparison between families.

Mainly because those notions that come usually from solving uh Gröbner basis problems uh usually mean different things. So, our approach is to build a pipeline that can fairly compare uh those vectors. Designs are not compared directly, but they're compared through their spec vectors and the comparable vector that we build. Uh this is also a work in progress, and uh we're uh we're advancing now. Finally, what we said um is that uh e-graphs actually find equivalences.

Um we can tweak that idea into find optimizations, not through a cost function, but by enlarging the equivalence class. >> And the uh the the idea that we had is that if we can model designs through terms, we can also model attacks through terms. And if we uh connect properly those two e-graphs, maybe we can have some sort of evolutionary loop between the two. We can have We can have a an e-graph that designs hashes and e-graph that attacks those hashes.

At the time being, those two systems actually exchange scalars. They do not read each other's designs fully, but that's going to be a work of the future. We've been working in the reaction of the blue team actually acknowledging the attack and keeping track of the families of designs that have have been already beaten. This point, it's We have to know that this is not actually performing any attack. This is just modeling families of attacks and it's ranking those families of attacks in terms of time consumption or compact or complexity.

So, this is still a work in progress. What we have in the future is tweaking some of these very small parts. For instance, benchmarking, taking account some reference implementations and pipelining and and connecting all the expressible designs. Write a polish CLI documentation and also expanding the interaction between the two e-graphs for more complete information. That is, we want the e-graphs to be able to read the design instead of of a summary of the design.

So, that's pretty much it. We have been very busy with this and I we're very happy with our progress. If you have questions, comments, just reach out in the Telegram group and we'll get in touch. Thank you. and [clears throat] then if anyone has a question, there's a bit of time in the changeover and the next talk otherwise is going to be uh about I guess GPU related things and Tzu-Chien is going to tell us about uh lowering to stable lean and stable HLO and the bridge between those.

>> Yeah, so the lean stable HLO is kind of like a compilation stack for the like uh from the lean to stable HLO, which is uh the made by Google like for the parallelize um execution layer for the uh LLVM. So, it's kind of like a MLIR stack for the the language. So, it is kind of like writing the cryptographic protocols in lean and we can just um like uh do some formalizing the this protocol and then we can do some compilation over this lean DSLs and we can get some ZMTP under the ZMTP for the cryptographic protocol and then we can serialize this

protocol to the stable HLO MLIR text. So, this point is we should uh trust this serialize serializer for the writing the exact text because it's kind of like inspired by some concert C compiler and also for fiat crypto style. So, it is making some one um untrusted point for this making cryptographic protocol in the stable HLO. So, and then we can do some like compilation from the stable HLO to LLVM or the bytecode thing if we connect them with the formal formally verified thing in the that layers, then we can do all over the

formal like formally verified execution for the cryptographic protocol. Yeah. So, I and I made the like KZ uh commitment scheme in in Lean, and then we can execute on the this on on CPU. Yeah, thank you. >> Nice. Very, very cool. any questions? >> Yes, I have verified implementations of the BN curves, and also connected to the the the compiler.

So, I have a compiler for that. >> Yeah, there is a like one point is uh like AC thing is not really like a uh like verified cuz like it's from the uh like Fiat Crypto is a written in Coq, and then I just ported like for that thing to the Lean, but it's not really like uh 100% like formally verified. So, maybe it's like feature really not >> I I I have a port between them, which I can share. >> Oh.

>> So, but but great great work. That would be nice to connect. >> Uh yeah, so there's a lot of activity on the the compiler side, I think, at the moment. And so, the next talk is also about compilers, and also about MLIR, uh which is uh Tibeesh is going to tell us about basically putting an MLIR in Uh you're muted, Tibeesh. >> All right. So, we have a project called Vair, which is a verified MLIR style compiler data structures uh that we have developing since a while with the like also support from Ethereum. Um so, so the key idea is that

verified compilers is is is a well-established thing. So, they They well-proven. They are sometimes painful to develop and then one of the biggest concerns is that they have been typically quite disjoint from the production compiler communities. And MLIR is a tool that that pretty much is used across classical compilers, maybe even to to model SMD solvers. Uh Uh LLVM is used in Lean as a back end. There's a lot of AI and and scientific computing that's based on on on on LLVM or MLIR. And even like hardware design tools like like circuit are based on MLIR. So so obviously in theory you want to maximize the reuse and then so MLIR in in theory is a tool that enables that reuse. So so it breaks down the the like like all the different users of

compilers and pretty much exposes the individual abstractions as as so-called dialects that makes it easy to to kind of transition from from a classical compiler to to an EDA tool to to a crypto tool, all these kind of things. Um what makes MLIR special is actually not so much that it's a compiler, but it's a data structure. Right? So if you look at the left here, um LLVM and MLIR both use the same kind of data structure, which is um uh data structure to model static single assignment form code. And that means that that whenever you have a sequence of operations, um rather than a purely functional representation, it's actually very easy to jump from a definition A to its first use, the second use, the third use. Um or for

many use to the definition in in in in constant time. And the way that is done is is that MLIR is a uses a relatively pointer heavy data structure to for example to jump from a definition to the first use, to the next use, to the next use, um pretty much um random access on the data structure. So if you think about how to verify data structures in Lean, um to model this in um you pretty much need to verify a double linked list um in seven dimensions. So the way we do that is Lean obviously doesn't have pointers, but but you can just see a pointer as a natural number.

Um you can simulate a heap by using a hash map that maps pointers to to to to the objects in this case operations. And the operations themselves again um refer to pointers um just again using this natural numbers. That means we can directly like like one-to-one mirror whatever MLIR does in its C++ based implementation in Lean. At the cost of a relatively complicated data structure with a lot of um uh hash map indirections. We have independently of this talk, we have an optimization that gets rid of the hash map and makes it actually perform fast.

Uh but conceptually it's just a like a pointer heavy a data structure that that must be uh validated. Um the benefit of this is that we get the asymptotics right. So any kind of algorithm that you implement over MLIR where you iterate over the operations over the blocks where you start rewriting and translating, uh MLIR is optimized for asymptotics. So you get uh constant time or logarithmic time or like time in the number of users um complexity uh for for pretty much all of the operations that matter when you interact with a compiler IR.

Um we also tried our implementation. Here we call it Chainmail. Um compared it against MLIR. And what you see is that that you know on a synthetic benchmark with like like 3000 operations, um we are only 2x slower than than than MLIR. In this particular case, um the the benchmark is likely not bottlenecked on the data structure but but mostly compares like Lean versus C++ code. Uh on dedicated data structure benchmarks, we are roughly 5 to 10x slower if we go through the hash map. If we go through our optimized uh data structure where we eliminate the hash map, uh we believe we are pretty much matching MLIR even constant time. So that that that like like uh constant time optimization is not fully yet implemented and not fully proven. But but the nice thing about the

hash map uh based data structure that's already fully proven. Now how do the proofs look like? So we have three level of proofs. One is memory safety that pretty much just means that any pointer that ever appears in the data structure exists in our hash map. So we don't have any pointers that that that don't exist. Then we have data structure well formedness. That pretty much means that the double linked list or all these different double linked lists in the MLIR data structure are consistent. So a pointer going from to the next element and then from the next element back to the previous one should show a pointer to the base same operation. And then we have an entire layer of functional correctness.

I think there's >> Yeah, you too, sorry. Exactly. So for functional correctness we have an entire layer of a functional correctness. So we have an interpreter for LLVM IR, RISC-V and a couple of other LLVM and MLIR dialects. And what what was the probably the most challenging proof to write? We have a proof that that if you have a local rewrite and you prove it locally correct, we can lift that to the proof like formal correctness proof of the full program. Meaning any local proof applied at any location in your program will um preserve global um program semantics. Uh we use that to build an LLVM to RISC-V backend going from LLVM to RISC-V connected with the sale extraction of of the RISC-V spec also supported by Ethereum

here in the middle. Proofs are validated using Lean's BVD side. And yeah, we have a couple of dialects already. Uh we have a couple of transformations. And it's a relatively active project. So so we get roughly get five commits per day, have 17 contributors. We have close and median PR close time is eight hours and yeah. So please try try it out. Let us know. It's still a very early prototype but but we are interested in feedback. We are hiring if anyone wants to work with us. And the last thing before I advertise an event, I want to very quickly show you what it actually can do.

Um because I think it's quite nice. It's a This is a fast number trans- a fast NTT. Um so pretty much you just have a large MLIR file. Uh it's a textual representation. Um this is a test file. So this is the expected output. This is the the MLIR input. And so so Vea has a tool called vea-opt. Where you can run a number of passes to translate from LLVM to RISC-V. And you just run it on the file. And it behaves like MLIR, like a normal compiler, like you you you take a textual representation of its IR, you turn it into the data structure, you run passes on it, and you print it back out.

And all of that works. It's This one is not completely sorry fee free, but but we expect that to actually soon be completely sorry free. And yeah, then we we can build more of the compiler. Um I want to close with a short advertisement. So in September we have a small event on on like verifying LLVM MLIR in Lean. It's in Cambridge. Uh beginning of September. It's very small, so I'm not sure how many spots we have, but if any of you is interested, just drop me an email, and I'm sure we can find something. Uh thank you so much, and let me know if there are any >> Thank you. Uh and yeah, I've done some work in the LCK, so I can confirm it's pretty sick.

All right. So I think that's the end of the compiler the main compiler section before we get to the smart contract compilers. And so now we can switch to I guess the last topic of today, which is the EVM and then smart contracts. And we'll start with the Monad guest program verification effort that Monad have been doing. >> Hey. Hi everyone. Uh thanks for invite, Alex. Um yeah, um today going to talk a little bit about the the work that we're doing at Category Labs to apply formal verification to the Monad execution clients, and in particular the the guest program that we are extracting from it and sort of working towards uh like E proof compatibility and and reducing a compatible guest a blockchain execution client is

obviously a really sensitive bit of software. There are lots of ways that you can get this wrong with pretty pretty bad consequences, and so we have for the last 18 months or so been going pretty hard on applying formal verification to the actual C++ that we're we're writing at Category Labs in the in the Monad client. Uh pre-2026, um this was slow going. It was hard to make progress. Uh verifying such a large piece of software is is tricky. It's a a huge volume of proofs proof to produce, a lot of code to reason about, lots of sort of invariants, lots of things that you need to to keep in scope, and so we we were making progress, but it was it was slow going. Um

this year we have been able to sort of really accelerate what we are doing by way of like an agentic proof workflow, which I which I will go into in a second. Um our approach uses this tool called Brick from a company called Skylab. Um It takes the the real C++ in the the execution client, embeds it into an AST in in Rock, and provides you this tool called Iris, which is a set of separation logic rules for reasoning about the the actual sort of standardized C++ semantics.

Um our aim is to produce like fully machine-checked proofs of correctness for the the whole execution client top to bottom. So, we've been able to to make much faster progress by using this like agentic workflow going back and forth with Codex and Claude um to to help us figure out how to prove correctness for components of the the Generally speaking, uh we our workflow is to go back and forth stating through stating sort of specifications for correctness, refining them, and then asking the the agent to produce some concrete counterexamples.

We found in practice that they are generally pretty good at finding counterexamples, and you can make a lot of progress towards good specifications by having them sort of attack your your specifications with counterexamples, and at the point where they they slow down and stop making progress giving you counterexamples and ways in which your your specs are broken, at that point you can you can switch over and begin to have them actually produce proofs. generally speaking, they're good at helping with the sort of the creative parts of working with theorem provers, things like loop and concurrency invariants that the the underlying like proof automation tool sets in Brick can't automatically derive.

Um and so far we we've made like we've cut like four person-week times for proving particular specifications down to like a less than a week of effort for for one engineer, and we're internally doing a lot of work to sort of make this accessible to regular engineers and to bridge the gap between the people who are who are writing C++ and the actual formal verification engineers who are who are doing it. Uh we've had some as a a few people have highlighted in their talks, we have a a like certificate of this being being useful.

We are working internally on a a feature for for the Monad network. Um this is not like an Ethereum feature, this is a new feature for Monad where we have a a a commitment scheme for a different abstraction on storage. And so, we've been working pretty hard on formalizing this top-to-bottom. We have a C++ implementation of a new commitment function based on Blake 3. Um there were pen and paper proofs of correctness and we we ported these over to Rock and produced proof that this new commitment scheme can't produce collisions without the underlying Blake 3 compression function also colliding.

The the use of the C++ embedding into Rock also gave us a a useful certificate here in that it found uh a really subtle bit of undefined behavior in the that none of the sort of standard compiler tools were able to to find for us. ASan doesn't flag it, compiler warnings didn't catch it. Nothing else identified this and even prompted to to hunt for undefined behavior. Regular like code review with frontier models didn't didn't find the bug. And we we were able to sort of minimize this and produce an example where we could demonstrate that GCC actually did miscompile the program in the presence of this undefined behavior. And so, we we have an actual

certificate of a safety and correctness improvement in the in the client that we found by using this sort of iterate and prove loop with gigantic workflows. I'll share in the chat after this we have a blog post out today that goes into a lot more depth in on all of the the stuff that we're doing as well as some of the the other places where we've successfully verified parts of the client. yeah, and then to to sort of conclude, this is all in service of producing a more correct, safer safer clients and that carries over to the work that we're doing producing a a risk risk five compiled guest program for for Eth proofs. Um if you don't know that your your client compiles correctly, if it has undefined behavior or behaves incorrectly, then then your

whole or that's off with your your guest program. And so, this is all in service of producing a a safer guest based on the the monad execution clients. Cool. Uh again, thank you for the invite. I'd have to answer any questions quickly in the change of the time. we have one message in chat, but it's not a question. Uh okay, and then uh so then we have uh I guess two other talks on guest programs of some kind. Uh first EVM SM and then EVM cell, which are both very new projects. I'll let you talk talk about EVM SM.

>> EVM SM is um EVM guest written in um assembly. And the risk five assembly. And the idea is that okay, well, uh at the end we have we we we are trying to make a ZK EVM. And we have like risk five ZK EVMs. So, we need some program to run on top of ZK EVMs. And we want theorems about correctness of this risk five byte code. And what's the simplest way to do it? Yeah, maybe the simplest way is to write assembly and write theorems about it.

And there are like program logic sub for assemblies from decades ago. So, we can maybe just use it. And it turns out that LLMs are really really good at it. Um when I keep agents uh one agent in a loop, it produces roughly like 10 theorems per an hour or something. And that covers like four or five basic blocks. And that kind of looks practical enough. So, I was running this I've been running this. And actually, Derek has been running this, too. And then, so we have been producing theorems about risk five assembly. And one of these is like the heaviest piece is the correct division algorithm for like 256 bits divided by 256 bits. And it's proven the um the

division. And it's it's it's it's performance is okay. And also there's a there the lean theorem also tells you the worst-case number of steps, instruction steps. And then for division it's 954. And then like when you run it like the performance is sometimes very good like compared with the other two. Sometimes very bad. But I don't know not very bad but I mean sometimes worse. And then like especially when you divide by small number it's worse. But the nice thing is like you know anybody can find a pulley case saying like yeah here's a faster algorithm especially for like divide by big numbers and here's a theorem and the theorem in lean is not broken so it's you know guaranteed to division and it's very easy to review.

And I can maybe merge it very quickly. there are some uh other efforts going on like not all op codes are done. Like there are some like exponentials and the signed divisions. Basically these things are in progress because like they did have to wait until the the components are finished like the exponentials use multiplication and the STV uses the user division or its subroutines. So like they were kind of waiting until these components are done. Um the comparison against the say risk five spec is still in progress. I mean I I I I guess this is the this is becoming painful like every every time I say formally verified I have to like

put an asterisk around it. So like um this is becoming more of a priority like We have been running the test conformance and this have the the this There are still errors but these are mainly about the gas accounting and we have confidence that the this approach works in the sense that there are like enough amount of memory to do all the calculations. Um we still need a specification in lean about the state to this execution client and then just for smart contract verification, but also about like parsing the block, parsing transaction, parsing receipt, and so on.

And you know, in a call like this, when I say this, like you know, somebody might remember and come up with one. So, that's why I'm saying this. Thank you very much. Any questions about this? And otherwise, we have a fairly related talk, which is EVM sell, which Francesco can tell us all about. >> Hey guys. Yeah, so I'm Francesco. I'm part of the ZK EVM team at the Ethereum Foundation. I kind of stumbled across the effort that you know, the EVM ASM effort, and it became particularly interesting to me because I've been primarily focused on

integrating ZK EVMs into consensus clients, and I was just particularly interested in how we can kind of harden the security argument around it. So, I explored EVM ASM, and then essentially stumbled across sale. kind of set about essentially defining the EVM in sale. So, those that don't know, I'm sure many of you do, but sale is essentially a language that is purpose built for defining ISAs and the semantics of instructions. So, So, yeah, we've essentially got an initial implementation.

The way that we've structured EVM ASM, we've essentially defined kind of the core opcodes, the semantics, similarly for gas and core frames, and then all effects go through kernel, this kernel interface. So, we have a kernel interface for accessing state, making modifications to memory, making modifications to transient storage, etc. So, it's pretty kind of explicit in that regard. And what's nice about the the the sale implementation is it has pretty rich tooling. So, you can extract it to various different back ends that allow you to do various different things.

I must say that this is still, you know, very new. So, much of this I have not done personally, but I believe RISC-V has been defined in sale and and many of these kind of flows have been evaluated for that. So, you know, the the the the assumption is that it should work similarly. So, kind of the the next step would be to extract the EVM sale specification into lean and then, you know, potentially try and support the EVM ASM effort in time of in terms of being a specification to test it against. And more generally for any kind of RISC-V guest, we can evaluate compliance.

There's also Isla Reese. I'm not sure if I pronounced that correctly, but it allows for symbolic execution. So, this is this is quite interesting because we can potentially, like, automatically generate test vectors. So, if we make, you know, introduce new EIPs or new features, we the the the the hypothesis is is that we should be able to automatically generate test vectors for the new feature and then use those test vectors to you know, to evaluate various clients.

And additionally, it could potentially be extended to for use in contract verification. I have compiled this down to see. We have 100% of the the East test, both the state test and the blockchain tests working well. They're passing essentially. Um, we also are able to compile this down to risk five. So, um, we I've compiled this down to risk five and, uh, simulate or emulated it on, uh, Spike, the Spike emulator.

Um, and I believe you can also extract to rock as well. Um, just, uh, yeah, I guess it it makes sense to just note that, um, the memory and, uh, kind of state interfaces are currently defined as kind of abstract using, um, C header files, which are then subsequently kind of satisfied in the target environment. Um, similarly for the cryptographic operations as well. Uh, this is a moving like it's it's, you know, it's under rapid development, so um, the current commit in EVM sale is is pretty old, um, and I'm hoping to commit the 100% uh, like test, uh, compliant version within the the next day or so. Um, so

yeah, that's all for me. Uh, yes, there is anything to tell about setting up uh, I guess the call with the the sale people, uh, to talk about so I said to be honest I was even forward with selling Cambridge, uh, but I guess we'll keep things moving to try to not run too over time and so the next talk will be about the verified by Google compiler I think also the sizing this case, uh, and Ramana's going to talk to us about what I think is the most complete compiler verification effort for smart contracts.

So, let me share quickly. >> Thanks, Alex, for the the introduction. Hello, everyone. I'm Ramana. Uh, Uh, I'm I'm speaking on behalf of many different organizations. Viper, which many of you will know is one of Ethereum's smart contract programming languages. Um, Verifier, which is the project that I started to do formal EVM semantics and smart contract verification. And Sequence, which I co-founded, which is doing formal verification for everything. And we're in particular doing smart contracts at the moment.

this talk is about the verified Viper compiler effort. But as anyone who thinks for a second about what compiler verification means, uh, that includes formal semantics for the target and source languages. So, I'll start since we just heard from two speakers about EVM semantics, I'll start with the the bottom end of the compiler, which is on the left here, the Verifier Verifier EVM semantics. Uh, is I would say a production quality executable formal semantics in the whole four theorem prover. Uh, we had a for Prague and it's recently been upgraded to Osaka and it's going to be upgraded to Amsterdam as soon as that hits mainnet.

yeah, this is um, validated in multiple ways. So, if this EVM sale, uh, that we just heard about, you know, doesn't export the whole four, we could think about doing a proof for an additional bit of validation. But that doesn't exist yet. So, what we have for validation is the East test suite uh, with about 99% correctness on that. And the reason it's not 100% is just because execute I haven't done like a fast execution mode for it yet. I'm doing execution in logic and so some of them time out. I can run them for longer and then we'll hopefully get the 100%.

but beyond just executing the semantics, we can also prove things about the semantics. So, we have validation of semantics both on passing the test, but also proving properties about it. For So, for the EVM semantics, we prove things like gas monstrosity and that a call fits inside of state frames. So, when you make a call, you only touch the storage of all this all the contracts that got called during that call, but not anything else. So, the rest of the machine stays safe, and this is useful obviously for proving things uh if you want to do um smart contract verification at the level of bytecode.

Uh so, in addition to the EVM semantics, because we're doing compiler verification, we also have done the formal formal semantics for Viper, the programming language, and for that we have validation for the of the semantics just in terms of the Viper test suite. So, the Viper language has its own test suite for its language, and we check um we don't have full coverage of their test suite at the moment, but that's that's ongoing work, but we have a pretty comprehensive feature coverage, so we cover the entire Viper language. so, this this compiler verification project, I'll speak a bit about the rest of the details in a second, but it's currently kind of paused because Sequence is working um well, it's kind of paused depending funding. Like, we get a if we get funding or contributors to go finish the

rest of the compiler verification, we'll go ahead and do that, but we are pursuing opportunities to do smart contract verification and out side of Ethereum formal verification. for the for the time, we have limited bandwidth, limited um so, that's why this is this is in the state that it is at the moment, but we it'd be great to finish it. yeah, so uh part of that it builds on top of the Viper semantics. We have a program logic for Viper, uh it's like a whole logic that lets us do smart contract verification, and we're doing that with the our Agentic prover agent that can automatically prove correctness of many smart Um so, when it comes to the compiler correctness stack and the compiler

correctness proofs, uh we had a big effort on this in the beginning of the year to get a definition of the Viper compiler, which is the also like production-grade compiler. It's modeled on LLVM, or it uses many of the same concepts as LLVM, and it does many optimizations. yeah, we did the definition of the compiler and proofs and the proof framework for infrastructure framework for many of the optimization passes and compiler passes. Those operate on the Venom intermediate language, which is Viper's main intermediate language for its compilation. Uh so, those are about a half done, I would say. Like, we've got about 10 of the passes proved completely and then partial proofs for many of the other um compiler passes.

We've also taken a stab at the other two bits there, which is going from the Viper source code into this intermediate language for the lowering phase. Um and the final bit of Venom to EVM bytecode. Uh those are kind of scaffolded, but the proofs are still open. Uh so, that's the current status of the verified Viper compiler. Um as Alex said, it's uh it's a big project. There's been many, many lines of code in here. A lot of them are AI-generated, of course. Uh and a lot of them are with our um prover agent, not just using a bare LLM, but we've got an agent to do the proofs for us.

Um and yeah, I'm happy to take questions on that. >> Uh thank you very much. I'll just see if there's any questions. Uh but yeah, this is this is a thing. Very, very cool work. And then I guess have you played around with sorry, I lost contracts? Yeah. >> Oh, uh you're trying to put contracts like Solidity to Viper? >> Uh yeah, or any uh I guess Solidity is the main one, but yeah, any any other language. >> We have We haven't done We haven't done like a serious go at it, but we've thought about it. And it's obviously as soon as someone comes to us and says like, "We want We definitely want you to do it, we'll do it." And um I think I just remembered also that Yoichi said that he wanted a a formal semantics for

the full EVM, including the blocks and the transactions and like the full state machine. And that we we have that here. like verifying models all of that. So if you want if you want an EVM semantic formal EVM semantics to look at I suggest taking a look. Do you want Do you want to upstream your semantics >> to sell cuz you could have then extract for sell the whole four and validate them. Or like at least validate that your streaming to sell is consistent. >> I think the way that I would rather do it than upstreaming is to import the EVM sell semantics and then do a proof of equivalence cuz then we get to keep the semantics in the format that I've defined it which is suitable for doing all of our meta theory proofs and doing the compiler proofs. So I think it's

like there's different ways of formulating this. >> Yeah, yeah, I see your stream very lucidly here. Like you you would keep the whole four ones just validate whatever is in sell against the whole four ones. >> Yeah, it would be really it would be really nice really nice to get a proof of correctness there. Proof of equivalence. >> Yes, so so one motivation is if we if we do move towards having fewer guests then having spec diversity and cross-checking the specs will become more important. >> Exactly, yeah. Spec validation is very hard. Uh okay and then uh next up is Veritex uh which is a a recent effort as well to have smart contracts in the >> Sorry, uh real quick could I ask a question before we proceed? I I I don't know

the the the raise hand in Zoom. Um I wanted to ask uh for the purposes of uh formalizing Viper and etc. how do you think about gas introspection and like how do you connect like the high-level spec to like the the low-level >> That's a good point. Yeah, so if I Viper does not have does not have gas like you kind of assume that your contract you know gets as much gas as it needs um in the Viper semantics. So it's not modeled there, but you do have the low-level up codes like you can ask for how well you can do tricks in the EVM or ways to look at how to introspect on the gas.

part of the compiler proof is probably going to be the hardest part and it's a bit that we have we haven't finished it yet, but we have a plan for how to do it, which will involve adding a gas oracle to the Viper semantics that lets us say what like how much gas you started with and how much you actually use at any point. And we don't calculate that, we just take it in as an oracle input at the start of the semantics. And we know that such numbers exist for every time gas is inspected because you know, there's a real underlying machine at the bottom. Um so this is a kind of informal sketch of how I would do that proof, but it remains to be seen whether or not it gets done formally.

If that makes sense. I would just talk about it offline as well. >> Yeah. So get gas is a nightmare. Gas is a nightmare thing is the real deal. Um okay, and then yes, so the next talk fairly related, which is the timing Verity. Verity is I guess a different attempt at verification, which is having a lean DSL to which you can port things and then there's some compiler verification effort that's also on the way. Do you want to let me know if you want me to share the slides or if you're sharing?

>> Uh I'll I'll share if that's okay. >> Yep, go ahead. Can you see it? >> Okay, perfect. So hello everyone. So I'm Ben from Verity and I didn't know really how familiar you guys were with formal verification and so on, but considering all the all of the talks I I listened to today, you guys are pretty familiar with formal verification from what I understood.

So I'll pass the beginning of the of the presentation just to present Verity as Alex said, Verity is a lean DSL to write a smart contracts and the main goal for us at Verity is to be able to model Solidity smart contracts, even though we do compile to Yul and then to to to source. Um to to EVM bytecode, my bad. Um the goal for us is to model your Solidity smart contract in Verity and then be able to formally verify it directly in Lean. So, three-step process. First, you model your smart contract in Verity. Second, you write the specs, the theorems, the the invariants, you can call it whatever you want, and then you send an an LLM to

write the proof. So, in general in the classic formal verification space we had before LLM were so good. So, basically before um in 2025, basically, um well, we had SMT provers do the prove it part where basically they're going to try a lot of possibilities and sometimes the time the timeout. And the problem was on non-linear code, which is a lot of code when it comes to DeFi, well, the timeout or we take an as an assumption all the mathematics in the protocol, this kind of stuff. Um, so, here uh the the big change with using Verity and other formal verification tool that use more

reasoning and LLMs to write the proofs is that you're able to do unbounded formal verification and you're not using raw compute, you're using an LLM that is actually able to reason on the code and to prove that it's correct using mathematical arguments. Uh, so, we we we do that. We model, spec, and prove and prove code. Uh, so, to to give a small example of what we've done, so, we worked a bit with Lido V3 and yes, very very simple function, for example, this function we model it in Lean in in in Verity and sometimes we have we do have the features at the same level as Solidity, but the goal is to is been like four months we're working in

Verity. The goal is to have all of the features and to have feature parity with Solidity and not really to to reinvent a new language with original features and and better features. Our goal is really to modelize Solidity. So, we will have something very very similar to to to Solidity. And once you you've done that, you define the invariants. This is one of the invariants we defined for for the Lido smart contract. In that case, it's basically the fact that the vault is solvent. So, you have more ETH behind every stETH. And when you do these these specs, of course you you write it in in Lean, and it looks like this in math, but you can also formalize it in English.

All of that in the vision that in a future where everyone is live coding everything, you do not really want to actually audit code, but you you want more to audit specs and to have a mathematical proof that the specs cover everything in the protocol, no that the specs the implementation matches the spec. And then you have to audit basically only the spec and not the implementation anymore, which is like way probably way easier. Even though it's not that easy, but it's more easy than actually doing the whole implementation.

And then what we do is that we on the third the third step, what we do is that we send an LLM and we ask him to to write a mathematical proof in Lean that the implementation, which is the modelization here, matches the spec, which is a bit like the theorem the the invariant. And and to to verify that, the theorem the LLM will do Lean build. And if it fails, retries, retries, retries, retries. And like this, you have an energetic loop. And if I I actually have on my laptop right now four four different protocols being proven, and it's been like 2 hours.

And my laptop is in complete PLS mode because it's been 2 hours Codex is running on the laptop to try to to prove. Doesn't succeed for the moment, but for the moment, but I'm sure it will. So, it's preferable to do that in the cloud. My cloud I had a cloud problem today, so weren't able to do so. But at the end, you have the theorem that is proven, and the theorem is basically on the example of Lido that stETH can only be minted if the vaults total locked ETH exceeds total minted stETH. So, vault solvency in that case. And yeah, that's that's a bit what we do at at Verity.

Um if you guys want to prove software, want to prove your smart contract, well, you can you can send me a DM on on Telegram. And if you just have questions, please do the same. Send me a DM on Telegram, and and we can discuss it. >> Thank you. And then, we've got two more talks left. Uh so, the first of these two is going to be Leo, who's going to talk about his recent uh fun adventures in bytecode and AI and formal verification in Lean. >> Yeah, do you want to share and give me your link?

>> Yeah, give me 1 second. >> There we go. Yeah, so this will be a short one, likely. It's a good segue to come after Verity. So, EVM Smith is is an experimental framework I've been playing with with the idea of uh well, the EVM as an inspired idea of writing um EVM bytecode directly.

So, not RISC-V, but smart contracts. And having AI write the bytecode directly and the Lean proof at the same time. So, combination of Lean and AI. And the first experiment that I that I did was actually to try to see if this actually makes any sense. So, I'm using the Nethermind um EVM Lean uh repo that has the the Lean spec in in Lean uh sorry, EVM spec so, I wanted to try to prove something complicated. So, I had the AI write the a small uh wrapped ETH contract, not the same as as the standard one. Doesn't have a transfer function, only deposits and withdrawals. But, the property I was

interested in was solvency. So, basically, that the contract has um enough ETH to pay back um all the all the people that that have deposited money into it. And this is a pretty difficult thing to prove. Um it's an inductive property over any amount of transactions that you can um that you can have. And but, AI was actually successful at at proving this. It took many hours with Opus 4.8, I think it was. Or 4.7, not sure. Um one of these. But, it was about, I guess, like 10 10 to 15 hours of um of thought.

Um but, I think this is pretty impressive, honestly. This is is not the first thing that I tried immediately, but like the definitely the most complicated one. And I think the fact that this was successful actually probably means that you could prove anything kind of reasonable that you can actually argue about your contract um as long as it has that property, of course. the other thing I wanted to check is what what if I take a something that Viper has literally compiled? Can the AI actually understand enough of the bytecode to make modifications and improve the equivalence of the two um bytecode? So, the idea here was to do like custom storage layout thing, where we don't want, for example, the Keccak um

appended storage um slot for her mappings. You want to use something um, that doesn't run Kachak. And this was actually pretty easy for for Glide. It immediately was able to prove equivalence of the optimized version and the the ones compiled by both Solidity and Viper. Um, I think I had both. And that and and after these people a lot of people were like, "Yeah, this is looks great, but who's going to be reading these these theorems?" Like a handful of people can actually read these theorems and and reason about what they actually mean in the context of EVM.

So, the next thing I wanted to do is like, can we actually have a small EDS inside Lean that kind of looks like Solidity, has some formality to it still for some formalism, but lets us reason um, about it in a bit more high-level, so then AI came up with a very simple DSL that was only enough for rep ETH cuz they didn't want to make it too um, generic at first. And I think it it actually looks looks pretty nice. Um, so like basically 100 lines of um, of DSL code in in Lean and I think this looks pretty pretty nice. There's a few more properties that look look like this as well in in a similar DSL.

Um, and there's a point that I think Yoichi was also making before that like, um, do we even need a compiler at this point? Of course, it's half what I'm saying how is half half trolling, but yeah, it's it's it's pretty impressive what it can do in the context of writing the bytecode and writing the proofs immediately. And if you can have high-level specs um, like these properties that kind of look like the high-level code anyway, and people would be reading these only and not having to read the whole bytecode.

Um, I think it is it is a possible future. So, yeah, so there's blog posts about each of these items um, in the first link. The framework itself is into a second link. So, yeah, thank you. >> I can I just clarify something? what is there any VM semantics in this work or is it kind of like a you know, you figure out what the instructions mean as you need to. >> Yeah, uses not Nethermind's semantics, the EVM Yul in repo.

>> Oh, okay. >> And I'll put a link to the EVM Yul stuff in in the chat. >> Did you Did you make some some comparison about the the cost of the proof uh comparing to other methods? Just with LLMs, I mean. >> Um no, not really. I only tried with with Clyde. I saw that your guys did this comparison recently. >> I I mean, yeah, we we we made a comparison on the models, but not really on the method. The method was always using Veri Chi and not directly the Uh and that's why I'm surprised that like I think it it

it could be very expensive using directly the bytecode. It It should be like very hard for for the the proof to actually pass comparing to to Veri Chi. That's That's why I'm asking. >> Uh from these experiments it looked it looked fine. Um anything that was like the this the solvency property with reentrancy and everything also took a long time because the EVM Yul in repo wasn't like super fitted for this. So, it it didn't It had a lot of Yul stuff, but not a lot of EVM scaffolding. So, part of these like 10 to 15 hours that I mentioned were actually writing all the scaffolding to be able to reason about EVM directly.

So, it's hard to say exactly what what scaffolding, what was the property proving. But when I tried smaller things like the manipulating the EVM bytecode directly to write this custom storage layout and then proving it it was immediate I don't know matter of seconds or minutes. >> But I would expect the solvency to still be hard even if we had the scaffolding already but I can't tell you exactly how how long it took just for that. And that was office 4.8. Sorry. >> It might have been 4.7 because this was I can't remember exactly when 4.8 came out and the the first one was like end of April beginning of May ish so might have been 4.7 but could

also been 4.8 but definitely not fable. >> Okay, thanks. >> Okay [clears throat] and then we've got the last talk of the the last talk of the day which is by Anya from Argo and this is I guess a bit different which is just looking at incentive security. >> Uh off you >> Thanks. So yes, I'll be telling you a little bit about what we're doing at Argo and like Alex said I'll be talking about incentive security that we formally prove with act. So I'm kind of hoping that most of you have heard of act before but just in case you haven't when I say act I mean this pipeline here. Um it's like a specification language in

which you can describe a behavior of your smart contract um derived from the source language probably and then what we do is prove it equivalent to the actual EVM bytecode using the AGVM um symbolic execution engine and its equivalence checker so this is also maintained by Argo. And then the real reason why you do it because then we extract uh sort of a state transition system a high-level way to reason about the smart contract we extract it to rock and lean and then in that you can then in Lean for instance define and prove properties like solvency. So we did solvency for AMM.

Um but I want to talk to you about what we are currently doing. So this is the work in progress part. Um we are not interested just about code security, but also economic incentive security, and we want to formally prove it. So we use the already existing act spec for your smart contract, and then we automatically generate a model to a tool that is called CheckMate, which is designed to prove incentive security. So what do I mean by incentive security? It's that the users or players are incentivized to follow the honest protocol, right? And incentivized it means there is some monetary reward for when you're behaving according to the

specified protocol, but additionally, you also want to make sure that the honest players cannot be harmed, no matter how other people or agents behave, and that the protocol itself is collusion resilient, which means "Hush hush, don't tell anyone what you're doing" doesn't pay off. You will always be worse off in the end if you're doing something that is not according to the protocol. And these three properties they have like a mathematical formulation that the CheckMate tool automatically checks using the SMT solvers. So what we're doing is going from the act spec to CheckMate in an automated way, and I would just want to give you the high-level idea of how we're doing it. So the idea is that the

players are the addresses of your smart contract, and then the actions they can take are the transitions, so public functions of your Solidity contract say, right? And we then set the caller to be the player we're interested in, so the specific address we fix. And then what their payoff is in the end, the economic incentives, can be defined from the state variables that are available to you, balances, or other storage variables in the contract. And the trick is that this final model, this game tree that we produce, uh respects the call graph of the smart contract. And additionally, all of the preconditions of the transitions, think

like require statements in your code. So, obviously, I'm hiding a lot of detail in this picture here. >> But I just wanted to give you like the idea of of what you can do uh automatically from a smart contract to the economic incentive. one other line of work that we're also doing is replacing this equivalence check uh that is done in ABN from something that you can prove directly in Lean. So, we will call it, I think, Equivian. Uh it's not open source yet, but it will be soon in a few months. So, the idea is exactly to do the bytecode equivalence with spec uh and the um some semantics of the EVM bytecode, and you

can then run agents to to to check for equivalence. Um so, I didn't want to spend too much of your time. Uh so, I will stop here, and you can ask me questions if you if you like. >> Yeah, thank you very much. And so, I think if you're looking at Lean, you might have seen uh there's an econ lib that started in Lean recently, which would probably be a good place to formalize whatever, AMMs and other incentives and economic mechanisms that are implemented in smart contracts.

Uh and then you could tie this all to specs. >> Mhm. >> Uh okay, so I think that concludes all of our talks. Uh I think, as usual, the East Coast call is running off by about 30 minutes, uh which is right on time. but that's basically it for today. If there are no other questions, uh I'm going to see you all invite every speaker to put their slides in the chat. and uh see you on August 14th to I guess talk about binary fields again. Maybe there will be an executable uh specification for flock in OCaml. Maybe with a compiler. Uh who knows? We'll We'll find out in a bit over a month.

And maybe we'll put some ideas together to be solved as well by then. Hopefully. Uh so yeah, thanks everyone. Uh I don't know if you have any final comments, Justin? Uh and advice to you all in August. >> No, I just wanted to thank you, Alex, for hosting this call. This was great. And thanks, everyone. See you very soon. Bye, guys. >> Bye-bye. >> Bye. >> Cheers.