Ethproofs Call #7: Guest programs

Transcript

intro

Hey, let's get started. Hello everyone and welcome to EF proof call uh number seven dedicated to EVM guests. Uh we have about 70 people on the call and people are uh trickling in. Let me quickly share my screen up. Okay, so um as usual uh we have a telegram group. Uh there's about 500 people in the group now. Um there's some good conversations. If you'd like to join, just scan the the QR code or join with the link uh below. Um of course, uh probably most of you watching this video uh knows about this. In order to have a

ZK EVM, we need two things. One is we need an EVM implementation, which we call the guest program. And we're going to compile that to a ZKVM. And in 2025, we made a huge amount of progress on ZKVMs, their performance and the diversity. Um, and um, I feel like there's more work to be done on the guest. We've mostly been to a large extent relying on revm and we need more diversity there. So in 2026, we're going to have two uh, call series. Um, so in addition to the EF proof core series, we're going to have a a a new ACD breakout um called

the L1 ZKVM uh ACD breakout. It's going to be led by Kev. It's going to happen possibly monthly uh possibly bi-weekly. I guess Kev will tell us all about it. And it's kicking off very soon uh in a couple weeks uh on the Wednesday, February the 11th. Um but yeah, going back to the e- proof call series, we're going to be focused in 2026 on uh security. So in addition uh to the guests, we're going to be discussing pad on two uh on March 20th.

Um I'll be sending out the the poll for the calendar invites uh shortly after this call. We're going to be talking in particular about the uh Pedon prize that was announced on Twitter recently. That's a $1 million prize. Uh and then there's going to be all sorts of other miscellaneous security topics uh scheduled for for this year, including for more verification. Now, um in order to um kind of introduce this this new topic of guests, uh Farah has created this new guest tab. Um so right now on e proofs, we have four different guests. Uh and as you can see that of the 12 provers uh 10 of them are

using revm and we we're kind of slowly uh building up the the diversity and what I'm expecting will happen over the course of 2026 is that this tab will really blossom uh and expand significantly. Now um one reason for for having this call is that there are some uh EL um clients that have that are written in in ZK unfriendly languages like like like Java. Um and so really there's kind of two options uh available. You can either rewrite your state transition function or you could adopt uh an existing one as your as your as your guest program.

It seems like potentially Bess will go down the rewriting path, potentially Aragon is going down the adoption path with EVN1 and and Silkworm. Um, and you know, there's still potentially a decision that a final decision that needs to be made uh for for GE, but all of these entities will be uh speaking uh today. Now, in addition to the guest tab, we now have a new spreadsheet called the the guest tracker, which basically tracks all of the implement EVM implementations that that I could find.

Um, I found about 40 of them and basically try to uh bubble up those that are most uh suitable to be used as as as guest program. So, you know, in addition to all of the implementations that come from the Ethereum ecosystem, whether it's the L1 or the L2 ecosystem, we also have some implementations from um other L1s, for example, Monet, Polka Dot, Falcon, and Near um and maybe um some of these uh implementations which are securing, you know, sometimes billions of dollars uh today and have existed for for for several years. um could be basically adopted as uh guest programs

and so we'll hear from some of the maintainers of these EVM implementations. So today's going to be an extremely busy call. We might um o overflow and overrun beyond the the two hours that are that is slotted. We have 14 presentations uh each um five minutes. So, we're going to have first the um the EL teams uh present what their plans are and um and you know what EVM guests they've tentatively adopted so far. And then we're going to be talking about other candidate uh guest EVMs, most of which are um kind of outside of the uh the Ethereum ecosystem. And then we're going

to have a closing talk on Zero OS. But before these uh 14 presentations, we have 10 uh quick updates uh as usual, two minutes each with some Q&A. And uh yeah, without further ado, I'd like to invite Mo uh to talk about uh Pico and uh achieving uh real-time proofing on 16 GPUs. >> Uh hi Justin, this is Alan. Uh I will be presenting the recent updates on the pico present. Uh >> perfect.

Mo Dong: 16-GPU proving

>> All right. Yeah. Let's see. Can you all see the screen? >> Yep. >> All right. Cool. Yeah. So, uh I'm going to present some of our recent updates on pig laws and some intermediate updates here. And then three months ago uh we were releasing this virtual version of pico prism that was deployed on uh 64 GPUs uh where we employ this divide and conquer method to use subblocks uh to uh to run the whole uh block workload. So basically each block is divided into seven subblocks and approved on seven

GPU machines each with eight GPUs in total and then they were all aggregated on the eighth G eu machine. So with this divide and conquer we were able to achieve almost the real-time proving uh we were able to prove the more than 99% of the Ethereum blocks and 12 seconds were out of blocks uh in total like 7200 blocks on executed on September 1st 2025 and since then we have been developing uh many different updates as well as optimizations for the current architecture because obviously 64 is very far from the uh 16 GPUs. Um so uh there are different different optimizations that we have

been employing. Uh for example, we have this uh updated AOT compilation compared to what we originally have which was the interpreterbased emulator. Um so the ahead of time uh emulator is replacing the our original interpreter based emulator uh with native compile RO code generated directly from AL library. Um so um we just remove those pre-instruction decode and dispatch overhead during our original emulation. So the emulation whole procedure will be able to be accelerated up to. So this is one of the biggest progress that we have and then there are still many different optimization that we haven't applied but

yeah it's ongoing there's also data to >> yeah um yeah so final result is like this we still have like uh yeah many things going on uh but we are now able to prove the more 99% of the time under 12 seconds uh for exactly the same set of blocks now. So yeah, so um uh this is the intermediate uh and we hope to see that we were able to prove all the blocks recent blocks within 12 seconds or even less than 10 seconds real soon.

>> Yep, that's all. >> Okay, perfect. Uh just as a heads up, I'll be keeping strict timekeeping because we have a very packed schedule. Um, congratulations uh, Alan and it's good to see the AOT uh, optimization uh, being implemented everywhere. Uh, and great to hear that you have more optimizations coming. That's that's that's great news of course. Um, next up we have E from uh, Axiom. Hey everyone. Um, so yeah, I'm here to present OpenVM 2.0 up uh our recent release uh which uh proves Ethereum in real time on 16 GPUs. Uh we've updated

Yi Sun: 16-GPU proving

OpenVM to now have 100 bits of provable security and a proof size of under 300 kilobytes. Um onto the numbers on a string of recent uh mainet blocks starting from block 24 million. You can see the histogram of proving times on the bottom left. Um we got a P99 proving time of 11.8 8 and an average of uh 6.7 seconds on a cluster of 165090s. And we also introduced a new benchmark which is to actually assess the proving performance of OpenVM on a benchmark called coremark which is typically used for embedded CPUs. And so we looked at the scaling of the proving speed uh as the number of GPUs increases. And we're

able to go from 11.4 4 MHz on 1590 all the way up to 139 MHz on the full cluster. And finally, like um Alan was saying, we also implemented AOT execution and we're able to execute R 5 at 3.8 GHz. Um so all of this is powered by a new multilinear proof system backend that we've implemented for OpenVM uh that's called Swirl. So it's based on WR and has particularly fast recursion. Uh so you can check out the details on the OpenVM website and we just posted a more detailed uh release blog yesterday. Uh happy to leave a few seconds for questions.

>> Perfect. That was super quick. Uh I guess one question is uh okay there is a question from clim already. Do you have an idea why the histogram of latency pics has a second mode around 11 seconds? We're we're actually very curious about this as well. We're not totally sure. One hypothesis is that I I think Aztec has been posting a lot of blocks which use very heavy um elliptic curve oper pre-ompiles and our guess is that these are the blocks that contain those operations, but we're not 100% sure. >> Cool. Um and I guess similar to Alan, do you feel like there's more optimizations to come or are we starting to reach saturation in optimizations?

Uh no, I think there's quite a uh bit of things on our road map. Um so yeah, hopefully we can deliver some more improvements in the coming uh weeks. >> Perfect. Congratulations. Um next up we have uh Jun who will talk about Prism ZK testing. >> Uh hi it's Jun. So I recently worked on the uh optional proof with aka EIP 8025. So uh let's uh I'll prepare a one minute demo uh video and before that I'm going to just briefly introduce about how this local network works. So uh it consists of eight nodes and there are two stateless node here which means it

Jun Song: Prysm zkAttesting

doesn't have e at all. So uh there's an external prover right here to submit execution proof when it receives a block go events from the network so that these two nodes can follows the chain and um um attach to the chain so that it can participate to the uh consensus as well. So yeah let's see a quick demo here. So uh in the left side I'm running a ctois and in the right side I'm running a dummy prover here. So yeah, I'm just I'm going to skip some very boring stuffs and yeah uh there are uh two terminal sessions following the load here. So uh the first one is the safety node that receives a proof from the prover and the

right size is the u stateless nodes that receives proof from the gossip sub. So uh if you want to see in prism that uh if your node follows the chain well uh you can see this kind of low sync new block sync new payload and you can see uh those two logs are appeared uh repeatedly in both of the sessions. So it means that it can uh follows the chain at all and maybe I can forward here. Uh if we see Dora um let's see uh there are some attestations happening.

So uh there are no uh validators part uh there are all validator participating in in the consensus. So which means uh it can follows without uh it can follows the consensus without the e only relying on the external approver and verifying itself. So that's it from my side. >> Very nice. Um do you know when you'll have a mainet validator running this? >> Uh I'm not so sure. So uh there is uh still ongoing discussion about the overall architecture uh about the EIP8025.

So I think uh yeah this is just a uh exploring some feasibility. So uh I I guess we are targeting the Gfork but yeah we have to discuss more. >> Okay, perfect. Um and I also look forward to potentially using it on my validator. Um I see we have a question for for Eon in the chat from Sergey. Do you know if Scroll L2 plans to upgrade to OpenVM 2.0? >> Yeah, obviously the final decision would be up to Scrolls governance. Uh but yeah, that's the plan.

Tamir Hemo: Hypercube release

Okay, perfect. Uh, next up we have Tamir who will talk about uh, Espeon Hyper Cube being released potentially. >> Hi everyone. Um, I wanted to announce the opensource u of hyper cube and um, so we released our version 6.0.0 0 beta which is the beta release of hyper cube to crates and also it is available uh on GitHub and one new thing about it is the GPU code is also under our MIT uh Apache 2

license. Um the audits have been completed and we will have a mainet release uh very soon but you can try it out and um and let us know all the things you find. Um and in the future we also have um improvements to proof size as really more bottlenecked by audits at this point um and more to come. Wow, absolutely amazing. Uh Kev is asking what was the reason for going full MIT Apache.

>> Yeah, I think we realized that this is like something that is important for the community and for like resilience as as it will be used for L1 proofs. Um, I think that everything is really just about we're we're still trying to find a balance of like uh the business and the um public good kind of place here. So currently our business model is like proving a lot of L2s and you know our collaborations with with those ecosystems.

