Kevaundray Wedderburn:Okay, I think we can, get started.
Transcript
Kevaundray Wedderburn:Well, but… My screen.
Kevaundray Wedderburn:The Zoom is recording… okay, cool.
Kevaundray Wedderburn:Welcome to the L1 ZKVM breakout call number 3.
Kevaundray Wedderburn:Today… We have 3 items on the agenda. The first one is an update on EVM ASM.
Kevaundray Wedderburn:The second, which can be rolled into the project updates, is an update on the DevNet for the ZKCL, and the third one is the project updates. So just starting off with the first one, Derek, if you can…
Kevaundray Wedderburn:unmute to give us maybe an update on EVM ASM, and maybe a small introduction to what it is, in case folks don't know.
Derek Sorensen:Yeah, absolutely. It might be easiest if I can share my screen. Okay, perfect.
Derek Sorensen:Let me… Okay, how's the font size?
Kevaundray Wedderburn:It's looking good on my end.
Derek Sorensen:Okay, anyone… Does anyone want it any bigger?
Alex Hicks:A bit bigger would be good on my end, because I'm on a laptop screen.
Derek Sorensen:Let's see, is that better?
Derek Sorensen:Okay.
Derek Sorensen:Right, so, a… EVMASM is a project that was, started recently by Yoichi.
Derek Sorensen:At ZK Security, and, I have recently started to contribute to it, and so any caveats on, I guess caveat on, on…
Derek Sorensen:I don't know. There are probably some details that UHE will know better than I do at this point, but let me just kind of give you an overview of what this is and where we're at.
Derek Sorensen:Evmasm is an attempt to write a guest program for, L1 ZK EVM… ZKVMs, the EVM in… directly in RISC-V assembly. And so there are some good reasons for doing this.
Derek Sorensen:Yeah, lean… Lean4 is a good place to do this. First of all, we can formally verify and have really high assurance at a very low level. Second of all, AI… Gen AI is very good at,
Derek Sorensen:if it's constrained within the context of a, like, a proof system, like Lean 4, you can get it to reliably write good code that is also correct, because you have to… you force it to be proved correct with regards to a spec.
Derek Sorensen:So, we have a formal specification of RISC-V through SAIL, and we have a formal specification of the EVM, that was done by NetherMind that was extensively tested, and there's kind of a whole story there. So, the idea here is to, write
Derek Sorensen:the EVM in assembly for RISC-V,
Derek Sorensen:Prove the RISC-V bit of it correct with regards to sale, prove the EVM bit of it correct with regards to our EVM spec, and have it as optimal as possible, and importantly, have it maintainable and kind of generatable through AI.
Derek Sorensen:And, because everything is proved correct, we have high assurance that the AI has done its job. So, no human has to do all of the super low-level, painful, painful things. So, let me just give you…
Derek Sorensen:a quick overview, so in EVMASM, there are two key components. There's a model of the RISC-V,
Derek Sorensen:of RISC-V, and within that is the EVM implemented with RISC-V semantics. So, I'll start really quickly with the… looking at RISC-V.
Derek Sorensen:If we go to,
Derek Sorensen:Yeah, if we… if we just go to this basic file, RISC-V has… we have, I think, 55 of the, RISC-V opcodes implemented here.
Derek Sorensen:Which is a subset of the full RISC-V, as I understand it, but kind of the ones used by the EVM.
Derek Sorensen:And their semantics are given in this execution, file.
Derek Sorensen:So, for example, add.
Derek Sorensen:I have been working today, to prove this… there's… there's sort of a… there's the…
Derek Sorensen:The state is, modeled by this machine state type,
Derek Sorensen:And there's, kind of the program counter, things like that, and so today I have been proving it equivalent, with regards to the sales spec, which is kind of done here. And so, I've made my way through. We've been able to prove so far that 24 of the 55 opcodes are correct.
Derek Sorensen:And then, on the EVM side, we have, as I understand it, so I guess here are the opcodes we have implemented.
Derek Sorensen:Each opcode, for example, AND, Here has, the format is pretty consistent, and so there's,
Derek Sorensen:There's a program, file which gives you the actual opcode, in… so, yeah, this is, in, kind of, RISC-V instructions, and so, yeah.
Derek Sorensen:And this is all done in 64 bits, and so,
Derek Sorensen:And so the spec of this comes in kind of a limb spec, so you're looking at, the behavior of the opcode based on its 64-bit limbs, and then a more high-level
Derek Sorensen:like,
Derek Sorensen:spec for the full 256-bit. And all of this uses horror triples and separation logic, if that means anything to you.
Derek Sorensen:so, where are we at?
Derek Sorensen:From a high level, I guess…
Derek Sorensen:So, from the EVM, this is, this is,
Derek Sorensen:We're having Claude maintain a plan and keep it up to date, so if you want to know at any time, you can always look at the plan.
Derek Sorensen:Like I said, we have many of the opcodes on the RISC-V level implemented.
Derek Sorensen:And we're working on formally verifying those.
Derek Sorensen:And we've done kind of the more basic ones, and there are some more advanced ones, to… to do next. From the EVM side, as far as I know, so the kind of 54, these, like, primary opcodes, they're all done. They're all at least, implemented, and they have a spec.
Derek Sorensen:We haven't yet formally verified anything against the EVM spec done by NetherMind, which is a little bit of a higher level of abstraction, so that's kind of… that's a to-do.
Derek Sorensen:But… and then, there's stuff, relating to, like, memory, state transition function hasn't even been started yet, I don't think.
Derek Sorensen:And, you know, so there's a lot to do on that side, from the implementation perspective of the EVM, as well as from the verification. But…
Derek Sorensen:this has all been done in the context of, I think, just a couple weeks, maybe 2 or 3 weeks so far, and
Derek Sorensen:And… yeah. So we're… the goal is to,
Derek Sorensen:make this as secure as possible, of course, with the goal of it being bug-free, as efficient as possible, and then also as easily maintainable as possible. And so, a lot of the work here is going into the workflow for GenAI, so that,
Derek Sorensen:So that we can reliably have the most high-assurance guest possible. So in some ways, it's kind of an experiment, but we've seen a lot of… we've seen enough, really high-quality
Derek Sorensen:products of Gen AI when handled by experts, that we, are optimistic, I guess.
Derek Sorensen:So, I think that… that is my… that is my update.
Kevaundray Wedderburn:Thanks, Derek. There's a question in the chat by…
Kevaundray Wedderburn:Alexandra, it seems that the overall size of the EVM implementation is very small. Is that around 1,000-ish RISC-V instructions for the EVM?
Derek Sorensen:That's a good question. Let's…
Kevaundray Wedderburn:I guess…
Derek Sorensen:me.
Kevaundray Wedderburn:VM implementation's not fully complete yet.
Derek Sorensen:No, it isn't fully…
Alexandre Belling:Yeah, so just to clarify, it's because I saw that, the implementation was using, like, 20-ish PIS5 instruction per opcode, and, for 50 opcodes. I believe it's only, 25% of the VM up codes, or something like that.
Alexandre Belling:If my count is right. So yeah, that's why I was, basically eyeballing, 1,000, research instruction, but I remember seeing a complete health program for the EVM, and it was, like, more in the 100 thousands.
Alexandre Belling:So that's why…
Derek Sorensen:Maybe…
Derek Sorensen:So something like Byte is… more involved.
Derek Sorensen:Mole was more involved.
Mamy:So, I think one of the reasons is that a complete ELF program generated for a ZKVM is likely to have lots of extra functions for,
Mamy:Accounting, for example, gas costs, function calls, etc, while, if you start from assembly, you remove all of that overhead.
Alexandre Belling:Yeah, that makes sense.
Alexandre Belling:Because the compiler would intuitively try to minimize the number of instruction code per EVM execution, while here it's, basically minimizing the program complexity, because it would just be too complicated, to do one function for Gaza counting or stuff like that.
Mamy:I can't say. I haven't looked at EVMAs yet.
Derek Sorensen:Hard for me to say, I… yeah, yeah.
Derek Sorensen:Things may get more complicated with the STF, that will definitely be, quite an involved…
Derek Sorensen:Yeah, hard to say.
Mamy:if we start doing, those kind of efforts, on, formally verifying low-level primitives, I'm wondering if we shouldn't try to formalize, air,
Mamy:representation, because I know that in the past, some of the teams that were trying to add GPU acceleration, they basically reused the weakness generation from, let's say, SP1 over 0, and then they plugged that trace into their own
Mamy:GPU prover.
Mamy:And if we have this kind of,
Mamy:formally verified serialized error, we can also have in that AVM ASM, some kind of, some of the opcodes are really, they have no branches, like all of those divMod,
Mamy:Add, or etc, and we can… Decide to generate, how do you call that?
Mamy:An optimal, error constraint, because if you look at the ad…
Mamy:opcodes. Right now, it's very inefficient due to, all the carries.
Mamy:I would even implement it differently in RISC-V using unsaturated arithmetic, but we could bypass that by having, similar to EVM ASM, some kind of EVM error.
Mamy:formally verified for just the opcode that are… that don't have, branches. Because we… we can just, we know that the trace with error that we generate will be minimal for them.
Kevaundray Wedderburn:This might be too in the weeds for this, for this particular call. Maybe we should take it off.
Alex Hicks:So, if I can add one quick comment, just for the sake of, kind of, completeness, and then we can move on. So, one interesting thing, actually, that came out of, of this effort, Mammy, is that Yoshi did…
Alex Hicks:had a look at basically comparing some of the assembly that Claude was generating for this to some of the assembly that was being generated by the Rust compiler.
Alex Hicks:And, one interesting thing was that Claude produces more straight-line code, whereas the Rust compiler produces more branching. And so, for some quirky reason, Claude is actually producing, at least in some cases, more optimal assembly than the Rust compiler does, because it has less branching.
Kevaundray Wedderburn:Thanks, Alex. I guess one.
Derek Sorensen:restaurant.
Kevaundray Wedderburn:Before we wrap this up, Derek, do you have, like, any aspirational,
Kevaundray Wedderburn:Goals as to when you think we could possibly prove
Kevaundray Wedderburn:The SDF, or even just the EVM part.
Derek Sorensen:aspirationally.
Derek Sorensen:I think we can make a lot of progress in the… in the next couple of months.
Derek Sorensen:I think it's… it's not… it's not…
Derek Sorensen:Out of the question that within a few months, we have something that's… that's working?
Derek Sorensen:I… yeah.
Derek Sorensen:I hesitate to commit to any, you know, any of that, or, you know, I, I feel very optimistically about the speed of this
Derek Sorensen:project, but I also… I also don't want to raise expectations, unreasonably.
Derek Sorensen:This is… this is… yeah, this… this is a really interesting exercise in low-level programming with… with Gen AI.
Derek Sorensen:And I think if we succeed here, then that may have other implications for ZKVM's optimal implementations of things.
Derek Sorensen:But yeah, personally, I would, you know, during the summer.
Derek Sorensen:I would really like to have something, like, working that we can actually
Derek Sorensen:Try to plug in places and see what we get.
Kevaundray Wedderburn:Great, yeah. I mean, yeah, that sounds amazing. I look forward to, sort of, more updates on this to see how far you guys go. And yeah, thanks, Derek, for sharing this.
Derek Sorensen:Yeah, yeah, no problem.
Kevaundray Wedderburn:The next one, I think we can just go onto the project updates, so just going into the execution witness and, the guest program.
Kevaundray Wedderburn:updates by Ignacio. We can do the DevNet updates, once we get to Francesco.
ignacio:Sure, can you hear me?
Kevaundray Wedderburn:Yep.
ignacio:Yeah, we'll share the screen.
ignacio:Can you see my screen?
Kevaundray Wedderburn:Yo.
ignacio:Cool, yeah, so just before the project number one updates, I just wanted to mention that, with Cody, we did a presentation from… for the EPF study group of CKVMs for Ethereum.
ignacio:So, if you are interested in having, like, a, let's say, complete picture of what is CGVMs for Ethereum, I highly recommend
ignacio:Looking at this, Youtube video on…
ignacio:Or the slides, if you watch.
ignacio:So, regarding project number one, which is the execution witness, we have some updates,
ignacio:So, developer Rucha has been working on this new Engine API RPC proposal, which is called Engineer Paddle with Witness. So, the idea here…
ignacio:is that we have a specialized engine API RPC that… can, do…
ignacio:Like, two things, in a single call, which is getting the execution witness for a new payload,
ignacio:Which is something that now we have to do with two different RPCs, the usual engineer payload and the bug execution witness. So he has been working on formalizing a spec for this new engine API RPC.
ignacio:And, there are pretty good results into this strategy.
ignacio:So I highly recommend anyone interested in this in looking at his, execution API PR and his E3X implementation branch, that is a work in progress.
ignacio:Regarding the specs and tests for execution witness generation,
ignacio:We have been working pretty heavily on this in the last month. We have,
ignacio:Yeah, 139 new tests covering a wide range of
ignacio:Important cases to check that the
ignacio:Execution witness generation ELS is built correctly.
ignacio:The current testing coverage is pretty good, in the sense that all the fields of the execution witness are covered, you know, like.
ignacio:reasonable scenarios. There are still some of them that should be covered, mostly regarding really weird water cases of getting out of gas in
ignacio:Particular situations that can create some kind of partial execution witness, but we will keep adding them in the near future.
ignacio:And also, all these releases, that we are making are for… Tests that…
ignacio:Can be run in the current…
ignacio:In the latest, Val DevNet,
ignacio:chain. So, basically, this is mainly to simplify EL's life, because they are mostly working on the latest Baldemnet for Amsterdam.
ignacio:So, they're gonna use the same branch to run these tests and see how it works.
ignacio:Regarding, ELs working on this, we have some progress here, so I3X is already passing the, this version, this version of the, of the release.
ignacio:So that's pretty good. They are not passing the latest one, because I created this latest release, like, just some days ago.
ignacio:But there's good progress there. Reth is starting to…
ignacio:More formally build the correct branch structure to start running these tests.
ignacio:Kept these some, GAF PRs to…
ignacio:Also be able to facilitate running these tests.
ignacio:And, some from Silkworm has wrote an…
ignacio:a cool document that goes through a more, like, step-by-step reasoning on why checking execution windows in a guest program is needed.
ignacio:Maybe for many of us, this was somewhat obvious from the start, but…
ignacio:I think this is very useful to really keep explaining the logic behind all these decisions, so highly recommend you read his document.
ignacio:And yeah, that's everything for project number one. I will continue with project number two, which is about guest programs.
ignacio:On this front, we also have a new release.
ignacio:In this case, in the last update, we have some kind of draft-ish spec of the guest program.
ignacio:Now we can say we have a fi- like a…
ignacio:kind of finally complete, spec. Of course, things can change, but the spec is complete, in the sense that the host program is in the spec.
ignacio:And, we also have, 25, tests for testing that the guest program
ignacio:will reject invalid execution witnesses. This is extremely important to test correctly, because
ignacio:Even on… even if you are running budget blocks, if you get a wrong execution witness, being because
ignacio:you don't get enough information. For example, you don't have all the bycodes that you need for execution, or the NPT proofs of the state accesses are not correctly constructed. The guest program must fail, and…
ignacio:Because it cannot really act on data that cannot really be checked correctly, so this is very important to have good coverage.
ignacio:So, yeah, the release is the same as the execution with those tests.
ignacio:And the strategy for… Running them is the same as I mentioned before, you can run it on…
ignacio:Your EL working branch, that is targeting the latest PADEV nets.
ignacio:Yeah, that's it for project number 2. I have updates for project number 6, but I can't do them later.
Kevaundray Wedderburn:Perhaps we don't do it numbered and just do number 6, because, the benchmark in Leeds
Kevaundray Wedderburn:Follows on from just the guest program.
ignacio:Cool, I'll continue then.
ignacio:So, regarding benchmarks and metrics, we have some interesting new library. This is a lib SST library, written by Lambda class.
ignacio:So this, Rusts…
ignacio:SSC library is mostly constructed to be really performant, focused on CEVMs, but it also has good performance in normal execution.
ignacio:There's a interesting blog post, that goes into more detail, so maybe you are, if you are interested in this topic, you can read this blog post.
ignacio:And also, this library is constructed to be no STD, which is a requirement for
ignacio:for the CGVM standards case programs.
ignacio:I integrated this library into AirGuests, which is our repository, which has the Ethrex and REST guest programs.
ignacio:And I confirmed that this is, this had a 2x speedup in the public input calculation, because the public input is calculating the history root of a structure.
ignacio:So yeah, in the overall picture, this is about, like, a 5% speedup on the whole block proving time, which is pretty nice.
ignacio:And this also allowed, to comply to being OSTD, for all the dependencies of the guest programs. So, any CKVM that supports running OSTD programs,
ignacio:It would work.
ignacio:So yeah, and on the right, I have some screenshots of the repository,
ignacio:benchmarks, that is comparing to other known SSC libraries out there.
ignacio:So something else, that,
ignacio:I, I did is, like, a refresher of this CG, these 6…
ignacio:emulator profiling tool that the Six team has.
ignacio:This is basically a way to provide guest programs.
ignacio:Without, like, actually proving the blocks, so it's basically kind of an error cost, kind of profiling.
ignacio:I did this a while ago with a version 0.14 for CISC, and I kind of refreshed it with the latest release and some improvements in the guest programs.
ignacio:And we have seen really good results. This also materializes the ellipse SSC, your library, improvements, and allow us to keep
ignacio:Keep track of, like, where the proven cost is going.
ignacio:So, yeah, this is pretty nice.
ignacio:And finally, I am working on some integration of how to transform all these benchmarks, proving time results from the East benchmarks.
ignacio:Into concrete repricing proposals.
ignacio:And we already have, like, our own dashboards for things, but I thought it was interesting to say
ignacio:Maybe we can use the same methodology that is being used… that is being used for Glamsterdam repricings.
ignacio:Because at the end of the day, if you use re-execution times of logs, or proving times of logs.
ignacio:The analysis for concluding which is the right repricing for opcos or pre-compiles should be…
ignacio:applicable. So, what I did is I took, Maria's, repository, where she has, all this analysis pipelines to conclude your repricings for
ignacio:from re-execution times, and I kind of adapted it to proving times.
ignacio:and basically… yeah, what I want is to, yeah, stand the shoulders of this world, so…
ignacio:We can reuse, the analysis part of, of…
ignacio:Of what we need to get into the conclusions, because…
ignacio:hopefully we know how to reinvent the wheel on how to conclude new prices from data. So that's kind of the idea, and these reports are automatically generated whenever we have new benchmarking numbers, so the whole idea here is to just go from data to conclusions.
ignacio:In an automated way, and pretty fast, so we can see how things look like.
ignacio:And yeah, that's all from my side.
Kevaundray Wedderburn:Great. Thanks, Ignacio.
Kevaundray Wedderburn:Checking to see if there are any questions, while it's happening, Margin, if you wanna…
Kevaundray Wedderburn:share your screen. I guess some things to note, just as a small summary, is that the witness generation, as I wrote, has gone down by 20x, and this was just from switching from JSON RPC plus JSON to HTTP plus SSD.
Kevaundray Wedderburn:The 2X in ZISC cost reduction, was mostly from optimizing the DMA in the GPU, and I believe, memcopy.
Kevaundray Wedderburn:And… Yeah, I believe those were the two big optimizations that we saw.
Kevaundray Wedderburn:There are no questions, so…
Kevaundray Wedderburn:Martin, do you want to take it off?
Marcin Bugaj:Yeah.
Marcin Bugaj:So, can you hear… can you hear me?
Kevaundray Wedderburn:Yeah.
Marcin Bugaj:Yeah, fine.
Marcin Bugaj:So, today we are doing a quick recap of Project 3, which is CKVM Guest API standardization.
Marcin Bugaj:All standards are in the ZKVM standards repository.
Marcin Bugaj:We now have 5 standards accepted.
Marcin Bugaj:First is RISC-V target triple, which is a minimal 64-bit ISA for proving Ethereum blocks.
Marcin Bugaj:Second, is the I.O. interface, a portable ZKVM-independent way, to receive private inputs and emit public outputs.
Marcin Bugaj:Enabling zero, copy support for data transfer.
Marcin Bugaj:Third is Cryptographic Accelerator C interface, which is basically a C header exposing EVM precompiled equivalent operations through a common C API.
Marcin Bugaj:And two new standards, were merged since the last
Marcin Bugaj:ZKVM breakout call, those are execution termination semantics.
Marcin Bugaj:Does a standard,
Marcin Bugaj:That happens… the standard… the standard… it standardizes what happens when a guest program ends.
Marcin Bugaj:And it says that successful execution may produce valid proof, but failed executions cannot.
Marcin Bugaj:The next standard is memory layout restrictions.
Marcin Bugaj:Ckvms are free to define their own memory layouts, and CKVMs must provide linker scripts.
Marcin Bugaj:So, the standard is basically permissive. It says that, each CKVM is free to define their own memory layout,
Marcin Bugaj:A quick reminder on what these standards mean in practice for ZKVM vendors.
Marcin Bugaj:So, many ZKVMs still run on 32 bits, and the migration to 64 bits is expected.
Marcin Bugaj:On the Rust side, the Rust target is bare metal, that implies no STD support.
Marcin Bugaj:So, every guest program has to be compatible with no STD.
Marcin Bugaj:And if it depends on STD, it won't… it basically won't compile.
Marcin Bugaj:On the AIO and accelerator side, please make sure that these are part of the SDK.
Marcin Bugaj:Good news is that, some ZKVMs
Marcin Bugaj:already implemented partial API conformance for accelerators. It's actually close to completion in at least one of them, and we'd like to see the rest of the KVMs
Marcin Bugaj:Implement those standards.
Marcin Bugaj:And finally, Ethereum Foundation can dedicate engineering time to help the KVMs, to help vendors implement those standards, so,
Marcin Bugaj:If any support is needed, just reach out.
Marcin Bugaj:And two new proposals. The first one is Mimo Memory Resources.
Marcin Bugaj:The problem that it solves is that the memory layout restriction standard, which just was accepted, lets each vendor define their own memory layout, and that's a right call, but it creates a gap, because every vendor can lay out memory however they like.
Marcin Bugaj:And guest, guest program authors have no idea how much stack and heap they can safely use across
Marcin Bugaj:all the KVMs.
Marcin Bugaj:So this proposal closes that gap, mandating a minimum.
Marcin Bugaj:Every conforming ZKVM must provide at least a certain amount of stack, and at least a certain amount of heap.
Marcin Bugaj:If a guest program fits within those minimums.
Marcin Bugaj:It's guaranteed to run on any conforming implementation.
Marcin Bugaj:The specific numbers for the stack and heap size aren't in the proposal yet.
Marcin Bugaj:They are, they are placeholders. We need to profile the most demanding guest programs under, realistic
Marcin Bugaj:Conditions before we commit to… values.
Marcin Bugaj:That work is ongoing.
Marcin Bugaj:The next standard is memory safety guard regions.
Marcin Bugaj:Right now, the KVMs have no reliable way to catch two of the most common low-level bugs. No pointer dereferences and stack overflows.
Marcin Bugaj:ZKVMs are bare metal systems, so without operating system or hardware support, and these kind of bugs would lateralize silently. The program corrupts memory and keeps running.
Marcin Bugaj:Potentially producing a proof of a broken computation.
Marcin Bugaj:This proposal fixes that with, two mandatory guard regions.
Marcin Bugaj:Small zones of memory that are deliberately left unmapped, so any access to them triggers abnormal termination.
Marcin Bugaj:The first memory region is,
Marcin Bugaj:It's for, catching null pointer traps.
Marcin Bugaj:The first 4 kilobytes of the address space are reserved, so any reference immediately causes abnormal termination instead of silently corrupting memory.
Marcin Bugaj:The second is a stack guard region. Also, 4KB region sitting just below, the stack, so that when the stack overflows, it hits the guard region, and the program terminates.
Marcin Bugaj:There is one limitation worth mentioning.
Marcin Bugaj:The stack guard doesn't catch, stack clash.
Marcin Bugaj:vulnerabilities, that is when a single large allocation skips over the guard… the guard entirely. There is a compiler-level fix for that, but we can't mandate compiler… compiler flags in the Zacavian standard.
Marcin Bugaj:They are basically recommended in the standard, so we recommend that guest programs enable those flags when compiling their guest programs.
Marcin Bugaj:We implementation, we expect,
Marcin Bugaj:The implementation costs vary, quite a bit across different proof systems.
Marcin Bugaj:Yeah, that's no data for that yet.
Marcin Bugaj:Please review the proposal, and leave feedbacks for the last two proposals, which are under review.
Marcin Bugaj:Yeah, so that's it from my side.
Kevaundray Wedderburn:Great. Thanks, Machin.
Kevaundray Wedderburn:Checking for questions, tao, if you want to share your screen while…
Kevaundray Wedderburn:Ruben says, for the accelerators, I proposed…
Kevaundray Wedderburn:Two of these, maybe we can take that async,
Kevaundray Wedderburn:Because I think I'd need to review those.
Kevaundray Wedderburn:I can see your screen, Tyle.
Kevaundray Wedderburn:But I can't hear you.
Kevaundray Wedderburn:Oh, mic issues…
Francesco Risitano:Walter, can you hear me now?
Kevaundray Wedderburn:Great, yeah.
Francesco Risitano:Okay, cool.
Kevaundray Wedderburn:But I can't see your screen anymore.
Francesco Risitano:Yeah, I'm gonna reshare that for one moment.
Kevaundray Wedderburn:Okay, cool. While that's happening, Ruben, I think, exposing Catch ActF is probably a good idea, actually. Maybe the same with Shorty 56,
Kevaundray Wedderburn:Okay, cool, yeah, I can see your screen now.
Francesco Risitano:Cool.
Francesco Risitano:Yeah, so the key update is, we've essentially been able to deploy a test network
Francesco Risitano:And run it end-to-end with a GPU-based, prover backend.
Francesco Risitano:the kind of initial tests that I've run are…
Francesco Risitano:more focused on integration as opposed to performance, but the general idea is, you have a single, kind of, property or YAML file which defines the, test network services, so we deploy multiple beacon nodes, multiple
Francesco Risitano:validator clients, we have a proof node.
Francesco Risitano:And, some additional, kind of, auxiliary services, Grafana, Prometheus, etc.
Francesco Risitano:So we've, we've…
Francesco Risitano:heavily leveraged, the kind of frameworks that PandaOps provide, and I'll speak about them
Francesco Risitano:shortly, but ultimately, yeah, we have a pretty, kind of, easy-to-use framework now, or at least it's, there's PRs open to, kind of.
Francesco Risitano:Provide this functionality, so sometime soon, we should be in a position for,
Francesco Risitano:yeah, just single command deployment of, test networks. As I say, I… we can't do it now, but it's across many, kind of, PRs and branches, so, once that's cleaned up, I will, share the… share the commands, and if anyone's interested in using this, then, do reach out, and I probably will share, some…
Francesco Risitano:Instructions in due course as well.
Francesco Risitano:On that note as well, I did speak with Manu from Prysm, and we have kind of provisionally
Francesco Risitano:kind of targeted the tail end of next week for, an initial interop, DevNet, so that would be between both Lighthouse and Prism.
Francesco Risitano:I need to touch base with Manu to see the status of his progress, but, you know, hopefully if progress is going well on his end, then we'll be in a position to, to proceed with that at the end of next week.
Francesco Risitano:Moving on to the consensus specs, there's been some updates to the P2P protocol, specifically the introduction of two new message types, the first of which is execution-proof status.
Francesco Risitano:And this essentially allows peers to communicate, the latest block that they have been able to validate using execution proofs, such that peers can, kind of strategically
Francesco Risitano:Choose, you know, which peer to request and sync proofs from.
Francesco Risitano:And secondly is execution proofs by range, which essentially just allows you to request,
Francesco Risitano:Proofs for a specific range of blocks.
Francesco Risitano:We've got a more general refactor, and this,
Francesco Risitano:Covers a number of, kind of, open…
Francesco Risitano:Issues or unresolved, points in the, in the specs.
Francesco Risitano:One of the big changes was the proof node API, so ZKBoost, which is essentially the service that the consensus layer uses to generate proofs. It's an external service. The API for that changed, so we had to kind of propagate that through to the consensus specs.
Francesco Risitano:And that there's one open question, relating to the execution proof status, which I just, touched upon. The proposal here is to introduce proof types as well, so that, peers can gossip
Francesco Risitano:And essentially, like, announce or publish which proof types they support, such that we can kind of dynamically,
Francesco Risitano:You kind of iterate or migrate to new proof types,
Francesco Risitano:So, that could potentially be used for bug fixes. That was a proposal by Kev. But yeah, it's still a bit of an open question at the minute, and we haven't concluded on a… on, you know, how we're going to proceed, but there's an open PR for those changes.
Francesco Risitano:Then, yeah, we made some changes to Kurtosis, so this is the ETH PandaOps framework that we use to orchestrate deployment of DevNets and testnets.
Francesco Risitano:So you essentially just need kind of a container orchestration backend, either Docker or Kubernetes, I believe, are supported. And yeah, you can just, kind of spin up these environments with a single command. Previously, it didn't have support for GPU backends, so we introduced that.
Francesco Risitano:And similarly, in the Ethereum package, which is essentially the layer that sits on top of Kurtosis and defines the shape of the network, we added GPU support for that as well.
Francesco Risitano:Then on the Lighthouse side, introduce some…
Francesco Risitano:observability, observability features, so essentially just, metrics which are pushed to Grafana, sorry, to Prometheus, and then Grafana consumes them.
Francesco Risitano:And, I've provided a link here to the, to the network parameter file, so essentially the DevNet, config, config file. And if anyone's interested, they can use this to spin up a GPU, backed, proven network.
Francesco Risitano:And yeah, on top of that, there's just been various different, Lighthouse changes to align with the updated specs, and, yeah, a few optimizations as well.
Francesco Risitano:Yep, that's all from me.
Kevaundray Wedderburn:Thanks, Tom.
Kevaundray Wedderburn:Just looking for any questions in the chat.
Kevaundray Wedderburn:Are the lighthouse changes upstreamed already.
Kevaundray Wedderburn:So currently no, but we're in talks with Lighthouse for upstreaming, these changes.
Kevaundray Wedderburn:Checking for any over questions…
Kevaundray Wedderburn:If not, then, Han, do you want to share your screen?
Ladislaus:Oh, there's another question by Bonamas, whether the prism changes the upstreams.
Kevaundray Wedderburn:It's been done by Manu, who is on the Prism team. I believe we're using a Prysm branch, so it's not necessarily in the main Prism
Kevaundray Wedderburn:Like, the main branch that they use?
Kevaundray Wedderburn:Cool. Yeah, this is great. A lot of progress, and yeah, I know, Tal, you've been working on it for quite a bit, and pushing a lot, so yeah, this is great.
Kevaundray Wedderburn:Han, do you want to share your screen?
Han Jian:Yeah, sure.
Han Jian:Tao, could you… oh, yeah.
Han Jian:Can you see my screen now?
Kevaundray Wedderburn:Yeah.
Han Jian:Okay, so, yeah, I'll get some update on the project file. So, on the ZKVM integration side, we upgrade the disk to 0.16.1, and we see some good performance improvement.
Han Jian:And on the proving pipeline observability side, we integrated open telemetry in Array and ZKBoost, so we can see the proof traces from Grafana clearly.
Han Jian:And we also added another separate simple dashboard in DKBoost for real-time event and historical proof monitoring, and you can see more details in the latest release in DKBoost.
Han Jian:The Grafana dashboard looks like this. You can see, for each block, you can see the trace in each part, how it takes, how much time it takes.
Han Jian:And if you don't want to set up the whole stacks, the ZKBoost also provides a single page that shows what's going on internally.
Han Jian:And next, we'll try to integrate the cluster client directly into ZKBoost, if we are going to eventually request the roof creation on the cluster, so we can bypass the array, hub.
Han Jian:And also explore the proof cancelling, so if the block proofing takes too long, we can cancel it to avoid the proof request queuing up, and then keep improving the observability. And that's the update for me. Thanks.
Kevaundray Wedderburn:Thanks, Helen.
Kevaundray Wedderburn:Just checking for any question, are all of these dashboard views provided via Grafana?
Han Jian:Some of them, yes, and the custom one that you just see is… is, like, the… is separated. You don't have to set up the co-funnel to see that.
Kevaundray Wedderburn:Cody, do you want to share your screen while we field for more questions?
Kevaundray Wedderburn:Okay, cool.
cody:Alright.
cody:Yeah, so on security…
cody:The structure of the slides is almost the same as last time, but with some updates on each. So, regarding RISC-V compliance, I mentioned this Act 4 upgrade, which is a change to the testing infrastructure from the RISC-V community, from RISC-OF to, this Act 4
cody:framework, and having run that, I've found quite a lot of compliance issues and some new bugs, which I have reported, to the various ZKVM teams.
cody:And I'll say more about those down the line, but it's very fruitful. This is coming from… from new tests.
cody:And also extending some of the testing.
cody:To a new extension, which is, to do with misaligned instruction, loading.
cody:And…
cody:Oh yeah, and also, the testing is now doing proving of these, test binaries. Like, my monitor is doing this, and not just executing them, and also verifying, and there were some interesting results there as well.
cody:We have some grantees working on fuzzing, and they're finding, bugs, which we'll disclose, eventually, but we have good progress there.
cody:And, on the topic of speccing, I was speaking with Alex Hicks about the question of whether the sale spec, which you heard mentioned in Derek's presentation, will cover this, these unaligned accesses.
cody:And the relevant extension is this one here, which is listed in the ETH Act standards. And, Alex found this active PR and engaged with them there, so it looks like they're working on
cody:I'm giving good spec coverage of this extension imminently, as well as, broadly speaking, Improving some of the…
cody:The testing and configuration framework to make it clearer what,
cody:You know, what your model spec is covering.
cody:When you're doing, testing or formal verification from sale.
cody:I also mentioned, this question of what does formal verification give us last time, and I pointed to a paper by Nadeem Kobasi, that found some issues in, formally verified libraries, and just yesterday, another paper came out,
cody:by the same author that is now finding some issues with the HACS framework.
cody:So I don't have firm conclusions for that, but it feels like a noteworthy development to make people aware of. He does point out some strengths of hacks, but he's also able to push through some buggy code and have it be accepted.
cody:In some… in some sense, so…
cody:It's something that we'll want to look at when we, start to adopt formal verification.
cody:And I posted these kind of preliminary SNARK specs that I had been working on. The idea just to extract really simple Python implementation of ZIST's
cody:approver…
cody:And, this time I now have something similar for OpenVM, and the goal here really is to see whether the workflow that I developed for doing this before translates well, and I think it does, based on this experiment with an OpenVM ProverSpec, because it was done with
cody:I would say less than half as much effort,
cody:both in terms of time… wall time spent. I spend even less of my own personal time prompting
cody:And, I mean, less than half…
cody:And in terms of token consumption. So, I think we can produce really simple implementations that are reinforced by strong testing as the beginning of a specification.
cody:If we want to go with Python specs.
cody:So, that's my update for today.
Kevaundray Wedderburn:Thanks, Cody. Any questions?
Kevaundray Wedderburn:Let's see…
Kevaundray Wedderburn:I guess I have one question, Cody. Could you maybe say your thoughts about, this Nadeem Kerbesi…
Kevaundray Wedderburn:Paper, and yeah, what are your thoughts with respect to formal verification?
cody:I… I've only read a bit of the paper, so I don't have much of an impression of it.
cody:it seems to point out that there is a complex pipeline that transforms Rust into something functional, which can then be transformed into F-star. I…
cody:I don't know if we would be using F-star, I think…
cody:we would be using lean. I don't know if the same, I suppose, similar issues apply.
cody:Yeah, I don't know. I mean, I don't know if we plan to use hacks or where we plan to use it. For me, the question is…
cody:sort of where… You know, on the timelines that we're talking about, say.
cody:well, for optional proofs, I don't think we require formal verification,
cody:But maybe as a security requirement for mandatory proofs, we would. And…
cody:the question for me is, like, where can we be really, really confident in the correctness of the software based on formal verification? And that has to do with being really explicit about the boundary and assumptions.
cody:And making complementary test coverage to that. So, progress is moving really fast. I'm always trying to
cody:Pin down exactly what the progress means.
cody:And… for now, I don't feel I have a strong confidence in any particular, formal verification,
cody:assurances, but I, broadly speaking, am very confident we'll have some, and so it's kind of a conversation with the practitioners, to know where we need to provide complementary efforts.
Kevaundray Wedderburn:Cool. And, Alex Hicks from the snarkification team wants to quickly comment, I think we have, like, one minute.
Alex Hicks:Yeah, so on… on the hacks bit, just because you were… you were asking about it, so I think, it was a really interesting paper, I think, so any extraction from Rust, or any language, C++, Java, whatever, that people commonly use to any proof assistant is always trusted, because the language that you're…
Alex Hicks:Extracting from typically does not have formal semantics, and so you always have
Alex Hicks:an issue in that sense, that the translation has to be trusted. With respect to…
Alex Hicks:what Nadeem found. It's actually quite interesting, because, well, we kind of assume that there can be bugs in these tools, because they're trusted, and the tool chains can sometimes be quite extensive.
Alex Hicks:But it was very nice to actually see concrete instances of such bugs being reported. There are other bugs that we know of, which are just kind of routinely fixed, so with respect to the…
Alex Hicks:would be the one that we might use and tease as well, on evaluating this, and they've been fixed. But it's possible that there are more. And one approach that we're taking also to deal with this is, obviously, that we've explored
Alex Hicks:other options to verify things, one of them being just writing assembly. EVMASM is an example of this, and then the other is just actually compiling from,
Alex Hicks:specifications in our clib with, what would be a formally verified compiler, and so we're, we're luckily not over-committed, you know, to using these toolchains, because we know there can be bugs, and they also have other limitations, actually, which they don't support all of Rust, because some Rust features are just hard to map into Lean safely.
Alex Hicks:Let alone someone who do map and have some bugs. So it's, it's nice to see the work that's being done on this. I was quite happy Nadeem worked on this, and, luckily it doesn't affect our plans too much, other than being a good reminder and, to the
Alex Hicks:point, Cody was making, I think, it was a plan from the start of the product to have a final report at the end, for whatever we use to verify production code, to have both an audit of it, and obviously detailed documentation of boundaries. So that is, that's still the plan.
Alex Hicks:And we'll have, obviously, more to say about this, and I'll be very happy to discuss this more in other calls, actually. I think it's quite important.
Kevaundray Wedderburn:Yeah, great. Yeah, thanks, Alex. And, yeah, just on time as well. Yeah, so that's the end of the breakout call. Thanks everyone for joining. I will see you guys in roughly one month.
Ladislaus:Folks.
Chat Logs
00:15:12
Alexandre Belling:It seems that the overall size of the EVM implementation is very small no?
Is that around 1000-ish R5 instruction for the EVM?
00:15:35
Alex Hicks:the STF will be much bigger though
00:17:45
Alex Hicks:can we talk about optimizing the produced assembly?
00:19:12
Alex Hicks:ok Mamy is doing it :D
00:19:54
Mamy:xD
00:20:24
Yi Sun:One concern about EVM -> AIR directly is that the correctness of the AIRs depends on the global memory / execution model of the zkVM.
00:20:37
Mamy:this should use unsaturated arithmetic. And there is a formally verified ways of doing this in fiat-crypto
00:20:49
Alex Hicks:PR this to claude.md please
00:20:54
Alex Hicks::)
00:20:56
Tamir Hemo:It also depend on field sizes etc
00:22:04
Tamir Hemo:To add to Alex point we can also add skills for the AI to write zk optimal assembly vs hardware optimal
00:22:23
Alex Hicks:yes that's the idea, the performance profile is obviously very different
00:22:34
Mamy:One concern about EVM -> AIR directly is that the correctness of the AIRs depends on the global memory / execution model of the zkVM.
I wonder if we can have a common AIR serialization format that can handle the variatiosn between the zkVMs?
00:23:00
Alexandre Belling:For direct assembly-written EVM, I expect the auto-precompiles approach might work well.
00:23:42
Alexandre Belling:As there would be typically not that many modules. And that would also avoid to maintain an AIR for EVM opcodes
00:23:47
Yi Sun:Replying to "One concern about EV..."
One concern about EVM -> AIR directly is that the correctness of the AIRs depends on the global memory / execution model of the zkVM.
I wonder if we can have a common AIR serialization format that can handle the variatiosn between the zkVMs?
I think this might be difficult. We have a separation between these as the “Core” and “Adapter” part of chips in OpenVM, but I wouldn’t expect the separation to generalize across different designs.
00:24:40
cody:Does evm-asm currently give a way to execute a RV64IM binary?
00:28:32
Derek Sorensen:Do you have a link for these specs and tests?
00:29:42
Kevaundray Wedderburn:Replying to "Do you have a link f..."
Its in the execution specs: https://github.com/ethereum/execution-specs/tree/projects/zkevm/src/ethereum/forks/amsterdam
00:34:52
ignacio:slides link proj 1, 2 and 6 https://docs.google.com/presentation/d/1YPIU2jPPTetAUw_qzQsefKntXIqOPeFZja7udtFVQUI/edit?usp=sharing
00:35:07
Ladislaus:Hat auf "slides link proj 1, ..." mit 🙏 reagiert
00:38:33
Mamy:@Alex Hicks https://github.com/Verified-zkEVM/evm-asm/issues/175
00:38:50
cody:Replying to "Does evm-asm curre..."
bump
00:39:15
Derek Sorensen:not yet, no. But hopefully soon 🙂
00:40:44
Kevaundray Wedderburn:Replying to "@Alex Hicks https://..."
We could also test this with normal guest programs too
00:41:49
Kevaundray Wedderburn:Replying to "@Alex Hicks https://..."
Maybe some sort of conditional compilation such that if the ISA has instructions like add-with-carry, then it uses saturated limbs and without it uses unsaturated
00:42:17
Ruben:for accelerators, i proposed https://github.com/eth-act/zkvm-standards/issues/23
for io, https://github.com/eth-act/zkvm-standards/issues/21
00:42:59
Francesco Risitano:Sorry mic issues
00:44:52
Kevaundray Wedderburn:Replying to "for accelerators, i ..."
keccakf makes sense — I think a lot of zkVMs have accelerators for the permutation anyways.
It would maybe make our interface incoherent however because the exposed methods correspond to evm precompiles
00:45:07
Barnabas:couple more days
00:45:32
Barnabas:just wanna make sure its very user friendly
00:45:35
Kevaundray Wedderburn:Replying to "for accelerators, i ..."
+1 on logging too — maybe @Marcin Bugaj you have some thoughts on these too?
00:49:44
Barnabas:are the lh changes upstreamed already?
00:50:08
Barnabas:are prysm changes upstreamed already?
00:52:46
Francesco Risitano:Are all of those dashboard views provided via grafana?
00:53:54
Han Jian:Slide for project 5 https://docs.google.com/presentation/d/16TJS0fwgxg9IzjLZWq-xsolKP9eOD2t6wolT-eLipfA/edit?usp=sharing
00:54:49
Francesco Risitano:Slides for consensus layer updates: https://frisitano.github.io/slides/presentations/optional-proofs-2026-04-08/index.html#1
00:54:58
Ladislaus:Hat auf "Slides for consensus..." mit 🙏 reagiert
00:59:15
Alex Hicks:can quickly comment if you want