ZK14 - lambda-vm: minimalistic and performant zkvm - Diego Kingston (Aligned)

15 May 2026 · 13:52

Diego Kingston of Aligned presents LambdaVM, a RISC-V-64 zkVM built with LambdaClass and 3MI Labs, recorded at Zero Knowledge Summit 14 in Rome. He covers how the team designs AIRs to minimize constraint count without sacrificing soundness, why they chose Lean 4 for formal verification of the zkVM's correctness, and their post-quantum approach: 128-bit security, no trusted setup, and hash-based proving throughout.

Speakers

Topics

Transcript

Really happy to to be here with you. And this is collaboration between aligned lambda class and our amazing partners from 3MI Labs who have been helping us developing the design and everything. So, the idea is not to talk precisely of like some cryptography part, but mostly behind what is behind the design philosophy and why we need yet another ckvm because there are many.

But we see that there are like some problems in in the space related to them. And so we wanted to to address this using the same philosophy we used in in other places. So basically what we think is that our application is going to be okay because we coded whatever we did and then we assume that the rest is going to be okay and there will be no problems. And if you've seen lately, there have been a lot of attacks due to for example supply chain attacks or because one of the dependencies you had had some some kind of flaw or

somebody introduced like some some bug. And the thing is that if you look at the code bases of most ckvms, they are hundreds of thousands of lines of code. And even though like you have like nice security arguments and everything, one thing is what you have in paper and another thing is what you have built. Um and so the problem is that um any of these things can fail and you see that you have a very big attack surface, big assumptions, and then auditing these uh becomes uh really painful.

So, um there are like three things that we we see that keep happening. One is that you don't own your own stack. You depend on a lot of things that others build. And then, for example, there may they may introduce like a subtle bug and that's outside your area of control. Then, a lot of um people generally create a lot of like abstractions, unnecessary abstractions. Uh and that makes things uh very uh hard to reason about.

Uh and it doesn't make your code uh more maintainable or simpler to understand. It makes it on the other hand, really complicated. And then, of course, the problem is that if your uh code base is really large, then nobody can read it all, reason about it, understand the different dependencies. Um And these are not bugs per se, but they are I think perhaps like poor engineering choices because they make uh your system really really fragile.

So, we betted here on on the opposite. The idea is that most CKB VMs got really performant by adding a lot of like clever tricks and a lot of optimizations. Here, what we said is we are going to do the opposite. We are going to make something that is like really simple, has a very minimalistic code base, and it is performant. So, what we are going to do is stand with one ISA. We are going to use one lookup argument, one memory model, so that our VM is really simple to understand and the code base is really easy to audit.

And this is the same philosophy we use with Ethrax, which is the execution client developed by by Lambda Class, where you have the whole client in around 60,000 lines of code, and so that is something that is really easy. In fact, we wanted to make it even smaller. The idea is to optimize um a lot, and we think that in this era, where people like bytecode, having something that is really simple is the way to go. It's really easy to to write code bytecode, but that makes everything like really, really big, and then it hides a lot of subtle bugs, and

we are going to see more exploits, not less, due to bytecode. So, as I mentioned, the idea is that we are following the same philosophy. Uh the idea was that with the execution layer, you can read everything, you have everything vertically integrated. We use Rust, we use few generics. Uh we think that you achieve performance through clarity, and if we focus on long-term maintainability, which is something that uh some projects don't take into account.

And the idea here with the CKB VM is more or less the same. The idea is that all the crypto primitives will be precise are precisely in the code of the VM. We have exactly one language, Rust. Uh the idea is 3 MI Labs developed a very nice spec that we are currently optimizing, and the code maps one-to-one to the spec. And the idea is that all this makes it really easy for the code to be formally verified, which is one of the requirements the EF is putting forward, and is spending a lot of money to ensure that we don't have any bugs.

So, to give you an idea of the architecture, or at least the the structure of the VM, the idea is that we have 14 tables, more or less. Uh 18 chips and and templates. The idea is that we have the general like CPU chip that dispatches to to the rest. And this makes it like very easy to reason about what's going on with the the VM. And then the idea is that as in the rest of the VMs, we have uh a memory argument that um unifies everything.