Very nice. On the slide that I'm showing here we have um basically some updates highlighted in in in yellow. So we have now openVM and Pico that can do 10 kilowatt proving and we have SP1 which is now uh dual licensed. Um and we also have some uh some uh improvements on on on the proximity gaps and the provability. So this uh table is very very quickly uh becoming all green which is uh absolutely amazing. Um, next up we have uh Clemore Walter who will talk about uh Star.

Clément Walter: STARK-V

>> Yes. Yes, I'm here. Uh, how do we share the screen with I mean I'm with Zoom. >> Um, there's a green button in the in the bottom with share. >> Ah yeah all screen uh authorizing. Oh, I I so much never use Zoom. >> Um, >> do you do you see the screen? >> We can see your calendar. So, if you um share Okay, that's better. >> Yeah. >> Anyway, so yeah, this is a good presentation uh about this project that we made during the past three days with boat. So, we built a risk five prover with stackware tech. So we we were very

close to of course everything stack has built but as you know stackware is focused on their own stuff with Cairo and stark net. So we said okay why not building a ris prover based on the experience that we had. So it's more of an engineering perspective of a recent build of a risk five prover. I asked GPT to generate this ugly image just to have something a bit nicer because I draw the slide really in 15 minutes later on today because that one was off. So the tagline is really a new agent native risk 5 RV 32 IM program because we did this like a months ago and it has been 99.9% AI code written does not mean that we have not read the code it means that we

have been really by design from the very beginning been working with the fact that the AI will write the code and we will be focusing instead of the spec and we will leverage the agent to do the things that usually human don't want to do to make sure that we can sort of have something that is both auditable more easily and smoother. So my first side was like okay the team so is not here and I just just to be clear this is not a kakarat project kakarat does not exist anymore it has been sold to to zama this is not a starkware project this is our own so don't go to stare people has something don't speak about kakarat is and so agent native what does it mean that uh we build from scratch when you

want to build without agent you're like okay I'm going to reuse libraries or so because you want to save on time but the agent they write code faster so you don't want to to bother using library you can tell the agent take inspiration from this library but generate new code I mean if at some point you get much more flexibility on how you want to handle all the complexities of mixing different parts of logic they have the knowledge the agent knows so you really spend 99% of the time in plan mode reviewing the plan what do agents want to do and the very similar thing I may stop here because then example it's macro inensive codebase. So instead of writing a lot of code, we ask the agent to write the macro the macro the macro that we can focus as human on defining

very high level things in terms of what we want to prove and so this might be the last last slide because two two minutes is very short like for the air for the table for example we wanted to be able to express almost in markdown the tables and the constraint. So we have asked the agent to write a macro so that we can define the the all the tables of all the prover with this single macro and then we generated for example a risk interpreter and directly in the risk five at compile time we trace the operation and we generate the witness based on the table that we had in the macro before and thanks to macro at compile time you have a lots more lot lots more guarantees that you are not mixing up values in different places in

different tables and so forth. So that's why also be able to be quite fast but two minutes was fast as well anyway. >> Okay. Thank you. Um we have a question. Uh do you also review and understand all the code the agent has written? >> Yes. Yes. Yes. Yes. So the pen base is 100. I mean it's very readable. Everyone can go and look at the stack five codebase. I have reviewed all the code myself. I don't merge blindly. This is not a front end project. This is a real project. But Phil it means that you know it's not the same reading and writing and the agent has writing cities that you don't and then so you can focus on the writing and macro. I think the macro is really a big unlocker focus and asking macro to the agent.

>> Cool. And um did you find many bugs when you reviewed the AI code? >> Not so much. I mean the AI is not inventing code because if you really spend time in planned mode you know what the AI is about to do. you don't discover things but I mean >> the design the function they input the output that you decide and then they just write it on their own and then it's fine like that because with Rust very good compiler you have a lots of back pressure to do agent so at the very end it's it's kind of easy I mean kind of easy >> okay wow brave new world thank you so much CL uh next up we have Farah and Will who will share if proof's updates

Fara Woolf: Ethproofs update

Yep. Let me share my screen. Okay. Yeah, we pushed a major update to e proofs that implemented much of what we proposed in the last call. So, prover personas are now live. So, um basically these four prover types. So, a team can have one of each of the four prover types for a cluster. Uh GPU price index is now live and running weekly. So all uh prices will be tied to that weekly average. Um and all historical proofs have been migrated to a quarterly average price. Uh we have new onboarding flows for signing up uh new teams and signing in as an old team. Um and that

comes with a a new team dashboard in the UI where you can both create and edit your clusters. Um and then also we've added a new external API so you can edit your clusters through that. Um, as Justin mentioned, we have launched a new page tracking guest program diversity. So, go check that out. Uh, we relocated and revised the pizzas based on feedback from EF teams and others. So, proof sizes were changed to match the real-time proving requirements. Now, um, protocol soundless soundness was removed just because it was difficult to audit and kind of verify. right now uh security target was changed to sound to soundness and it will be provided by soundcal

moving forward. Um and then we pitched new designs for the security sprint leading up to um the next ethuse call in ECC. So this is kind of the next chunk of work that we'll be working on. So kind of look for this to start to come live um towards the next call. I'll present that. >> Okay. Fantastic. Um, yeah, thank you for >> Go ahead. >> Uh, just to follow on my short update with that is, um, we have a new ERS builder channel. So, if you're submitting proofs, you've got a guest program or a ZKVM on ETH proofs or you're getting very close, uh, DM me and

we can add you to that. So, that's where, um, we've been sort of coaching people on the new onboarding and we're going to be sharing, uh, Figma comps. So, a lot of the teams that really like quote unquote have skin in the game, we want to make sure that we're getting their feedback and uh integrating that feedback into what metrics we're going to be highlighting. And then uh lastly in the chat, one more shill for uh our ETH proof uh sorry, ETH CC uh and can side event that's coming up on March 28th. So, make sure you sign up. There's only a handful of seats uh remaining.

Amazing. Yeah, I feel like the the pace of change, I mean, in general, is is is increasing, but for Ephrove specifically, um we're going to have lots of new widgets, lots of new pages coming very very soon, which is super exciting. Um, cool. Um, any questions? Nope, just a link to the Beast Mode event. Perfect. Uh, thank you, Far and Will. Next up, we have Kev, who will talk about uh the ZKVM Discord interrupt and all sorts of other things.

Kev Wedderburn: zkEVM Discord, interop, guest development

>> Yeah, thanks Justin. Uh second, I don't have any slides, so I'll just uh say what I'll I'll give an overview first. Uh I plan to talk about the planning, interrupt, discord, and then the guest program. Uh just one important note, uh as we go into the sort of the guest program talks. Uh so on the planning uh as many of you are aware we published a document breaking down the ZKVM project into several sub projects uh gathered feedback and we've now kicked off uh most of the protocol related work with a uh strong focus on specing out the requirements and endto-end integration.

Uh currently things are progressing well and later this year we're planning uh to have a ZK EVM interrop event. uh this could potentially be a side event in uh Mumbai just because uh a lot of people will be there already. It depends on the attendance overlap and we'll be reaching out sort of in the coming weeks to sort of gorge interest. Uh but either way, we're targeting something close to Q4. Uh on the discord uh to stay up to date on sort of the project and if you want to ask questions about protocol integration, uh definitely recommend joining the ETH R&D discord. There are currently two channels L1 ZKVM. Uh this is this is for like general ZKVM things.

Uh unrelated to CL and EL integration. Then there's L1 ZKVM protocol which is where you'll see like the EL CL specking and the integration work. So this is related to the uh presentation by Jun. In the future maybe these two will be merged. uh it just depends on uh how integrated the ZKVM teams uh become in the future. And the last note on the guest program uh as many of you are aware uh if you're actually building a guest program, what you're proving is the core uh STF uh logic. But last year we sort of realized that actually you need to prove a bit more if you're a core dev. It basically

means you need to prove uh the engine API new payload. Uh and if you join discord we can sort of talk about it and you can see what uh the specs will look like. It's a bit of a change but not uh too much but it's something to keep in mind. >> Okay. Thank you Kevin. Is this a does it have a performance impact or is it just a a minor change? Uh currently it doesn't have a performance impact but once we go to block in blobs it will uh just because you now need to prove that the payload is being chunked into uh blobs and this involves potentially doing KZG commitments uh which might be expensive for a lot of

the ZKVMs. Okay, interesting. Um, and yeah, in the chat we have a link to the the road map. Uh, thank you so much for sharing. Uh, Lis, any questions for Kev? Seems like, uh, yeah, you're going to be very active in 2026 at the social layer with, uh, all of the various calls and events that you're organizing, which is fantastic.

Um, Diva. >> Oh, yeah. Just uh, one question. Um I think I saw on the discord something about there being uh issues with the upstream Rust compiler with regards to um some issues. Uh do you have some idea when it will be sort of mitigated or how it will be? >> Uh could you uh maybe be a bit specific? I didn't >> I think it was regarding uh the um the memory allocation. I'm forgetting the exact uh term. Um Um I can't >> might be the unlinard the yeah the underlined. Yeah exactly.

>> Um yeah I think this is sort of a general just to give more context we was we was planning to standardize what happens if the guest program was to do like an unaligned load and an underlined store. Um I think we've just merged in and said that compilers may have bugs like the Rust compiler may do an unaligned load. Uh and this is a bug but it's not a correctness bug. sort of a performance bug. Um I don't know if the issue linked in the chat has been solved, but what we've said is that ZKVMs just will need to handle it. Uh so if your if your RS compiler is spitting out unaligned accesses, then it won't break the ZKVM. It will just make it super slow.

>> Okay. Uh thank you Kev. Next up we have Mitri. That's the final quick update. Hello. Uh thank you Justin. So I would like to introduce uh a new thing that we uh decided to be necessary inside EF cryptography team and um the story is that uh ZKVM is a very sophisticated design in general and having talked with all the teams how exactly they uh structure the proof uh we see that it contains a lot of non-trivial things like how uh the program trace is split into segment how internally operations are rearranged into dedicated the chips

Dmitry Khovratovich: security sprint

and after that after you proof this segment as a separate circuit how exactly you aggregate them using recursive snarks uh well this is kind of a general paradigm that's is satisfied by almost every KVM but the details really matter so how you organize your memory which pre-ompiles to separate how you organize this consistency checks and it uh appears that uh the details about this like do details are necessary uh for us to reason about the security of ZKVM designs. And for this we decided to ask for like a more formal and more detailed exposition. How exactly the things are done, how the segmentation is done, how consistency is proven and how

uh the consistency is guaranteed among chips and segments with some specific arguments like permutation argument, lookup argument and other things. And we believe it should be uh a document that covers all these things and the details about the recursion uh about the details about the statements that are proven at every step of the recursion and how exactly they combine into the final statement about the correctness of the original program. So we think that uh such a document uh should be written it's not a definitely a spec it contains much more math and more English and it should be prepared in phases and on the right you see an approximate timeline we have in mind so we have just communicated the

preliminary requirements to the teams and uh we will publish them very soon we ask to integrate uh their circuits and lookups into sound by the end of February and basically we expect the first deliverable the first kind of superficial thing uh in uh uh 1 of May which is called milestone W1 and then we soon published the new requirements based on the feedback from the teams and the final document ideally should be produced in beginning of December uh collocated with this require milestone of achieving 128 bit security.

Yeah, that's it. >> Okay. Um, lots of due diligence from the cryptography team. This is great to see. Um, any questions for Mitri? We do have one question in the chat for E. Um, how did you measure the 3.8 GHz and are you taking into account pre-ompile instructions?

Yeah, this is um on the coremark benchmark. So we ran coremark with 10,000 iterations um and use a setting that only includes risk 5. So no pre-ompilements, >> no pre-ompile. Okay, perfect. Yeah, very impressive numbers. Um cool. Um we're going to be starting the fivem minute presentation. So, first we're going to have six presentations from uh six different EL client teams starting with GE. Uh so, Giam, the floor is yours to talk about Keeper.

Guillaume Ballet (Geth): Keeper

>> Hey, um let me share my screen. And while I do this, thank you very much for uh letting me go first. I'm sorry to frontr run everybody, but I've got I've got a babysitting issue. Um Okay. Okay. Is that it? Yes. Okay. All right. Can you guys see my uh >> my presentation? Okay. Perfect. So, yeah, I would like to talk about Keeper, which is the guest uh program from the guest team. Um the design philosophy is going to be fairly different from the ones you're going to see uh um after in the the next presentations. Uh we there

was a there was a conversation in Berlin uh back like uh last year last June and uh we agreed with the ZQVM teams that uh we should implement the Linux interface or at least compatibility. Um this is not uh the road taken by other people but other guest programs but uh we uh well we we think u it needs to be uh ZKVMs need to be a general computing platform. So uh in this respect uh the ZKVM teams we talked to agree. So we decided to explore this uh this uh approach for for the time being. So

yeah, we're not sweating that much, Justin. Um, and where does the where does the name Keeper comes from? It's like a lot of guest projects. It's based on the Mass Effect universe. None of us have played it, but uh apparently there's those uh program those entities that are quite secretive. So we thought it would be the the perfect name for for keeper for the for the guest program going into CKVMs supported targets. uh because of our choice uh of our design choice is going to be limited. So so far we only support zyron. Um we had some successful uh tests with openvm and powder. Uh but powder decided to rewrite everything. So

uh we're waiting for for the update to see how good the performance is going to be. Uh and we're going to go through the wom pipeline. Uh we also had a very good conversation with the with succinct uh in in Buoss. So we're also going to explore Wom on this side apparently uh looking for name arbitum is also interested in using uh Wom. So so that there's a good synergy for us here. Um the last uh the last uh ZKVM we're going to target for the time being is is ZISK.

uh we would take the route of co compiling for risk risk 564GC which as you know is not compatible uh with the with the target but uh we're going to make some tweaks and see how far we can go with this. Um we're only considering two tool chains. I assume nethermind will have a lot to say about this but uh but for our guest program where we want to stick to the stock goal because we we know it. Uh the problem is it either requires an OS support or dirty hacks. Uh there's also Tamago which uh doesn't really target the platform that is targeted by by the others KVMs. Uh but since apparently it's going to be merged some of it is

going to be merged into mainet uh mainline we are also experimenting with it. So what did we do so far? Uh we tested a few hundred blocks no issue reported. So uh at least our our mo model is uh is sound enough to to continue. Um and yeah, every time we commit to master, we build a release of keeper. Uh we don't actually publish releases on our page yet, but uh yeah, we're working on it. Um what we're going to do therefore uh in the future is to try to do chase some performance. So add more pre-ompiles. uh try uh an alternative interpreter, maybe a Zigg one, maybe EVM one. We'll see. Uh

we're going to try to remove the allocator because the the garbage collector is the is the big uh well the big issue really. And uh what we would target first is things that could apply to mainline guest. So outside of the ZKVM so that everything that gets developed is not is not wasted. And another goal we have is to push uh start publishing our proofs uh on East Proof with with Ziren. Um so I'm hoping we can do that in the next few months. Um yeah, I'm out of time, but that's al also most of what I wanted to say. So yeah, thank you.

>> Okay, fantastic update. Um and I didn't know about the potential integration there. Um I realize that these are like probably very preliminary numbers in terms of performance because you don't have the optimizations with the garbage collector and the pre-ompiles but like can you share like what is the starting point right now that you >> Yeah. So the starting point I mean uh it's it's it's slow it's ugly. Uh we're not uh we're not um ashamed to say that that our our goal is to be correct. Uh so I think uh what Ziren did but we don't have the pre-ompiles. Like we don't have a lot of pre-ompiles. Uh Ziren made measurements and we're like 20 20x slower than uh than our EVM. Um

but like I said it's it's only a starting point and our goal I mean we we need to be functional of course but we we want to focus on the correctness more than the performance. >> Got it. Thank you. uh Kon uh and congratulations. Um next up we have uh Dragon who will talk about our EVM. Um hello everyone. Uh to be honest when just asked me to present our EVM I was not sure what to do because I think this group is very familiar with it. So in general uh I would like to share uh just a second.

Dragan Rakita (Reth): revm

Yeah, basically I even started as the hobby project four or five years ago and at the beginning I have like uh few few guiding principles that I want to like to make to allow me to like guide myself on decisions when I create or modify RVM and I think they're very like even now very very important. Um first one was for is of course CV and compatibility. Any consensus bug need to be squashed. Everything needs to be corrected. Every test needs to be pass it needs to pass. Second one was speed.

I wanted to build very fast TVM that everybody can use. Um third one was simplicity. So it's easy easily used. So the anybody that need like EVM execution can just plug it in plug the database uh at that point of time just send one section and that should be it. And the last one is let's do it no std. At the beginning um idea was to support JavaScript or CPP binding or anything like that but in the end it was very fruitful for ZKVMs for no std support.

Um yeah old basically and basically it was hobby project that point of time this like logo that I created at at that point of time uh presently um I think everybody used for reason um revm is very like used by all the builders all zvms it's integrated in red Um I think additional one topic that I could add in this principle is basically extensibility.

It's basically it allows something like op red opvn to be created and just extend use revm as the library. Uh this became like very good guiding principle for the future because everything that's made change or found can be like focused in one codebase. Um yeah there was yeah uh there was a lot of uh PRs related to both the improvements to the code base. I think Kev did a lot of those about uh allowing pre-ompiles to be plugged in with uh ZKBM versions. So yeah my DMs on that

side are always open if you have something even if you don't have time to implement it. uh just saying hey this could be good is always helpful. I think that's it for me. >> Okay we have a couple of minutes for questions. Um one question from me is uh my understanding is that you're now part of the Tempo project. Uh does Tempo have any plans for doing ZKVM stuff? not on me to say anything.

So in general I basically employ by tempo. Fortunately I can still work on RVM improve it basically make it better, make it faster, make it more usable. So I'm very glad that I'm there. Yeah, perfect. Um and um all of the um you know improvements to IVM specific to ZKVMs have they all been upstreamed to IVM and do you feel like there's more ZK EVM specific work to be done?

uh everything that I know are upstreamed but there is some things that I don't know and uh what would make RVM faster in ZKVM for example allocation is very slow that that basically is feedback that I got multiple times so using something like bytes or statically allocating before execution helps but in general uh having something like some benchmark or having some flame graph that could be done for ZKVM size to show me hey this part of the code is not great for ZKVMs would be very very helpful maybe that's like big ask but yeah

it's great to hear that you're so open to uh to improvements uh for the ZKVMs um and yeah if anyone wants to improve the memory allocation that might be a lowhanging fruit uh for you uh to work on And uh Kev says, "The main X benefits that we merged a while back was the trait interface that replaces pre-ompile patching." >> Yeah, Kev. >> Cool. Yeah, congrats Kev. Um, thanks Dragon. Next up, we have um Ivan who uh will talk about LEVM in the context of Ephre.

Iván Litteri (Ethrex): levm

>> Hello everyone. Thank you for the invitation and the opportunity. Uh I'll be sharing my screen right now. Okay. Can you see? >> Perfect. U well I'm going to talk about EXE live levm u and guess program diversity. Let me here's a quick overview of what I'm going to talk. I'm going to talk a little bit about shortly our eex the current status of our guest program. Why does diversityity matters? how CKVM teams can integrate with ERX and how they can get involved on that.

So, EX started as a another execution client in RAS and then we are now transitioning to a CKVM guest program which uses LVM underneath which is our implementation of the EVM protocol. Uh it's designed it was designed from scratch to be CK friendly. Um yes and it was made for pro right now we are EXEX is in production as an execution client and also as a guest program we are host we are running a onrem CISK prover on proofs which was this week um offline because we were doing some modifications to it but it is

up again and right now the guest program has integrations with CISK SP1 and Rick zero we working on we are finishing the iterations uh with openvm and pico and we are planning on integrating air vendor in the near future and why we stepped in diversity matters uh the foundation of the is diversity we need to do the same for guest programs right now almost every prover is uh using rev and ref there are a new guest on uh here to use and it's it would be fine for all CKVM teams that try Ethics

integrate their CKVMs and also host approver. Um in our repo we have a great guest program. It was a recent refactor that makes everything easier to understand and to read and to integrate. We have instructions on how to build the ELF and also how to integrate your CKVM there. This is more of a call to the CKVM teams to use ethics and to collaborate with us. We are very open at the end of the presentation also some links to the telegram where you can find us. We already are working uh closely with some CKVM teams but we are open to the ones that we are not currently doing.

So the message is FX is ready. Let's build together a future with a big diversity of guest programs. So these are some of the links. Um the the Telegram, the Twitter, we'll we'll be having a discord soon for community also. And that's it on my side. Uh I don't know if there are any questions. So you mentioned writing LEVM from day one targeting ZKVMs. Can you talk about what specific optimizations you've made that are targeted specifically for ZKVMs and how that might differ from uh REVM?

Well, uh the there are things that um for example we we are avoiding a little a lot of the clones and our try implementation right now is being optimized uh to be more sec the the the only part that is not that CKBM friendly is the our try but the rest of the code is goes uh really We also uh planned all the the modules for the for the pre-ompiles. It's very easy to implement. It's not like the interface that K mentioned earlier. It's

some it's a little bit different, but we'll probably we will be adopting that in the near future. But yes, the the main thing was every CKVM has different pre-o compiles and it was a little bit messier. We have modules that are separated and you can switch which back end to use with feature flags for example from different CKVMs. And for the memory allocation, do you have a custom solution there? >> Not right now. Um but we are working on improving it even better.