And the idea is that the spec is like really clear and we know exactly which kinds of variables we're using in uh each case. So, the idea is that most of the constraints are simply reusable. So, we have like what we call templates. And the idea is that we have uh bit templates, sign, also addition and and subtraction are inlined for performance, negation. And of course, we have the the decode table, but that's mostly like a lookup. And the idea is that it's really easy to to compose uh the different things.

As for the chips, we have like some related to control and instruction fetching and and decoding. Then we have all the part related to arithmetic, then uh to memory. And of course, then we can extend uh everything to make it more efficient by adding specialized coprocessors. Uh the idea is that we work everything on a log up bus. And in general, the signatures are pretty small and we keep just uh one running sum. We don't have complexities, for example, related from having like local lookups and global lookups.

And the idea behind the proof system is go really easy. So, we are going to use a 64-bit field, in this case Goldilocks, using a cubic extension so that we can really target 128 bits of security. Uh we are using fry because it's really well understood. There are a lot of efforts at formally verifying it. For the time being, we are going for uh Keccak as the hash function. Then we are going to see if it makes sense to use an algebraic uh hash function or we could use, for example Blake.

The idea with the lookup is precisely use um log up and then for the memory, it's like a standard offline check. And the idea is that Sorry, it says conjectured, it's probable. So, the idea is to have 128 bits of probable security. Um So, um then, of course, for for the memory and everything, the idea is that um we can do this in the offline check and so we will carry information about the address, the value, the timestamp. And since registers are accessed uh pretty often, the idea is to have a special uh

way to deal with registers that is simply an an optimization. And then what we are going to ensure is precisely that when we read a position and and then we write, there is an increase in in the time timestamps. We still have to think a a more about recursion. We are also thinking about using a streaming uh prover. And we still have to to give it like some thought, but the idea is to use something simple.

Some people use, for example, elliptic curves to try to simplify some of these things. We want everything to be, of course, post-quantum secure. So, we are not going to use any type of strategy. And the idea is that the current state, which, for example, can prove Ethereum blocks using Ethrax, is only 20,000 27,000 lines of code. That is like pretty simple. The idea is to go less than that, but in the end, I think we will end around 35 or so.

And the idea is that we also have like minimal dependencies, and that way we can control what we have. So, we are not publishing numbers yet, but uh the idea and the numbers preliminary numbers that we have is really good. We are close to in performance to many of the state-of-the-art VMs. We hope to optimize the design a little bit more before we we release it. And um the idea is that right now we are on this version. We have to add like some few co-processors to make it like faster to verify Ethereum blocks, adjust uh the security.

And then uh we are also right now working on the GPU version. So, the idea is to have the GPU version uh in the coming weeks. And then we are analyzing some alternatives, maybe adding Logup GKR. From the performance point of view, it doesn't change much in terms of memory use. It's really good. Then we have to see some strategies to maybe shrink uh proof sizes. And of course the Ethrex integration is is done. We have to still improve some some parts, but it's working and so we have a full stack with minimal dependencies.

And well, this is just the idea to proving Ethereum blocks in in real time. And so we are using uh Ethrex. With that we get the risk five 64 IML, and then we run that on top of the Lambda VM. We generate the Stark proof. The idea is to compress it so that it can be be then uh verified in the L1. And so, well, the idea is that we want to make uh this VM as minimalistic as possible. We take into account every line of code.

Uh we try to have as few generic parameters as possible, as few dependencies as possible, and as always try to keep a one-to-one spec-to-code constraint ratio. So that it is easy to audit and and formally verified. And so, the idea is this is not a new philosophy. We are doing what we did uh with the execution client. The idea is this is going to be open source. Uh we plan on on releasing really soon once we uh finish some optimizations and and checking the spec and everything.

And the idea is that a reviewer can easily read everything in in a whole week. And the idea is to precisely make these small enough to formally verify and to prove Ethereum. So if you want to learn more, you can come and talk to us. And if you obviously have questions related to cryptography, you can also ask our guys from ThreeFold Labs who are amazing. Thanks a lot for for everything.