>> Okay, got it. Um yeah, if anyone has questions, just feel free to raise your hand, ask in the chat, or just on mute. Um if not, thank you, Ivan. Uh and we'll move to um Snaf from Aragon who will talk about Zilworm. >> Hey, uh thanks for having me. Uh let me try to share my screen. Okay. So, uh, Zilqu is uh an efficient, fast, stable VKVM core written in C++. The objectives keep changing. Uh, but curious

Somnath Banerjee (Erigon): Zilkworm

some of the bits that you should know about me that have been a core developer for Aragon and quite bullish on ZK. And this presentation is on a you want to laptop goes on to show uh how much you can do with open source today and uh not cave in to the big tech. Um but let's just go over what we did for Zum uh so far. So we're already live on ETH proofs since uh September 2025. We also deployed uh the turbo um version that is SP116 uh prover which was almost as efficient

as the RSP version running hyper cube. We went on to then optimize further to make the zilcom hyper cube and it performed around 2 and a half times faster. Uh eventually we delivered the the smoothest osaka upgrade. We were monitoring how the uh upgrade would uh work out at the fork boundary. Uh that went well and now we have 100% uh passing east. Um again correctness a little bit about the legacy uh of this project. Aragon had a project called silkworm which was a full client

implementation in C++. uh also used EVM1 in its core as the EVM um and it used a state sync model and so on but the takeaway from that was uh it was already 30% faster in execution and around four times faster in RPC that goes on to show that that's a very good candidate for the resource constrained uh ZKVM of course we have big thanks to give to the amazing EVM1 and all the contributors including Pav who's also working on this project. We decided to take advantage of the baseline at least 30 to 200% faster RVM on certain lines of execution. There's also the advantage

of low memory footprint and uh the work that goes on on the side like uh the index library for big numbers and so many uh work uh things on pre-ompiles. We basically forked it right now um in in a repository called CCM1 um and we'll continue to push changes to that. But how it all came um together is this 10 lines of Rust code and an overall CPP project uh in which we can directly use the CX bridge. So, Rust basically interfaces uh quite well with CPP and uh you can sort of just plug in uh the

whole zilqu um in any any of your approver system. Of course, we started with SP1. So, uh this is uh sort of how we just call the state transition function implemented in CP and just invoke u an external symbol on it. uh some unseen moments. So these uh incremental upgrades happened with a lots of graph and uh we just uh made sure that on every iteration we have like about 50 to 100% uh catching up uh and then eventually we uh cross the speed of revm and then I think last week uh we focused more on correctness so we

enabled uh ESTs both natively and on RV32 IM uh with KU to pass the equivalence test that we had in our minds. Uh and further this year we're going to focus on uh improvements for performance. Our eventual target is one gig gas have some simplified tool chains risk five of course and of course uh some performance tweaks and unification on the SQL IO with different provers. So we invite you to visit uh the documentation page and the project page on GitHub and I'm happy to take any

questions. Thank you, SNAF. Um you mentioned the performance improvement uh relative to revm 2.5 times faster even you know using turbo relative to to hyper cube I guess >> sorry go ahead what >> uh hyper cube is faster uh compared to hyper cube uh turbo is almost the same because turbo is inherently slower >> right right so you were 2 times faster despite running on turbo um so Yeah, one comment here is that um you know innovation at the guest layer is not just about diversity, it's also about performance. And I guess my question to

you is have you tried to doing an applesto apples comparison um revm um and and zilkworm using the exact same uh zkvm. Uh so so far we've been able to only integrate uh the hyper cube and turbo from SP1. I suppose uh their guest program is a derivative of RVMs. These are you know indicative numbers. Um the exact RVM deployment I'm not sure if I can do that maybe u with this or something which is already out there but the indication is that RSP is a form.

I'm not sure how much uh they carry the lineage. >> Yeah, I was kind of using RSP and IVM interchangeably. Um >> so this is an >> sorry I interrupted you. Go ahead. >> Uh it is the same ZK VM uh silicon hydro tubers. uh the direct comparison to RSVP hyper cube.

I think that's what they use if I'm not running. Tamir's on might correct. Yeah. >> So Kev is asking what is the reason for the 2.5x speed up? >> Uh I think a hard work trying to profile and lose memory footprint. Uh memory is a premium actually I have been told for the proer.

Okay, got it. So I guess if we have these like custom memory handlers, we might partially close the gap uh with uh with Zilwam. Um congratulations enough on on these great numbers. Um, next up we have uh Gary from Bessu who will talk about ZK Bessu as a placeholder name. >> Yeah, thanks Justin. Good morning from the uh US Pacific. Uh I've had enough coffee. I think I'm awake enough. Uh share my screen.

Gary Schulte (Besu): zkBesu

Yeah. So, uh, Gary from the Basu team. Um, I've been, uh, leading our efforts, uh, at building a guest program, uh, on the Basu team. Um, I kind of want to give you just a a heads up of where we've been and where we're going. Like, uh, initially our goals were to, um, leverage BESU, the codebase, and the team, you know, and the Lindy that we have there, uh, in a guest program. So our initial efforts were to build a state transition function uh guest program uh in Java using basu components. Um and we got fairly far with that and we're building for uh risk 5 targeting risk 5 with a growl grow VM LVM feature. Unfortunately it's um you

know it's OS dependent and linking to a static JDK. Uh we ended up with just massive binaries. Um we were contemplating you know targeting musel and using static you know using shims uh to get to bare metal. Um but we decided that that's going to be brittle and you know the u the tool chain would be very brittle the the resulting binary would be large probably not all that performant um and it basically destroy any lendy that we think we have with uh using basu as as a core library for a state transition function. Um so we pivoted um probably late Q3 early Q4 looking into um a native EVM that we

could drop into Basu. Our our goal in that case would be we would only as a team be maintaining a single EVM um rather than having a Java VM and a native VM that we would have to to maintain. The goal in that uh case was to kind of limit that so we don't have multiple you know duplicate work across multiple EVMs. um we got far enough along with that that we were um doing performance benchmarking and we found that uh even with like Java 25 FFM improvements um crossing that Java native boundary going back and forth between a native EVM and and Java for doing callbacks or tracing and things like that uh just that that um that native boundary cost just dominated

execution hugely. Um so we decided that that really wasn't a viable path either. Uh so late Q4 basically we decided that we need to go ahead and pivot to um another language and another tool chain that's uh you know specific to uh to that's going to be able to target bare metal risk 5 uh better. So we're kind of in the early stages right now. We have recently chosen on the Basu team to target to use Zigg um and specifically we're bootstrapping with a project called Zev that is a Revder derived port uh of Rev to to Zigg uh and we're you know making good

strides towards that. We're um we have a uh a working EVM implementation already and a the guest program is reading and writing you know inputs state witnesses and so forth and we're um kind of moving towards um we've got partial pre-ompile implementations and uh our goal is to have Fusaka support like kind of alpha quality Fusaka support ahead of excuse me ahead of uh Glamsterdam. That might be a bit of a stretch goal considering where we are right now, but that's currently what we're targeting. Uh, and then after that target, uh, we're going to be targeting just general, uh, you know, protocol schedule forward looking compatibility

uh, postclam. Um, also we are currently building with ZISK. Um, so we're we're not tightly coupled to ZISK, but we're really only focusing on ZISK, especially for like the CSR pre-ompiles and so forth. Um, and in our kind of final spike, uh, we're looking to do multi multi-ZKVM support, standards compliance, and a an extra stretch goal would be to, um, have an abstracted u EVM interface so that we could potentially plug in an additional EVM. Um, but I mean at at the moment we are working with Zigg, Zev, and Zisk.

And a little bit about where we are right now. Um, like I said, we have some of the cryptographic uh accelerators implemented for ZISK. Uh, we still have some outstanding work to do on some of those pre-ompiles. Uh, we're integrating the at least the reference state tests. Currently, uh, we have work to do on getting KCG commitments, verifications implemented, system contract executions, withdrawals, you know, all of the Fusaka specific protocol schedule stuff. Um but that's you know we're making making good strides and um we recently started having uh talks with the Ze team to potentially collaborate on a state transition function so that we could

have you know a a zig specific stack from bottom to top in the future. Uh and then also we're collaborating with Lineia on uh block proving and that's pretty much where we're at at the moment. Um, we're going to be um MIT licensed uh and we'll have a public repo to share soon. Stay tuned. >> Okay, amazing. Um, Kev is asking, "What have you found hard so far about reimplementing the STF for ZKVMs?" >> I think the most challenging uh aspect we've come across so far is the memory alignment issues. uh when we like when we try to implement pre-ompiles and cryptographic functions that don't have

accelerators built in uh trying to bring in third party libraries uh you know rust or C++ libraries u static blocks and things tend to kind of mess with the memory alignment um that's really kind of been one of our current stumbling blocks but I'm sure there'll be more to come but that's that's at our current state of development that's what we found the most challenging >> okay perfect and when you mentioned Ze, I just wanted to clarify. There's like two Zigg implementations that I found. One from Jordan, >> right?

>> Is that the one? >> Yeah, this and it's not it's not No, it's not that one actually. It is a u um an independent contributor um who's I think >> is it Raul Raul Jordan? >> No, it's uh Lodge is his GitHub handle and Zev is like it's it's it's fairly early but fairly complete. I could provide a link in uh >> yeah that'll be help. Thank you. >> Okay, great. Um I mean as a side note um the implementation from Jordan Copot is also being worked on by Gum on on the GF team and there were like very very early discussions of potentially having

um that be integrated with GE. Uh I don't know if Giam is are is Giam on the call? He might have had to leave. >> Uh yeah, I'm I'm going to have to leave in just uh a sec, but yeah, it's still an option, but uh so far we're going to experiment well try to make guess faster while uh Zev um you know matures. >> Okay, got it. >> Yeah, we've we've considered you know one of our stretch goals as I mentioned is to to be have a more abstract interface around our EVM implementation. So we could potentially uh change that uh be it something derived from ZKSM from Lineia or uh or ZEM or one of these other projects but that is a bit of a stretch goal at the moment.

>> Okay, very interesting. Uh thank you so much Gary. Um next up we have Maxim from Nevermind who will talk about uh Nem the implementation of the EVM in Nevermind. Hi. Do you do you see me? Do you hear me? >> We can see your video. >> Okay. One moment. Uh I will share the screen. >> Yes. >> Perfect. Okay. So um so I'm going to talk about nez implementation.

Maxim Menshikov (Nethermind): NethEVM

So what we have achieved so far we have made execution witness. We have developed a stateless executor. We've made a minimal EVM binary uh and probably the biggest chunk of work in terms of duration was uh risk 564-bit compilation and just a little bit smaller disk integration. Uh I will talk about some specific points of this work. So as for stateless executor um it it's still implemented fully in C. It's based entirely on nezmind client code base. It uses of course some conditional

compilation to trim unnecessary and incompetent code but overall it's still the same. Uh it's fully native and it contains no dependencies. After we build our binary, it's u it's a binary which we can run still on Linux in some ways if we have just a bit different in your script but uh it contains no single system call and it can run on this and other ZKVMs when when we implement them. uh then such stepless executor can call to ZKVM IO whatever ZKVM use and it can call to ZKVM pre-ompiles that's what is

implemented and it works for us as for um tool chain itself uh I will tell again that we we have adopted Alpine Linux um we needed it just to build net runtime because well it naturally needs a lot of Linux packages even if they are not really needed. It's a bit hard to trim all dependencies at this stage. So that's why we did it. But we changed compiler mode to risk 564 IMA. We disabled uh assembly usage, truncated floating point usage and fixed lib and wine frames and did many small other fixes. As for native, native is ahead of time compilation

actually. So to compile C# to native risk 564bit binaries we employ risk 564 code generator which is already implemented within net. First it wasn't ready but now it's even released so it can be used in net 10. We add many patches. First we removein and all other redundant parts. There are a lot of different models that are not really needed for us. We add zero library that's some um simple simpler versions of some functions and uh we also unflat just in time code generation libon wind staver and other parts which depend on

floating points. Of course we can't use floating points and we don't really need them. So they we trim them. Uh also we clean up big integer calculations because they still rely on floating points but we of course need some precision at this time. Um uh we have developed our fork of B flat. Uh in this fork we still build code as usual. No changes really. We add some compiler definitions and other stuff but in general it still follows our compiler flow. We add add extranet libraries for example target ZKVM libraries for input

output pre pre-ompilers and whatever. Uh the biggest part is extra native libraries. We add a new PAL a new GP it's well it's net models we add random number generators new TLS implementations C++ shims updated bootstrap and uh which is also important a garbage collector a new memory allocator implementation as well and then we relink it properly. So we just use of wrap linker option uh and by that we can integrate whatever we want quite easily um and it works in fact uh we start with native start entry point then

we run bootstrap then we run lip then bootstrap and where we initialize everything and then we run just a C# main which actually does a lot of calls into our modules implemented on top of big flat fork doing custom applications and whatever else. So uh and also in in order to make it work for example in zisk we had to do some extra work for example it doesn't tolerate data inside code sections I know there there was some work done but still we had to implement wiping data from code section it worked so yeah that's it

any questions >> okay thank you uh Kev uh thank you for your questions Kev Kev asks how many cycles does runtime initialization take? >> Oh, it's very good questions. Uh I know the counter goes over millions but uh I I can't talk precisely because it depends on the code size of course runtime in ination itself is quite small. Uh but uh every additional module adds uh static constructors and whatever else. So it depends. It's still uh change changing every time we edit stateless exeutor.

>> Is it fair to say that you could just run the initialization once and then take a a snapshot and then load that checkpoint? Uh >> oh. Uh I'm not very I'm not very good at stateless exeutor implementation itself. I'm more about C compilation. So, but as far as as far as I remember right, it's what was implemented by our team. >> Okay. And uh Kev also asks, is the garbage collector now just a bump allocator? Are you still freeing objects?

>> Uh we're not freeing objects right now. We don't care about it. We allocate objects just like from the top to the bottom right now. later if we need it we we will implement freeing but it's not tracker >> okay and do you have a max amount of memory that you can consume >> uh we have some preset u available I think it was 100 mgabytes for now maybe maybe even more but we can change it every time we want it depends on the virtual memory size that that is available so we are not quite limited on Okay. And Kev also asked, "Why did you

also have random number generator as an extra lib?" >> Oh, it's it's a good question. Previously, it was using OpenSSL and of course we can't use it this way, but uh eventually if uh random number generator is available as pre- compiles in specific SKM, we will use it. And I guess a question for me, um, can you try and quantify the the invasiveness of all of the changes that you've done to the tooling and maybe the probability of a critical bug being introduced by modifying the tooling?

>> Well, we don't modify tooling itself for shar regulation. We change some functions. We do quite safe changes in most cases. Uh there are not uh very safe in my opinion uh changes regarding object layout inside the garbage collector but uh it's all testable. We can just perform many tests seeing how it works and perform some validation and through other ways so should not be a big deal. >> Perfect. And uh do you intend to integrate with e proof soon?

Uh yes, as far as I remember there we we have just another team member who is working on it. So >> okay perfect. Um thank you so much Maxim. So this concludes the presentations from the existing uh consensus layer teams. Now we have um alternative EVM implementations and we'll start with Bruce from Monad who will talk about their EVM. Hi, thank you for the the invitation, Justin. Just let me share my screen here.

Bruce Collie: Monad EVM

Cool. Fantastic. Um, yeah, it's a pleasure to be here. Um, I'm here I'm here from Category Labs. We are the >> primary maintainers um of the the master. >> Sorry about that. >> I just muted someone. Thank you. Yeah, we are the the primary maintainers of the the Monad execution and consensus clients. Um the the Monad EVM is a GPL3 C++ implementation of the EVM. We support uh everything up to Osaka.

Um we tested um against replaying the whole of Ethereum history up to I think a block in the range of 23 24 million. I don't know where our sort of downloads are at the moment, but it's in the the sort of low 20s. Our replay compatibility. The the VM is live on the the monet running at a sort of notional supplier size capacity of 500 million guests per second um through boot. Um, the execution client is written in C++ and is optimized pretty heavily for the specific Monad validator specification. Uh, and so we have things like a a custom state database for

accessing raw MVME block devices. Um, there's a custom encoding of the database there. We've got a a really fast byte code interpreter for the EVM based on um guaranteed tail call optimization. Transaction transactions are executed optimistically in parallel. Um detecting conflicts and retrying. Um the database is written such that uh retries of conflicting transactions are really cheap because you've already warmed the database and the the stuff is cached in the the drive and in in memory. And we've got what we sort of believe is one of the best um specialized x86 uh 256 bit integer implementations as part of the the execution plans. Uh we're pretty early on in our our progress towards becoming

a zk guest. Um we have our interpreter compiling to a a risk 5 zis host already. Um so we've got somebody somebody working on that. We're sort of at the level of making proofs over single op codes at a time and the figuring out the the tool chain support because we're we're while we're written in C++ we're kind of at the the bleeding edge of tool chain support even for x86 codegen and so we're testing the the boundaries of what you can do with um available risk 5 tool chains and at the same time we're we're beginning to figure out the the practical steps that we need to to turn our our database and sort of inmemory state representations

into something that we can use for uh witness based stateless execution in the in the client. Um everything is is open source like I said it's a category lab monad. Um we're and again we're pretty early on in the the ZK journey. We're hoping to move pretty quickly and get towards a a working guest program Q1, Q2 and we're hoping to at that point integrate into get integrated into ETHs and have something something that's uh that's runnable and and hopefully pretty fast. Cool. Happy happy to take any >> Perfect. Thank you, Bruce. Um I guess we were talking about how Zilkworm is maybe 2.5 times faster than than our VM.

Zilkquerm is in C++ at least EVM1. Um how do you do you know how your implementation compares to EVM1? Um it's been a little while since I ran the benchmarks. We when we wrote the interpreter it is on sort of pure compute benchmarks comparable or faster to EVM1 and basically everything that we we ran it on. Um, obviously as you do larger programs in the EVM like host and state start to dominate your your execution time, but for raw execution, we we think it just passes faster or faster than EVM1.

>> Okay, got it. Um, I guess all of the optimistic uh execution that's not relevant, right, for ZKVMs. >> Yeah. So this is we we have a lot of like systems code in the in the client that we're going to have to figure out abstractions for and and rip out. But this wasn't necessarily written in in a ZK friendly way. And so we're going to have to sort of do a lot of um practical work to I guess have both coexisting in the the same codebase to find the right um engineering abstractions to to let that happen. >> Great. Uh Kev is asking what is the main motivation for Monet's investigation into guest programs?

it wasn't something that was sort of hugely on our radar until I guess you got in contact with us and said this is something that's interesting. I think we're we're basically interested in maintaining Ethereum compatibility to some some extent. We we have all the spectas all of the the replay passing and I think a general sort of alignment with the the Ethereum ecosystem and roadmap is is in both of our interests Very nice. Um yeah and I I learned on our call that even though um monad has some differences it's not strictly EVM equivalent you maintain a version of your implementation which is strictly equivalent to one >> we we we implement all the features that

are so for instance nonad L1 doesn't have um blob transactions but we have full support in our execution layer for running blob transactions. So we we we take care of the like EVM compliance even when it's not like directly commercially relevant for the monadel one. >> Thank you so much uh Bruce. Uh next up we have >> uh from the well he'll be talking about the Falcoin EVM and he used to be involved with Falcoin.

Raúl Kripalani: Filecoin EVM

>> Everyone yeah thanks for inviting me to this. Uh these days I work at the Ethereum Foundation. I lead the peer-to-peer team and some scaling efforts. But uh so this is going to be about a past life uh that I had where I was deeply involved in uh in Falcoin and specifically the Falcoin uh virtual machine project which also shipped a uh EVM compatible runtime and that's what we're going to talk about uh today. So uh why? So I was chatting with Justin a few a few weeks ago and uh we were talking about gas programs and kind of the difficulty and extracting the pieces that are needed from existing Ethereum clients to actually uh minimize what needs to run in the ZKBM environment and

kind of like you know how tangled things are just because the EVM runtime specifically were not built uh to be extracted or to be sandboxed and so on. So things are really tangled. So the t the challenge generally as as I understand it is um clients are monolithic. They're built for a bunch of things. Uh the EBM runtime is usually coupled with a client and there's large dependency trees and runtime overhead to prune uh on that path to to making them uh run within a zk a tighter uh zkm environment. So uh the filecoin em is actually built on the filecoin vm. So the so FEM is a was based hypervisor. Uh originally we had decided to run

multiple um runtimes or to host multiple runtimes um using WM as kind of like the intermediate um um instruction set essentially and uh the first runtime that was shipped in 2023 was uh the EVM runtime. So this is called febim. Uh just to give you kind of like a very quick uh overview. The filecoin the fm runs has this notion of actors actor and and the FM provides a contract to actors which revolves around uh providing sys calls which are very nicely packaged uh calls out to the host that perform things like IO crypto

randomness and things like that. Uh the FEM does gas accounting uh by we weaving in uh basically transpiling was bite code and we weaving gas accounting logic and the hold conditions and so on statically. Uh but the state is represented in in filecoin state model which is based on IPL uh which is also used in IPFS. Uh so this would be one part that uh would need to be translated. So the EVM runs as an isolated wasm actor uh with a very clean uh sys call boundary. So all the side effects and all the calls to the environment and so on are very nicely packaged. Uh and all this runs through

uh trade abstractions. Uh this is a rust codebase entirely written in rust. So uh compos of course and and also to ris um I I tried it tried it today. there is no shared state, no global dependencies and so extraction would be pretty straightforward. Um, specifically about the EVM runtime, it is a very small program. Uh, it is already no STD and a composer risk 5. Uh, as I said, it has all of the externals are B are very nicely abstracted in traits. uh and because it runs in a sandbox environment, it has no GC and it has predictable execution. We actually

restricted the FEM restricted the was um instruction set and kind of like the the features the W wasn't features to uh remove things like floats and remove things like threads and and and so on and SIMD that would introduce non-determinism. Um so so this like assumes that and it is LLVM friendly. Uh it's also entirely Ethereum compliant in terms of basically everything uh all the way up until so we started uh because this was launched in 2023 we started with ARIS with a Paris fork onward so it does not have any historical baggage uh but it does have the the newer features like zero and and transient storage that have been introduced since then uh so I

I do think that um it it is up to date with with the current uh environment so that's And it is entirely uh compliant in terms of gas accounting, hold conditions and so on. And it does have all the all the pre-ompiles that Ethereum requires. So this is just uh some some of the key strcts uh that are behind this uh implementation system the storage strct some of these uh sorry these are strcts and and storage as a as a trade and specifically added it here because it's one of the if we if somebody wants to use this EVM runtime and and build on it this would be something that we'd need to uh change. So yeah, so in terms of potential next steps, uh the idea would

be to extract the EVM runtime, remove it, remove the file specifics which are not that many. I think this could be done very quickly. Uh compile it to risk 5 and uh smoke test under a number of variants. uh and uh the important bit here is uh adopting the the MPT storage model cuz right now it's the storage is based on IPLD enhance. So uh yeah and then benchmark compare proving cost and so on. So like starting the cycle if somebody's interested in in doing this I'm very um feel free to contact me and and we can take it from there. I'm also in my own time doing a little bit of uh of this work. Uh but it is not my primary focus. uh I can help route any teams that that might be interested in

taking in in experimenting with this. >> Okay. Thank you, Ro. Uh I don't realize there was a different tree. Um Kev is asking uh is it up to date with Osaka? >> Uh I think yes. uh with I think with the exception that the file network does not support blobs in the form that they trans that they exist in Ethereum. So there might be some differences there in terms of uh some specific op codes but other than that it should be it should be up to date and if not it should be pretty pretty

trivial to bring it up to date. >> Cool. And who would you say is the main person on the Falcoin side of things? uh working on this. >> Yeah. So you can contact me and I can route you to the to the right person. Um just feel free to to do that. >> Perfect. Cool. Um I see no more questions. Thank you so much uh Raul. So next up we have uh Evani who will be talking about two separate EVM implementations that he's been working on. one in the context of near the Aurora EVM and a second one called the Swift EVM.

Evgeny Ukhanov: Aurora EVM & Swift EVM

>> You see my screen? So, hello. Thank you Justin for the invitation. So today I am presenting the Aurora EVM in the context of the emerging ZKBM landscape. I will briefly outline the specifics of Aurora EVM and its place as a KVM gas program candidate. So why is Aurori EVM specifically suited as a gas program and what are the key features? First the ST Aurori is written in Rust in the context of ZKVM. This ensures the maximum performance and full

tolerance and it is under the MIT license which opens broad possibility for community usage. Second, it is maturity. This is not a research prototype. The Aurora EVM has been running in production on the near protocol since 2021. It currently secures 10 million uh dollars. Uh this means we aren't just proving code. We are proving a codebase that has already handled million of real world transaction without failure. We are

proving battle tested code for the ZK context. Uh next let's dive into the performance uh constraints. Running the EVM inside ZKVM is computationally expensive. It is obvious the proving time tray direct directed with number of execution cycles. Here Aurora has unique architecture advantage because we originally built this for the near blockchain. We were forced to optimize strictly for was execution limits.

We had to optimize the instructions count for every operations to fit into near gas model. And I think this preexisting optimization for Wasen maps incredibly well for the circle count constraints of Z KVM. We effectively inherit years of lowlevel optimization in the account. Furthermore, correctness is paramount. We maintain 100% compliance of Ethereum execution spec test. We support all hard forks including the latest OCA. This guarantees the proof generated of our

gas program is mathematically equivalent to in standard Ethereum state transition. So what is the current engineering status? We have successfully compiled uh the full Aurora EVM codebase as ADK West binary. We can uh currently execute multiple transaction with uh the ZKVM and generate proof to uh to prove for our output. The core execution flow is functional.

The next phase is uh scaling this to full block validation. We are engineering the flow to handle the entire block context execution. We have set a conservative timeline to finalize the architecture to Q3 2026. This allow us to address the overhead challenges and optimize the performance and conclusion.

Aurora EVM is in a good state of readiness of the K EVM gas program. We are leveraging a production ready highly optimized trust implementation as fast tech or development verification competition. Thank you. >> Thank you. It's very interesting to see was as a theme uh for several of these any questions from the audience?

I guess one is um can you talk more about the the motivation for the new ecosystem to be looking into ZKVMs? uh actually uh one of the most interesting motivation uh as I said is uh because uh we inherit years of low-level optimizations and we tried to use some different solution for our Aurora engine and we realized that we are in quite good condition. It means that at the moment we can't use any other solution because we are optimized for cycle so uh execution. It means that

uh uh we can feed for ZK EVM excellently. It is my own opinion. >> Okay. Perfect. So all of the the gas goal thing that you've done uh in the context of the NEO smart contract applies here again. Makes sense. Um, cool. Well, I'm not seeing any Go ahead. Oh, no. Um, I'm not seeing any other questions. So, um, I guess we could move on to the Swift EVM.

Uh, sorry. >> No worries. they should change that. >> I guess one side note is that even though uh you know the Orai VM is securing 10 million now at its peak it was securing I believe billions of dollars potentially close to $2 billion. Um, so yeah, it's definitely uh stood the test of time. Really sorry for some reason not show my presentation in my slides.

Why too? >> Alexander, do you want to comment uh about uh the the total value secured in 2022 while we wait? Uh yeah yeah yeah you're uh absolutely right. The amount was uh extremely higher in 2022. Uh um it was uh when Aurora just released and of course in price for Aurora token was uh much much higher and amount of uh value uh was locked much much higher as than now. Yeah.

And can you talk about um audits that have happened to Aurora AVM? >> Yes. Uh we did audit with uh audit one uh company but uh at the same time we have uh uh bug bounty on hacken proof and we constantly uh uh uh respond to some uh reports that we uh receive uh and I mean that we uh uh constantly under attention of some hackers and uh Yeah. Uh at uh uh the bad thing that a lot of

reports are get generated now by AI and it's a bit annoying but yeah. >> Okay. Got it. Uh thank you. Uh we can see your your slides. Uh the floor's yours. >> Yes. I'm really sorry the for because it was a second presentation and it was hard to find it. So thank you again Justin for the invitation for my uh second uh presentation. Today I am presenting Swift EVM in the context of the ZKVM context. This is my personal initiative. Swift is the uh native language for the uh entire Apple ecosystem extending actually also

embedded devices. Currently the blockchain ecosystem in Swift is almost non-existent. You probably know it. Uh Swift EVM aims to be foundation building block uh to change that to unlock that uh unique niche. Next uh the rapid evulation of the KBM opens uh new doors for emerging projects. Nevertheless, Swift ecosystem is currently a blank canvas for the for that regard. Uh Swift EVM can serve as catalyst for a a new world uh

development community. We are effectively uh expanding the uh boundaries of where Ethereum can go. uh bringing to new platforms and uh environments. uh the current future of it for that project it is fully native swift implementation to achieve high performance and uh good points we had to build essential low-level libraries that simply don't exist currently in swift so uh also it is in MIT uh license uh opening broad

possib possibilities for community usage. The project is currently in an active development phase and it is technically in a quite good uh quite good uh shape. So uh Swift EVM has no analogies. It is the first native EVM in Swift language. We shows uh uncompromising aggressive optimization something rarely rarely seen in uh typical swift apps to ensure maximum performance. It is truly crossplatform running on Apple devices,

Linux or Android web assembly and also risk five because it is uh used as back end. Uniquely we maintain 200% test coverage and uh this is an exceptionally difficult standard to achieve but it allow us to verify every single execution path guarantees absolute reliability.

Uh regarding the ZKVM gas program, we are uh currently in research and development stage. The biggest challenge in technical challenge in in this case it is lack of nift runtimes. Our road map uh is optimistic. We are preparing the architecture for the KVM's integration targeting to 2020 2026 sorry 2027 for functional solution and

conclusion I am inspired uh by the idea of expanding the EVM horizon present. I truly believe swift EVM will play a vital role in bringing the gap between the Ethereum and ecosystem. Thank you for your attention. >> Thank you. Uh Kev is asking what is the ISA that the Swift implementation targets?

Oh actually uh it is GC for uh currently I tried for risk 5 64 GC also I I want to mention that uh previously ar for mal specification on appshar to and it is open source in github so I'm quite convenient with risk 5 and also tried it is an apj implementation uh So and in swift context currently I tested compilation only for uh 64GC but it is no problem because as as you know as we used be back end it is the same uh behind as rust so it is no problem at

all. >> Got it. So I guess in theory you could compile down to rest five sorry to was if if you wanted to >> as well. Got it. Uh also wondering whether arc is a problem in terms of performance for swift. Probably swift will emit more risk five instructions than C or Rust. >> Uh not sure. >> Got it. Um and Egony, how long have you been working on this passion project of the the Swift EVM?

>> Oh, it is was started in 2024 on September. >> And why I started is it is probably quite a model because uh I maintained our EVM. So I have quite good context of EVM and execution layer or for Ethereum. So I was quite inspired with that and I think unique niche for new implementation. >> Yeah. Uh and it's amazing to see so so many contributors uh write their own EVM implementations and today I learned about two new ones uh in Zigg which is fantastic. Uh thank you so much uh uh

next up we have uh we tang who will talk about the rusty VM in the context of polka dot. >> Hello. Uh yeah so uh I think uh I didn't prepare sorry I didn't prepare any slides but for rust evv that's actually a project that existed for a really long time. uh I think uh it's probably one of the oldest uh rust implementation that is still being maintained. The other one being part of the Ethereum which uh we all know is I'm pretty fully died already. But uh uh for Rust EVM I think uh I don't have much experience with Zika EVM but I will I actually want to

Wei Tang: Rust EVM

try to do some integration and see how it works. Uh one thing that I think uh would be of interest is last summer we did the 1.0 release and within it we have a new kind of a new generic design. Uh in it we have a new uh I think a quite well designed call stack. Uh so the new call stack would allow you to like you can you can allocate the call stack first on stack and then on heap or you can do that interchangeably. I think some previous team mentioned that they have some problem with memoration.

Uh I think this this could be a point that could be beneficial. So hopefully I will try to tweak some those parameters and see if it give me some performance improvement. Uh but uh that's from you. >> Thank you. We um you mentioned that this implementation is very old. Can you talk about um the total value that it's currently securing? >> Uh I mean it's I don't actually have the value. It started as a as what's called spooting VM back for Ethereum classic uh in I think in 2017 and then a year later

there was something wrong with the team and the project become generic and I rebounded it to just EVM because we have the name. Uh uh afterwards I think there are a few teams uh that worked the 0.x X version to use that in production. I recall there's Etherlink and also I believe the Aurora EVM is actually a fork of Rust EVM. Uh but of course they did a lot of new changes afterwards which become totally independent. Uh and we also use that sort of in uh in polka dot for there's a few pars the moon bean

uh and some of them use that but they have some politics and they are doing quite big private in their direction. So uh uh that could change the solution could change but uh the next they are indeed used by a few production ch.0 which is quite new and I don't think right now uh any production ch but hopefully uh I will try to improve that and see how it goes.

>> Got it. And if I understand correctly you're not directly associated with with polka dot. you may be more of a independent uh >> uh I'm no longer associated with polo anymore at this moment. >> Okay. >> Yeah. But I was so >> what is the motivation? Go ahead. >> Yeah. I was working with party for uh I think four or five years. Uh and also I I'm the maternal of the politier project which is basically the the core the backbone of all the polit.

uh uh two years ago at least. So >> got it. And what is your motivation for keeping to maintain uh Rusty VM now that you've left the polka dot team? >> I mean I mean the rusty VM it predates polka dot. It it predicts even the time I join party. So it's kind of a really longterm hobby project for me. uh it it doesn't directly relates to polish is kind is really generic. I I also try to keep everything really generic. Uh so uh I mean it's I think it's the oldest uh rust involvation. So it's I think it's really good to keep keep it there and

maintain. Yeah. >> So it's just mostly I I think it's mostly a hobby for me. >> Understood. Uh love the enthusiasm uh and the the passion projects. Uh next up uh we have uh Olivia I believe. >> Sorry. Okay. Go ahead. Thank you. Hey everyone. Uh can you see my screen? Uh it should be a presentation.

Olivier Bégassat: Linea EVM

>> Yeah. All right. >> Thank you. So yeah, let me talk about Linear's uh ZKVM. Um so I'll start by just explaining in a nutshell uh what it is we have. Uh first of all we're ZK EVVM so we provide a direct arithmetization of the EVM instruction set rather than let's say a risk 5 ZKVM. Uh we use a latisbased proving system called vortex which runs on the CPU currently which provides us with 128 bits of security and also handles all of our hashing uh internally. So SHA 2 SHA 3 for everything else uh we use uh optimized circuits so GAN circuits uh

for all the pre-ompiles and cryptographic operations such as signature verification etc. And the whole bundle of that is basically linear ZKVM. Uh I'll also just give a very quick timeline. We had our mainet launch in August of 2023. Uh we became proven fully proven only in February of 2025. But in the interim we've uh on the London hard fork but in the interim we've upgraded to Ozaka. All right. So um let me talk about uh uh basically client diversity and the strengths that we see in our approach with respect to that. So the first point I want to bring up is that uh we don't suffer from this uh compiler blackbox issue that is uh

yeah that is uh something that's being talked about. um we directly prove the execution of EVM bite code and of the state transition function. Uh our constraints reflect directly op code semantics and the architecture of the EVM from storage to memory layout etc. Uh this is true also of our struct of our traces which both in structure and in contents directly reflect the execution of the state transition function which for us is bas uh EVM and uh yeah as a consequence we don't have a notion of system calls or interacting with the Linux AI at all.

Uh we also by virtue just of the fact that our stacks evolve completely independently of other ZKVM stacks. uh we have no correlation failures failures to be expected with anyone else. Uh um we also directly by virtue of us directly proving EVM execution we have uh substantially smaller traces. Another fact is that uh uh for instance for catching like uh uh certain calls to pre-ompiles etc. Since we have a explicit understanding explicit uh uh uh yeah basically we we know when it happens in terms of our constraints we have it's very natural for us to basically redirect um data etc to specialized circuits. So

the integration with these custom circuits is actually quite natural for us. So I also want to highlight so those are the strengths that I see in terms of our approach with respect to providing diversity. Uh the strongest being potentially this uh no correlations no failure correlations but I also want to highlight some unique complexities that we faced and uh that we actually overcame in uh to a large extent. Um those complexities being the EVM itself, the fact that it's a moving target due to its evolution and hardfox etc. but also just the history of how the project uh uh developed and sort of very collective eclective kind of constraints. Um all of these were sort of salvaged or uh uh overcome uh through

design choices by basically compartmentalizing a lot the complexity but also uh on a constraints language level. Uh we've made great strides by introducing this uh uh uh constraints DSL which we call ZK assembly and which will uh figure prominently in what comes. All right. So in terms of the EVM and its complexity, a lot of that complexity will be common to basically any ZKVM. You have to manage call frames, RAM and ROM, this sort of stuff. As already mentioned, we don't have this notion of interacting with an OS.

So that's uh uh that's makes our lives somewhat easier. We also have this uh idealized model of memory which is that of the EVM itself where memory are totally disjointed from one another. There's no notion of reallocating memory or anything. memory belongs to a frame uh isn't shared and uh is yeah essentially infinite in some sense. The real complexity or real substantial amount of complexity comes from yeah ethereum itself in particular it's state managing the crude state during the execution but also the machine state. So everything around gas warmth refunds op codes themselves uh the state roll backs. Uh the matter of the fact though is that this complexity or this problem

was is essentially completely solved uh for about a year ever since we had a fully proven London release uh in February last year. And um in terms of us uh shooting at an uh moving target uh so following up keeping up with our hardox etc. that adds for us a development overhead because we have to yeah um hard fogs mean changes in uh EVM instruction set or the semantics of op codes or new transaction types etc. um we've been able regardless to basically catch up over a period of about 9 to 10 months uh uh to the latest hard Oaka and uh a lot of that velocity actually came from us uh using or

transitioning away from the old way we were writing constraints to the ZK assembly way and um yeah this has basically sped up development and is going to continue uh as we transition fully towards ZK assembly and So yeah this is my last point uh the sort of historical development of our project uh if you look at our spec it's very clear that for instance we were uh anchored very strongly in a certain we had very strong assumptions about the underlying base field of our arithmetization for instance and this yeah this uh seemed like it was sort of um keeping us in a particular arithmetization but uh

yeah basically thanks to these progresses we made in uh in our language DSL is that where we were able to or we are currently able to basically reinterpret these existing constraints and move away to Koala Bear which we uh will be releasing relatively soon. Um and uh another point is that everything that's been written in ZK assembly and at this point most of our arithmetization is in this DSL is by construction actually field agnostic. So it has no notion of an underlying field. All of that happens in a sort of a constrained compilation step that comes afterwards.

Yes. So, uh basically the the takeaway is that we're fully uh moving towards the ZK assembly stuff. Uh we want to be we want to apply this uh both to the pre-ompiles that I mentioned earlier which are currently written in ignitions that are managed by the prover. And uh another reason for us moving in this direction besides field agnosticity and ease of maintenance and upgradability is that it uh has allowed us to integrate uh with formal verification uh tools such as pickers uh which previously in our old system was uh um not really possible and we are baking formal verification methods into the language itself.

Um yeah, and I just finish with a bit of a road map of uh what's to come. Um and um yes, I guess I'm done. >> Great. Thank you so much. Uh great to see if integration for Q2. Um couple questions from Kev. Um curious how you debug logical bugs. For example, if you're implementing an EIP and it's not passing Ethereum tests. Um so this is uh in some sense it's relatively straightforward because we have these uh uh we have these traces that are a very faithful reflection uh of uh what happens inside of uh uh

the state transition function itself. So we we can basically inspect the traces and and see what goes wrong. Um, typically it's uh uh yeah, typically the the when we get to that part of the the project debugging let's say the the changes and semantics of mod x for the pricing of this op code etc. It's a relatively straightforward even though even a little tedious but it's a very straightforward path where basically by visual inspection we just understand where where our tracing goes wrong. Um it's uh it it is the the the the the in some sense the most fun but also the least difficult part of um um of implementing let's say a new EIP.

>> Got it. And second question, do you have performance numbers for the STF? >> Uh for the STF? So we're using Basus STF. Do you mean for the prover or for the >> He probably means the prover that would be my guess. Yeah. >> Yes. So uh our prover is uh uh currently running uh our conflations take about half an 30 minutes to prove. So we're uh still a ways from uh real time proving um and um yes but uh as I said we are currently running on CPUs. Our goal is to um basically um upgrade our constraints to become parallelizable. Uh which is uh yes it's part of our part it's it's part of our steps to the um

real-time proving road map that I mentioned at the end. Um yeah and uh we also he also hope to get some significant performance boost from transitioning to a small field uh koala bear. >> Nice. seems that Colar is becoming more and more popular and uh yeah Kev is asking is that with continuations and Alex replies with continuations we can do less. Okay, we're running out of time. We have two more presentations. Uh thank you so much Olivier. The last one is uh interesting is from uh Carl. It's a um implementation of DVM in rock uh what used to be called and it's in

Karl Palmskog: Rocq EVM

the context of of formal verification. Uh so K the floor is yours. >> Okay. So yeah so hopefully you can see my my screen now. Um >> yes. >> Okay good. Yeah. So I'm Carl. I'm an academic researcher uh in Sweden. So this is more work I call it an EBM specification but I would say that's kind of synonym in some sense for implementation or definition. Right? So just to give you a little bit of background. So the rock prover is I would argue a form of programming environment. Uh but uh it's a bit different from a lot of other like regular programming languages in that it kind of doesn't compile to anything out of the box. So it gives you a very

powerful typing system uh but then you sort of uh get something that is akin to Haskell without the IO monad. uh and it's very popular or rather popular among uh researchers who do programming languages and uh reasoning about them and uh I guess one of the points I'm here is that it also supports uh extraction of code. So you can sort of go from a definition in in rock to uh to a C program or and also further to uh risk five program using a verified compiler like comfort and yeah it's been around for uh in some form uh for 40 years uh now around or a bit more and usually there are kind of releases every

year that accumulate new changes and so on. uh and uh inside of Roxite has a big ecosystem and one specific uh one specific point is is the mathematical components library. So this is kind of a replacement for the standard library of rock which is many people would argue not not the most coherent library. So math comp is much more coherent and it's very well designed. Uh so it deals with mathematical structures like groups and uh and so on. uh and there is also a tool for kind of helping you to define your own structures called hierarchy builder. Uh and uh I guess here is where they it sort of uh diverges a bit from the implementations we talked on so far.

So this is kind of optimized for proof uh so mathematical proofs which are machine checked and uh yeah I mean it's this library has been used a lot for for math and CS. Uh so our goal here was in this project was to essentially define a canonical definition in rock of of the EVM uh to be used for example by other researchers but also for uh people who are using formal verification and so on. Uh and the again the focus at least for this definition is ease of reasoning rather than execution. So I view kind of execution as a separate step where you take these definitions and refine them uh in a pro proven way. Um and then you may get executable codes you can use

verified crypto and so on. Um and the point the goal is to maintain this as all of these kind of rock itself evolves and also math comp and the EVM and uh yeah hopefully it can be uh used by a lot of researchers and so on. uh and hopefully we we can also uh release versions of this so people can use it as a kind of uh reference for uh when they are kind of for example verifying smart contract languages and so on. So we will see how that works out. It's more social social matter. Uh so this uh one of the one of the components of this form of definition is a library for machine words. So this is like a way to reason about uh machine words in an abstract

mathematical way. So I just show you a very small fragment here of a Shaw definition. Uh so they are kind of meant for being understood by I guess mathematicians and computer scientists and then they can sort of use them uh to uh to refine for example for performance and this is licensed under MIT. So our uh or at least my work in progress definition of this EVM that's licensed under Apache 2.0. So you can see the public preview here on on GitHub. I'll post a link in the chat. Uh and we're using this old uh definition in a meta language called EVM by Uichi who used to work for Ethereum Foundation. Uh so that's at least my reference point for kind of see if it's it can be proven to

be equivalent. Uh and we also of course want to test with uh the usual tests but that needs then we need to refine it first. So hopefully uh so just very quickly we will uh that's work by my colleagues who who have a tool chain basically for uh for going from raw code to verify deficient code and also we want to use refinement automated refinement proofs for this. So that's it. Thank you K. So just to make sure I understand um you have your own formal semantics of the EVM in rock. you're trying to prove that it's equivalent to Yoichi's uh LEM EVM and then assuming that these are equivalent you know that

could potentially act as a good base for the definition of the EVM and then we have these like certified compilers that could allow us to extract C programs that we can run efficiently on >> right so I think there are two there are two ways right so I mean this uh this kind of proving the equivalence that's one thing but I mean you can you can you can also to kind of go directly to just uh refine it to something that maybe is not so fast but is is enough to actually run a test right I mean you can execute things inside of rock itself so this uh for example the verified compart compiler has been executed inside rock it's just quite slow right so but in the first step you can you can just kind of write a function inside rock which can then be for example extracted to a camel

and this is probably enough for running against tests and so on right so that's that can be done in parallel with this proving exercise which I think is more academic I guess. >> Got it. And talking about the the the compilation, Alex Hicks is asking, "What bpock performance could you be could you expect when compiling to risk 5 via 30 or compset?" >> Yeah. So I mean it's it's hard to say beforehand. So I I would uh so because there are lots of tricks you can do, right? So for example, you can insert uh I mean you could sort of leave a hole for some verified crypto code that you kind of insert maybe you prove that other in some other setting right uh so I think there are lots of tricks here as

as long as you kind of obey the form of verification results you can optimize in lots of ways so I would say it's a bit too early to tell uh exactly what performance we can get. >> Got it. And when did you start working on this? Yeah, I mean I guess last last year um maybe the around summertime something like that. So yeah, and I guess the like extraction libraries. So we build on also lots of other like earlier libraries like this Jasmine and so on, right? So it's more like we we looked at we looked at the whole ecosystem and kind of try to pull out the parts that people had worked on before that were appropriate.

Kev asks, is it possible to do all of this in lean? >> Uh, so probably the definition could be ported. So, uh, but uh, so again, I'm trying to use the the strings of this mathcom library. So, unfortunately, I think lean does not support this mathemical structures. So, the exact library cannot be ported to lean due to this. But probably you can do something very very equivalent to lean. It's just that there's a kind of ecosystem of of how you do proof. So it's basically a style of of proof style of reasoning where you do lots of rewrites. I think that could be emulated in lean but uh it's uh it's not as you would have to do a lot of

work on top of lean I guess. Got it. Um cool. Um thank you so much Carl and good to know that the repo is now open source. Uh maybe it was open source earlier today or or yesterday. Um yeah, and we have the link in the chat. Cool. Uh next up we have our final presentation and congratulations the 70 people who made it uh so far. Um Ryan from who will be talking about Zero OS.

Ryan Zarick: ZeroOS

Ryan, the the floor is yours. Uh, we can't hear you, Ryan. You might be muted. >> Now, you're still using uh Zoom here. All right. Okay. Uh, hi. Um, Raz, co-founder, CT of L layer zero. They were talking about zero OS. I'll try to go fast here. So, the promise of ZKVMs is that you can run any code. So, you just compile uh to Risk 5 and you're done. The reality is that's not true. There's a massive compatibility gap. I say compatibility does not mean uh uh like uh software compatibility. So when you're writing

your Rust code like any of these Rust libraries, uh they are expecting an OS environment uh which that does not exist. Uh so you end up having to fork uh all of your dependencies and make modifications to them so that they work directly with the risk 5 part. So the current workaround is fork rust tool chains patch thinner library uh and pray that it compiles. Um but the problem here uh is that your application uh that that you are actually forking the rust code and that's the standard library part and it becomes very fragile and it only works with that version of rust that you're doing uh and it will break on the next one. So this creates this long-term pain where you are trying to keep up with uh

every release of Rust. Uh you lag the upstream uh security fixes, expanded trusted computing base uh you know as rust matures has a mature uh you know security pipeline uh you your fork loses that protection. Uh every patch of uh that you you add uh increases this audit audit burden. There's also language hell itself uh where you only support most of them are only supporting rust which means you miss out if you need for some reason C or C++ code uh that becomes a pain as well and then fragmentation. So every ZKVM is also doing this process of maintaining their own version of rust uh and choosing which you know uh which versions of rusted upstream fixes to take and then going through this hell.

Uh so we needed a fix at this OS level. Um so introducing zero os is the solution that does uh operates at a different layer right it does the sys call trap handler uh implements uh the Linux sys call uh and traps at the boundary so what is zos it's a universal modular library OS uh acts like a unic kernel so you only compile what you need uh for what you're using it for results here is that you can just take offtheshelf R code in general uh like 99% of the creator should just work. Uh you automatically get the upstream fixes from Russ uh when when they make changes to the uh the language. Uh it's language agnostic so it should just work with

Russ C++ uh go is on the road map for us in the future. Uh and then obviously if everybody takes on a zero OS there's this shared kernel across all ZKVMs um that have this uh the all these benefits. uh design principles. It's single core, no interrupt, no preemption. Uh fast fails, so if there's up codes that are not or parts that are not implemented, it will fail at runtime. Uh it won't, you know, quietly fail there. Uh so you can make adjustments. Uh and then modular, you only uh include uh in your creates what you need. Uh overhead, uh so it is only 128 instructions per sys call. uh it is relatively neg negligible compared to the billions of calls seen

in block transitions. Uh so we did a demo uh and we had this code available on GitHub. Um we can I'll share the links after. Uh we did parallel signature recovery. Uh we implemented uh zero in Jolt. Um we used uh offtheshelf rests recover signers. Uh all clients need to do some multi-threaded version of this. Uh we did that with Brianna enabled. Uh and here is uh a snippet of that code right off the besides the the jolt macros at the top. uh it is just generic rust uh no extra modifications needed to jolt itself besides the zeros inclusion. Uh we call recover signers the actual pulled that library in called recover

signers uh and then printed out the results. Um here are those results uh where it ran them this proof worked and it was valid and did the multi-threaded version. Uh all you had to do for the dependency side is just include include uh thread and std out from the zeros side uh in your crate and it just works. That's it. Uh and then you pay for what you use. So it is only uh those parts of the library from zero are included nothing else keeping uh your code and what you compile small and light.

Um and it uses the standard Linux pis call pattern. Right? So these are all sis calls that were used uh in that signature in that example uh and they just work um language support. So we support rust C++ um and then uh goes in the road map ISA risk 5 uh technically you should be able to just use uh you could we could build in MIPS or ARM or anything else uh it is just and the idea here is it's a bridge between them. So you could in the future have rust uh go to the your rust code that was working 5 go to a myip space based one later and not have to make many modifications is the the dream the zeros delivers what zkms originally promised. Uh no one wants to maintain

the two versions in that example. Uh you would have to have two uh you'd have to fork ref and modify the recover signatures and have to maintain two versions of those. Uh this just works. Uh and then here's the resources uh for everything and I'll show the presentation and the links uh after. >> Okay, fantastic. Thank you uh Ryan. Uh I guess one question I have is what is the the business use case for implementing this? Um so from from like uh our side we just wanted we were building Z applications and we just wanted uh we realized that uh it felt kind of un like unsafe that we'd have to be keep taking on uh any

modific side uh that this whatever ZKVM we chose to work on that they would have to make a change and then we'd have to like take that new audit risk and so we wanted to build something uh that our stuff worked for and then we would put it in a ZKVM um that kind of reduces the the security uh risk from our side. It's like this is open source uh MIT Apache license. Uh we uh we want this to get implemented everywhere because we want to use it. >> Got it. And in those ZK apps that you you're working on, have you been using ZKVMs other than Jolt?

>> Uh we've played around with uh a couple ZKVMs. Uh we we talked we had some conversations with uh Succinct and others about Zeros recently, but we haven't used Zeros there. used it on on Jolt so far alone. >> Got it. Kev asks um in this model would all guest programs rely on the zeros tool chain i.e. a bug in zeros could mean a bug in correctness. >> Yeah. So if everybody implements this there that is the risk there is like obviously we all inherit like Linux and other other parts of uh what you're running on that are the risk profile. So the idea is that if everybody's working on this through like pros and cons, pros is that we're all working on the same uh

the same tool chain and so we're all contributing to making fixes and we can all get multiple audits on this one thing versus everybody having their own forks and they're getting their own audits and they're all kind of going in fragmented direction. Uh but yes, then there is obviously the trade-off there. That trade-off is that uh if there's a major bug here, they could introduce a bug on multiple CKVMs. So, uh, nothing's free, but we think like the risks, uh, the the reward the risk is worth the reward here. >> Jordi from asks, uh, does ZKOS uh, require MMU in the prover side? I I guess he means zero OS.

>> Yeah. Um, unsure Isaac, you're or GX, are you on >> memory management unit? Yeah. So I think um in the tra I think it's just like a it works well with the current stuff in the tracer we have like you look at a jolt trace we have that implemented but we don't have actual implementation of that on the kernel at least in the in the case then demonstrated. >> Okay. But uh but you should uh go into the link uh the integration guide look at exactly how the J team integrated zos

into jolt which is facilitating the team to integrate that. >> Yeah. Talking about jolt I'm expecting them to make a some sort of an announcement and presentation in the next call. Um you're one of the first teams to kind of make use of them which is uh which is really cool. Um Kev is asking uh what is the base ISA um needed for uh for from a ZKVM in the context of zero OS.

Uh I think it's uh right um I was just answer I think it's generic generic like I think it will work on both 32 or and 64 but in the case of jolt I think we tested with 64 564 IMA IMA okay got it any further questions before we wrap up this very very long Cool. If not, uh just to remind you, we have the very first uh ZKVM breakout on February 11th and on March 20th, we're going to have a dedicated uh Padon uh

call. Thank you so much everyone and see you see you soon. Have a great day. Bye.