Episode 335 - Groth16, IVC and Formal Verification with Nexus

Transcript

[Music] welcome to zero knowledge I'm your host Anna Rose in this podcast we will be exploring the latest in zero knowledge research and the decentralized web as well as new paradigms that promise to change the way we interact and transact online this week I chat with Yen Scot and Daniel minin from Nexus we start with a catch up on all things Groth 16 or grth 16 from the author himself then we cover the topics of formal verification in the context of zkps the Nexus architecture the benefits and

challenges of building a system from the ground up folding and IVC and what these properties offer in the ZK VM context and much more now before we kick off I just want to let you know about ZK Summit 12 which will be happening in Lisbon on October 8th we are excited to once again bring our our one-day invite only ZK focused event to life at ZK Summit you can learn about Cutting Edge research new ZK paradigms and products and the math and cryptographic techniques that are giving us epic efficiency gains in the realm of ZK space is limited and there is an application process you do need to apply to be eligible for a ticket and I've added the link in the show notes if you want to get that application in the deadline to apply is today so it's

really your last chance to get that application in if you'd like to give a talk at the DK Summit cool so hope to see you there now Tanya will sh a little bit about this week's sponsors Alo is a new layer one blockchain that achieves the programmability of ethereum the privacy of zcash and the scalability of a rollup driven by a mission for a truly secure internet Alo has interwoven zero knowledge proofs into every facet of their stack resulting in a vertically integrated layer one blockchain that's unparalleled in its approach Alo is ZK by Design dive into to their programming language Leo and see what permissionless development looks like offering boundless opportunities for developers and innovators to build ZK apps this is

an invitation to be part of a transformational ZK Journey dive deeper and discover more about Alo at al.org namada is the shielded asset Hub rewarding you to protect the multi-chain built to give you full control over sharing your personal information namada brings data protection to existing assets applications and networks NADA ends the a of transparency by default enabling shielded transfers and shielded cross-chain actions to protect your data even when interacting with transparent chains namata also introduces a novel shielding rewards system by holding your assets in a shielded set you help strengthen nada's data protection guarantees and collect n rewards in return namada will initially support IBC

and ethereum based assets but will ultimately serve as a single shielded hub for all assets across the multichain learn more and follow namada main net launch at n.net and now here's our [Music] episode today I'm here with Yen Scot and Daniel Marin both from Nexus welcome to the show thank you Anna I very nice to be here so I want to start with you yens I want to do a bit of a catchup folks might be familiar with you your last name Gro or Groth I'm assuming will be very familiar to a lot of our listeners and yes you are indeed the author of the grth 16 proving system when we did our initial episode many episodes ago we

actually spoke in depth about the grth 16 system and we talked about what had happened in leading up to that as well as what happened after but I think it might be fun to catch up with you on that topic I'm kind of wondering are you tracking all of the implementations of gross 16 yeah is there anything maybe new you can share yeah so so I'm not following all the implementations of of grth 16 I focus more on the science side than the implementation side but um uh we were recently at the CK proof conference in Berlin and CK proof is this standardization process where we're trying to standardize zero knowledge proofs and as part of that uh there's

now an effort to standardize gross 16 um so so I think that's very exciting that's s like the first standard that CK proof wants to get going what would that mean to standardize it like is it to choose one iteration or is it to make it a standard itself like just the research part so I think still open what exactly it means to standardize that's sort of like also part of the standardization process to to decide but the goal is to be very clear about what is a grth 16 verification and also set this standard so people can adopt it in in good faith they know they're getting the right thing right so the standard is a lot about confidence building in zero

knowledge proofs yeah also also formal verification of the verifier to know that exist yeah that was one of the efforts cool other than the gr 16 world what has happened for you since we last spoke when we last spoke I was uh working at definity and now I've switched to to Nexus so I joined December 2023 as Chief scientist of Nexus nice and what are you working on there like are you creating a new gr 16 like proving system are you working on a different part of the research yeah what kind of thing are you doing yeah so the goal really is to work on on Zer knowledge proofs and and that's why I

joined Nexus because I really wanted to work on Zer knowledge proofs and we are building a ckvm which we hope to have like working at really massive scale so we can prove that trillion CPU cycles per second so it's basically getting all of the Technologies together and of course this happened a lot in in the space uh in the recent years it's really moving very fast so it's about picking a lot of different techniques and putting it all together and choosing some points in the design space that we hope will uh get us there to this very high throughput that's cool I want to come back to exactly the the types of thing

you're working on when we talk a bit more about Nexus and the architecture there but Daniel welcome to the show for the first time tell us a bit about what you were working on before this and what your role is at Nexus before that I'll just say that uh probably when you asked Yan if he was working on a new gro 16 he wanted to hear like oh yes we're working on growth 24 or something like that maybe but interestingly it's not the case but you know maybe in the future maybe in the future I actually do track very closely all of the implementation of groud 16 but that's something else we can discuss later oh cool um yeah so a little bit about my background studied Stanford cryptography was part of the Stanford blockchain club and well

essentially while being at school started uh Nexus and the goal is just to provide like a hyperscale prover for verifiable computation that's it to enable verifiable computation and bring it to life in a really sort of like large scale really professional sort of like fashion but you're going to consider just verifiable cloud computing and our approach is to essentially combine uh scientific efforts and breakthroughs in you know from mathematics cryptography and Engineering as well as cryptoeconomic um efforts which we can discuss later as well to really build this like super powerful machine uh which we call the Nexus CBM what was it originally like was that the

original plan when you first created this project or did it have a different f Focus well it started about 2 years ago but more formally about a year and a half and the goal was to to enable verifiable computation but we were in fact taking a different approach for a short period of time of the company which was essentially cryptoeconomic security actually a topic that is pretty popular nowadays and the idea there was to use something like web assembly um as well as staking mechanisms to provide a stateless soft chain computational system that would allow smart contracts to Outsource compute to economically incentivize soft chain agents oh do you

put this in the category of ZK Co co-processors was it more like ZK co-processors and now it's changed so we usually don't call it like co-processor so usually a CK co-processor is like you use some general purpose verifiable computation system to Outsource compute from a smart contract right but it's only one application of verifiable computation right uh our approach has always been fully General general purpose from day one okay and so our goal is to allow developers to build things like ckco processors of different flavors actually and that is the primary goal when you first started though when you were talking about this

cryptographic security did you have a more narrow Focus then actually no we wanted to be able to execute in that pseudo verifiable fashion the execution of any Ross program using this cryptoeconomic incentives and actually part of the reason why is because I thought this was like two years ago that um CK was advancing not sufficiently fast in order for this technology to satisfy consumer demand but actually that changed very quickly pretty much perhaps like three months after we rised our seat round we focused 100% into CK and it all started uh when I read the Nova paper which was published in 2022 and from there it was very obvious

to me that that was the direction especially around like highly efficient proof aggregation and not only because of that paper but because there was like a stream of papers coming out of Academia etc etc that you know every couple of weeks they were popping out and we decided to go 100% into that direction I feel like I hear the term verifiable compute a lot or verifiable computation but can you walk us through what that actually is yeah absolutely so I think when people mention verial computation I actually think about a traditional cloud computing service just that it comes with a proof that simple okay and what does the proof represent though that is that instead of the cloud

is it instead of a third party kind of guaranteeing it or is it just it never was guaranteed and now it can be it can be verifiable well it was never a guarantee right now the proof um is something that uh Prov you as a consumer a guarantee but that you can also share with anyone in order to convince them about something it's always been sort of like part of our philosophy that developers shouldn't know whether they're Computing in a traditional environment or in a verifiable environment and the user experience should be exactly the same and the Nexus CBM was assigned exactly with this uh user experience in mind it's like you shouldn't know that this is a verifiable machine that this is a verifiable world

it should be essentially taken from for granted of course that's not the case because performance right but that's exactly what we're working on let's define and verifiable here like I'm trying to picture a use case of this like a developer creates a rust application what kind of application would need to be verified or verifiable or what element of the application so yeah so so first of all verifiability is about verifiability of the execution mhm and we verify that the output actually corresponds to running the program on a given input this differs from formal verification right where verifiability is a static here it's a dynamic process it goes after execution so essentially

you're trying to convince someone that some algorithm being computed is being computed correctly or more abstractly you're trying to convince someone that something is true and so there are obviously a lot of examples in the blockchain space uh we also find super interesting outside of the blockchain space what the possibilities there are even though the market is less developed but answering your question just a simple thing that you can prove is for example properties about your Google account without revealing your password right for example I could prove that I have a 100 emails from yens sent last night to me without you know maybe he was too worried about the C podcast what are we

going to talk so you know identity high security Computing of course all of private computation falls into a realm of verifiable computation there is also the field of re-execution right so this is quite an interesting property that has never existed in the history of humanity right which is the fact that if you computer proove for sound computation then no one in the whole future of humanity has has to rerun that computation because someone already spent a lot of resources in producing this proof to to add on on this right so there has been this notion of double

execution right if you have to have high confidence in a computation well how would you build that high confidence you would execute it on multiple machines maybe with different pieces of software developed by different teams of developers and so forth right and you would then compare those outputs and see do they match right and in that case you would believe leave the computation and it's really cool that even though it's much more expensive to just do a double computation right but it's really cool that you can now create a proof and now everybody has a guarantee that this is the right result and you don't need to worry about was there some random bug during the execution or whatever right that otherwise could could happen and

then to add on that if you just do two executions then you are not able to go to anybody else and convince them that this was the correct result but now when you have a proof that's verifiable by anybody then you can take this piece of data right and you can go around and show here is a proof that it's correctly computed and everybody will believe that data so you can send it around to other systems and can compute on this data and Trust the data because it has a proof and everybody in the future as well right so the the prove is theoretically valid for an infinite amount of time and that's why actually going back to our conversation of Standards standards are important because if we all agree on a

standard for a final let's say proof system like Gro 16 then my Gro 16 proof hopefully will also convince people living a hundred years into the future so like in this case you can create a proof but then people need to trust that the proving system you used is correct is working correctly and you're saying if there's a standard around Groth 16 or something and that is sort of an accepted strong proving system that people accept as correct then they wouldn't also have to audit the proving system because I guess otherwise they would potentially exactly exactly no you're totally right and I think this is something that people don't talk about too often which is like people talk about proofs and proving systems but

like no one talks about how do we convince ourselves that any of this makes sense right like you can tell me this is a proof here's like a million bytes of data and the proof system is I don't like Halo 2 so to say right well I don't know if the verifier that I'm using is correct if Halo 2 is sound if uh the prover for Halo 2 is not cheating so I mean like it it just doesn't mean to me anything right um so hopefully formal verification can help us with this as well as you more concrete estimates of like soundness and completeness properties of proof systems but just the like this is a social problem right how do I convince to you that this prove actually proves what I'm

trying to prove he and it's very hard and so far with like Groth 16 the proof of that basically comes because a lot of teams have audited and adopted it right sort of like they checked it they implemented it those implementations we assume have been extremely carefully checked and battle tested and then a lot of people use them so they've made lots of kind of there's lots of exposure of that system so if it if it was attackable the Assumption goes someone would have already done it um I always find that so odd that that's how we get our trust in a weird way it's just sort of like it hasn't broken yet therefore we believe I mean in some sense this is how the field of cryptography works

right it built our systems based on some assumptions about cryptographic Primitives that the discret logarithm problem is hard or you cannot break this lce assumption or something like that right and the basis for that trust is essentially people have thought hard about that those problems and not found a way to attack them so so there's a social process in getting to the trust right we don't have a process by which we can get trust that does not rely at all on on human effort so I do think this is something that's is part of the the system and it's interesting actually when people talk about proof systems right they say well you get mathematical

guarantees of of Truth and so forth and that is true you've sort like made some part of the trust process mathematical right but but you still do go back to some underlying assumptions right and you do need to have some human trust especially if you're not an expert in the field right you sort like have to take some cryptographers at the word that you know yes this is a secure proof system this is a your assumption to rely on so this is actually uh part of like your company strategy so to say as well which is like we recognize that a lot of this math is pretty unparsable for a lot of people and so a lot of trust in a proof system and its implementation being sound you know complete and sound

and being secure comes down to social proof and for that it's important that you like the people developing it are well World experts right um across multiple Fields whether that's compilers uh cryptography obviously to other Realms like formal verification right because otherwise how will you as a user know that you're buying into a system that actually provides security which is the core product of a system like verifiable computation right like if the people that are developing are not cryptographers or at least don't have expertise on this like how do you convince yourself my hope is that there will be a way in the future in which

trust in like experts um such as the people that we have in our team is not fully necessary because of new advances as well in formal verification which can provide undebatable proof of soundness but that is too futuristic nowadays today we just have to trust that the people that implemented aof system you know didn't miss a constraint here and there and that's pretty hard to do I feel like we should Define formal verification um I've done two episodes on this at least I know it's come up a lot but yeah can you can you explain what that actually is because it it does seem like it it's a step further than just the social it's like it's not just building something putting it out into

the wild hope like seeing if someone can break it it's actually almost like reverse engineering creating almost like a mirror project that like just makes sure that this executes the way it's supposed to um yeah let's explore that a little bit yeah I'll just say that I was recently seeing like there was like a call that vitalic gave at the Google event and he was saying like we want to move out from a just trust me bro right scenario and that's exactly what I'm trying to say right like a lot of the systems are like you know just trust me bro you know this is this is sound I've written all the constraints that I've promised to write the verifier is correct no one actually has a time or knowledge to go and check it out

themselves like I could build like approver today and say that it runs at a at a billion Hertz it's going to be really hard for anyone to contradict that claim because they would need to find a soundless uh exploit and so the hope is like with formal verification that that process can actually become automated and that it doesn't rely on social proof I think there are several layers of formal verification so like if you look at papers in cryptography right they will often come with a security theorem there will be a written proof and this is something that's developed by hand but it is a formal verification process right it's just processed by humans that develop that formal

verification of of the proof and we have seen in some cases that there are subtle details and the proofs are flawed and and so forth right so it's not a fail proof procedure but it's certainly is much better than not having a proof right if if you take a cryptographic paper that publishes some new scheme and it doesn't have a proof then it's typically a sign that it's broken okay um that is my experience like they they haven't been able to provide the proof that it works exactly so either either it's a sign that it's developed by somebody who does not have the technical competence to it or somebody who's too sloppy to do it or something else right but it it really is I think more than 50% of times if there's no security

proof it's just because it's broken mhm now if you look at the papers that do have security proofs right then they're typically good especially if it's been peer V viewed and so forth right but we do have exceptions to that as well either few cases there are really horrible flaws and and it's just completely broken quite often there subtle details and there's some Corner case where things are not quite as you expected from the security theorem so if you go a step further than that right so then you would say humans are flawed processor right humans do make mistakes humans do have a hard time keeping track of a lot of small details so you could say well can we have like a computer

system that can help us right and you do have formal verification tools like V and and Isabel Hall uh that can help you really check in detail that that a proof is uh correct right so now you would formalize the theorems you want to prove in their language and then you would use their proof system to sort like create a proof that this is a correct theorem and and they will have a a proof Checker built in that checks that indeed that theorem holds and it's even been designed these systems right so I think C you can sort like boil down to there's a core base which is actually not so many lines of code 5,000 lines of

code some I'm making up some numbers right but if you really want to verify everything you just need to verify that chunk and then you can sort like expand that out to the full system and that is what you're using to verify right so you're really trying to minimize the surface area that needs to be covered by by humans I always thought of formal verification is as more on the engineering side of things like that you've implemented it and then you create formal verification to guarantee that the implementation is acting correctly but is it more on the research side so I would think of it as as these tools allow you to prove theorems and they prove theorems about some model right so you have to model

what it is that you want to to prove something so you would have to write a model of what are sort like the the system that you're doing and and provide some theorems about that system and then you can prove that and you can actually go from direction of like if you have proof of that there are some tools that allows you to extract code from that that implements these systems right but like the opposite direction people are also interested in you know can you tie an implementation to the model that you're formally verifying right and and that would be really useful because one thing that happens is that you spend a lot of effort in creating this model and proving some theorems and now you have

an implementation that implementation goes out of sync with the model you have right because while you're updating something you come up with some performance trick but now it's actually a different system that you have than what you have in the model right so it's a very hard thing to keep those two in sync with each other and and people also thinking about how do you try to make sure that they actually do stay in sync with each other that's interesting I remember like I've spoken with some Auditors I think Auditors will sometimes do formal verification tools and there's almost like this spectrum of like the way things get checked rust in a way as a language is also doing some sort of check that things are correct that's

like a builtin I don't know if you'd call it like debugger but it's doing something to make sure that your program's exec you've written it in a way that it's executing correctly and it will kind of correct you if it's wrong then there were things like fuzzing and then on the sort of far end there was formal verification um and I guess that's why I thought of it more in the coding in like the engineering implementation side of things yes so so so I wanted to point out that the type checking system in in Rust indeed gives you some tools to formally verify things right it doesn't allow you to express everything but it does allow you to express some security properties and that's exactly the strength of rust that there particular some memory safety issues that don't occur in in Rust because you have this

type checking system um there are also attempts to build in more expressivity of of that type checking what you can prove into Ross the several projects that have tried to build sort like Advanced type checking so you can anot in the code that this these are like the post and precond conditions I expect from this function or method and then you can actually if you have built this system in you can also use the type Checker to check that those properties hold yeah I I will say that um here at Nexus we're like huge fans of rust I guess at this point it's not you know very unique but we really are so for example formal verification Tools in

Rost to verify Ros code with experimented with some of those all of the Nexus CBM is built in Rost we're working we recently launched um of course like a Ros ZK that works with Asing rust to allow you to compute multiple proofs in parallel we're working on a system that allows you to write like uh this pre-compile extensions to the instruction set purely in Rust and it's it's a little bit mindboggling to think like what you have is a piece of Ross code that verifies arbitrary Ross code it might be formally verified with rust code right so in rust on Rust somehow exactly exact actually our team is uh composed of

melians uh people that came out of the of Mozilla the project so for example one of our team members actually uh his name is Sean Shan mortell he designed the Ross logo oh itself but yeah we're we're huge Believers into into that and the reasons are multiple you know not only for from the memory safety and the compiler but also just a developer experience it's just amazing nice um and I also wanted to say an um on the point of formal verification what you said this is what we see a few teams doing that is like we Implement then we formally verify some subset of the constraints right um interestingly the approach that we've taken since day one is we first essentially like formally

Define the system and you will see that in the Nexus white paper we provide a mathematical description of the machine so quite literally the machine is represented as a touring machine so to say as an as a algorithm as a non-interactive succinct snark Etc right but it is actually represented as an algorithm and all of the algorithms are described therein and um how we do it is we compose algorithms from multiple open papers right just now as mentioned Nova hypernova uh incrementally verifiable computation systems so on and so forth and we actually combined this building blocks in a very modular way so to say to build a mathematical definition of the machine using this papers and this

allows us as well to prove that the construction is complete and sound because the proofs of soundness so to say come from the respective papers and then once the machine is mathematically defined we implement it uh once it's implemented because it's well documented from a mathematical point of view uh this gives us essentially two benefits number one formal verification is simpler because we know exactly what we're formally verifying like we didn't go out and Implement something and then try to do it instead we already knew what we wanted to implement then we implemented it number one and number two uh we hope that it will allow us to build multiple clients so not only um a rust based CBM but just as with

ethereum's client diversity for which there are like Ross and go clients so I want I want to dive into sort of the proving system and the Nexus system but before I do that I just want to one last thought on sort of the formal verification in this auditing sort of space has there been any proposals for like AI auditing like if you think of going back into that social model that you described of just like you put it out you make it as strong as you can you wait for someone to break it like can't they just and maybe not yet but like wouldn't it make sense to just like run AI agents at this thing like just throw as many hacker brains at it like has anyone done that so people

have used AI tools to find bugs and there many different tools that you can use to find bugs so it's also a question like you know how do they stack up against those other approaches right and I think I'm a little hazy here I don't know the this field very well right but my understanding is that AI is not quite as proficient as other tools in find in bugs so you would probably find more bug by other testing methods fast testing and and so forth than throwing an AI at at a system but they do find some bugs and they might might be different types of bugs right so it does give you a bit more coverage in the bug finding uh approach what it doesn't give you and

what formal verification gives you is sort like the elimination of all box assuming your model is correct right again there's an an assumption here right but under that assumption right you I don't know if any other tool than formal verification by a machine that can give you s like a close to 100% guarantee that they're not box that's cool all right let's make the move over to the Nexus system I feel like we got a little you know we got into the verification auditing world but now I want to kind of dig down into what you are building the proving system that you are talking about or even that mathematical model now I'm really curious what that looks like because you mentioned IVC and NOA when I think of a zkm I feel like

usually there is sort of a central proving system sometimes there's some sort of recursion built into it but tell me what yours yeah the Nexus ckvm or the Nexus machine really looks like and what proving systems are in there yeah yeah so first I will say that we have built essentially everything from scratch okay uh you know it's it's been essentially taking like zero amount of codes from anyone else except for our works prou and you know all of those guys the folks from Alo have contributed greatly to the artworks ecosystem so we provided the first open source implementation of the Nova proof system after Microsoft's own prototype from Street CTI right so that was great we decided to essentially

reimplement it productionize it using artwork tooling we've always wanted to have like a very solid foundation for the ckvm up on which we can iterate very fast and actually we did we provided an implementation of supernova actually very easily after the implementation of Nova was completed the implementation of Nova took quite a bit there were a lot of um engineering complications that I can talk about as well especially around two cycles of elliptic cures we implemented the cycle fold essentially techniques uh which allow for more efficient verification on two cycle of Cs and then we recently announced and released an open sourcing of the hyperd DOA proof system um it's it's more generalized it has multiple benefits

as well as the arithmetization of the machine right so we uh wrote in R1 CS the full risk five instruction set wow as well as the memory checking mechanism which is based on Merkel trees all of this and as part of R1 CS constraints we also have a part of the ckvm that has what do we call a proof compression mechanism which is essentially after we've computed like multiple rounds of IVC and IVC means incremental F computation right for the audience here um we compress the proofs because the Nova proofs are quite large and so that is well we essentially we've done it from scratch what do you use there is it a stark CU isn't it usually like I feel like there's usually like a snark and a

stark do you do that or do you just take another snark yes people sometimes do like a stark and a snark MH we have done what you could consider this is not entirely precisely true but what you consider like neither a snark nor a stark more like a Nar okay so without the S so not snar not Stark more like Nar without the suin part and that is folding one can be more precise there but essentially we make the tradeoff on the prover set of things to not be succinct the falling proof is actually the size of the circuit that is being proven which is pretty big but it allows us to do highly efficient proof aggregation right that's what folding

schemes in Nova asprova and Hova are good at and then we grab that you know real large proof and actually compress it with a snark in fact actually um three composed recursive snarks the first one of which is uh a modified version of Spartan developed by serat seti and an implentation by chenfang in artworks and then we apply a couple of other rounds the last one being uh well gr 16 okay and this is what allows us to get to the three group element uh proof size would you say then are you Supernova or hypernova under the hood and then a Groth 16 yes right now it's hypernova hypernova hypernova and then

the proof compress what we call the proof compression sequence out of which the last part is gr 16 so it don't go directly to gr 16 uh we need to do some mental gymnastics here and there to compress the proofs through multiple rounds of regression okay uh yeah because otherwise it's too much for uh grow 16 to handle there would be like a gigant circuit is this recursion done in hypernova itself or is there like another proof in between there exactly exactly so hypernova Nova Supernova and so on and so forth um are exactly the same for recr right okay and this is actually super important for example our machine is able to do IVC right just keep Computing keep Computing keep

Computing keep Computing within NE bounded and reasonably small amount of memory even your browser for example so for example you can do recursion on the browser and this is important because for monolithic snarks or Starks sure maybe you can prove a little bit on the browser if you know if your computer is pry powerful but to do recursion you do need to essentially use a lot of memory here that's not the case but the trait of that we're doing is that the proofs are large okay um and so they need to be compressed before they can be submitted to ethereum I see I want to understand the comparison here with some of the

other ZK VM teams that have come out recently so the first one I I've heard of that had the risk five instruction set was risk zero yeah and then sp1 came out earlier this year now we have jolt all of those are using Starks as far as I understand or some like you know in the case of sp1 oh jolt is not a Stark No no they they is a some Che based snark it uses a Spartan yeah oh uses Spartan okay so is that s would you say of those three then would you are you closer in spirit to jolt um because of the large field Universe yes so right now the Nex to C GBM exactly it's based on 256 speed field um snarks so yeah um

actually we're pretty close to there in terms of like like the actual field size but we don't have no allegiance to like large Fields right in fact we have been exploring quite actively small the small field Universe it just has many downsides but it also has a lot of upsides so what kind of research are you doing into the small field stuff like it sounds like would you be able to use something like Bas somewhere or is everything too built so you wouldn't be able to like sort of hot swap these things so so indeed we are looking into that right we're very agnostic about the techniques and there many techniques out in the field that we looking at so so this would be one of them so so I see this as a question of which kind of commitment scheme do you want to use to

uh commit to to field elements and then the trade off between large large field elements and small field elements um and the options you have for commitment schemes right because Peterson commitments do require large Fields but then they have nice homomorphic properties and and so forth so that that could and again on the small field side I don't know quite where the you know the landscape will will settle yet right so subas seems seem promising uh but is that what is ultimately going to win or not that's that's not clear people also looking at Lis based schemes for instance right but we're definitely yeah looking at at that as as an option right and I think the the question you could

ask is so like what is the the cost per bit that we are committing right I mean at some point we we have to look at what so like what is the raw efficiency we can get on on out of the proof system right and and we want to maximize that raw efficiency right and one metric is perhaps like to say you know what is the cost per bit that you are committing right another metric would be then okay within the proof system how many bits do we actually need to commit to at all right and there also techniques that try to reduce the number of bits that are committed right so so gkr has been successful in sort of like reducing the overall commitment surface h i uh

answering your question Anna I would say that one of the core properties of the Nexus kbm in our philosophy from day one has been essentially the observation that the ckvm can be thought of as a modular stack of components Each of which can be individually optimized and so for example uh yens and his theory team here at Nexus um and and others um we have been working extensively on what we call the arithmetization system that is inspired by jolt like techniques based on lookup arguments so what that essentially does is it's work to how to arithmetick as many CPU cycles per per

recursion batch right another direction of optimization is the prover itself uh which is yesan just mentioned we're agnostic to whatever prover we use we have built our own prover right as mentioned NOA Supernova hypernova we've built those from scratch and they couple directly with the circuits being implemented in addition to that we also have what we call the memory checking subsystem which is essentially like an independent module that does not not just CPU verification but memory checking and there's multiple techniques to memory checking the Nexus One machine that we released back in uh September sort of silently was using like a naive memory checking mechanism that was space of Merle tree right now that's still the

case for the Nexus 2 but we are um about to upgrade as well and then there's multiple other independent components like the proof compression mechanism right so that is completely decoupled and independent of all of this and then there's many more other components like uh what we call the Nexus compiler is a transpilation from risk five to just uh more and better and simpler suitable um instruction set architecture which we call the Nexus virtual machine and for example the Nexus virtual machine was actually inspired by the ethereum virtual machine and it allows us to further to do two things number one essentially you simplify risk five uh in a way that is just better suited for proving and number two to simplify it

from a human perspective for it to make it easier to audit there are some discussions here and there about whether that makes sense or not uh right now the Nexus virtual machine is essentially risk five uh with just you know tiny modifications next iterations of the access virtual machine will be most likely super sets of risk five and this gives us many many benefits but all of those components are like modular you know from the compiler to the CPU architecture to the memory checking mechanism to the pr to the artiz system to the commitment scheme to the compression system and how we work on is we have multiple versions of those in our library all of it is open source we

independently optimize them we couple them together it and that is what gives you a given choice of a ckvm that might be optimized for either proving um in large computer closers with a lot of memory usage or proving on constraint environments like a browser with small memory usage uh but perhaps more CPU intense right this has been challenging because I mean not not taking code um from scratch obviously gives you like a lot of slowdown initially right but uh it it has been very helpful to us to be able to iterate fast now that it's been built and it sounds like you had a lot of control but I I want to so you're I

think on the proving side proving system side what it sounded like was that you have this somewhat like modular you have components and you can use these optimization techniques so you wouldn't necessarily Implement like a new proving system you would just use the technique that some new proving system has showcased and then like included in what you've built potentially yeah if you can and sort of you mentioned like lookup tables and I'm assuming there's like other techniques maybe if you decide to do this small field thing I'm guessing you wouldn't just reimplement something but rather you would just try to extract what they've done and add it to your system exactly exactly so it just gets better and better and better right so from from a business perspective so to

say uh our hope is that this like the Nexus GBM can be thought on more as an ecosystem uh for cryptography where multiple implementations of multiple different schemes and components can be found and then one is a developer using the SDK can choose the optimal configuration for a given program and the good thing is that as the codebase matures and the system progresses essentially all of the applications that are compatible with the Nexus CBM you know just get better and better and better right so that's all Ross programs for now right that's good because it gives like the developer like seral fraction right um this has been also one of our core philosophies is that you should just be able to inell it run it

and get approv right yeah uh that simple and that that modular is has always been top of mine in fact I I would say Anna that our story as a company has been fairly distinct from that of others in the sense that unlike other folks that have um systems that go like super fast perhaps initially when they launched when we launched we were not ashamed to say that the ckvm ran at one CP cycle proofed per second okay one Hertz I guess this is slow it's very slow exactly so proof one cycle per second and the reason why is we folded essentially one CPU um instruction per step and this was back in September

2023 that was what we internally call the Nexus zero machine the very first version We presented it as Stanford um then around Ember of this year we presented uh the Nexus One machine the Nexus One ran at about 100 Herz on an M2 MacBook Pro 100 HZ is fairly slow uh or was fairly slow um by industry standards in that you know people say that they run super super fast we care about many things right as including recursion and proof compression and so it ran at 100 htz reason being there's multiple reasons but the the sizes of the circuits that we were proving are actually super large in the Nexus One

there were like 30,000 constraints MH which it happens just to be a lot per CPU side here at the Nexus 2 uh we have essentially Incorporated advancements from the jol techniques and this is actually something that we were looking into since like more than half a year ago which is to incorporate essentially jolt arithmetization techniques to reduce the size of the circuits so that we could pack more cycles for recre step this is exactly what we've done and so that was the next to announcement that we did probably like 3 weeks ago or something like that and there hop is to continue going in that direction across many verticals of optimization okay in collaboration with other teams as well but how fast is that one you sort of

said the 100 Hertz was one oh yeah so okay so with Jolt it gets about a 100 times faster than the Nexus one so probably like 10,000 Hertz yeah uh in our system uh but the problem is that you know being fully transparent it also has some downsides like uh doing ethereum verifiability is significantly more complex so you know it's It's tricky to just talk about Herz uh without it being like a full end to endend system so no for example like there are some systems that like you can make them go super super fast but they're just extremely hard to recurse extremely hard to compress and so it's like okay sure you

can go like super fast but it's not useful to anyone and then there are systems that are probably slower but at least are practical and you can recurse them efficiently and you can compress them efficiently that's what we had for the Nexus One machine so hope is like how can we combine this like uh all of this together so that you have a system that is fast compressible recursion friendly so on and so forth let me give you another example something that people don't talk about is you want a universal verifier and this has always been the goal uh with Nexus is that a single smart contract implementing the verifier for the machine can verify any program execution and some systems out there have the

problem that you need a different verifier for different um types okay exactly and then is that is huge like if you're a developer you would have to deploy a different smart contract for each different program right and a lot of non-cms as well in the past had exactly that problem um I myself myself face this like personally because there was some time when I was a student there that I was like trying any possible CK system out there right like circum nor I think it was in its initial base right there um also Leo right uh from the Alo team you know great products great tool chains Etc but the universality is a very important factor

uh in practice for any deployed system you just want to have one bar fire to rule them all so to say I see this has always been part of our core philosophy that is like how do we maintain that while improving performance when you talk about the universal verifier though I guess you're talking here about like the ZK VMS that are nonrisk 5 based right like in the risk five based do those also have Universal verifiers usually like the single smart contract like sp1 Risk zero and stuff like that yes and no for example the verifier may change when adding uh pre-comp to the architecture right because the circuit that is being verified actually changes so if you're a developer that uses machine architecture

that's different from other machine architecture your verifier will be different and you will need to deploy a different smart contract uh which is a which is a big deal so um right now the best system so to say have a universal verifier for a given machine architecture there might be a way in the future to even have universality across machine architectures mhm but that's not the case right now what I would say is the universality property um is not always maintained by risk 5 machines um sometimes for example uh the verifier needs to know some kind of like data from the program and that it's just like a huge trouble with the specifics of um

risk zero or sp1 um honestly we've spent a lot of time obviously you know here being in this space and reading and honestly we're not sure we're not sure about how the systems operate but what we know is how our system operates M and so with us it is like that so for a given machine architecture exactly for a given machine architecture the verifier is universe and this means like if someone deployed an application on the Nexus VM they wouldn't have to deploy a smart contract themselves it would just use yours right exactly just one universal Smart contract got it and and that's pretty much it going back to your the speed up that you're talking

about what are other areas like you sort of mentioned the Nexus 2 comes out but there's a few it's like it's faster but there's some other drawbacks what's next on your road map in that regard in terms of like adding new techniques are there any areas you're you're paying attention to well very a lot of exciting things are coming um on many many fronts so not only is the ckvm you know as mentioned like modular so we're working on on essentially every part of the modular CBM stack so our vision has always been to do large scale proof aggregation for the CBM and to essentially build an ecosystem of applications that consume compute and Supply compute so to allow

people to essentially lend their compute to participate in a really large scale computation so going back to our discussion uh that y brought up about uh re-execution um an are you familiar with a project called seti at home seti at home Siti at home from NASA and Berkeley in the so this was a project uh from NASA in Berkeley in which uh essentially NASA needed a lot of compute to do like astrophysics calculation to search for alien life in the 2000s they didn't have a lot of cloud computing power so they decided to tell people like hey please volunteer your GPU your Nvidia gpus and we going to do this massive large scale

distributive computation uh in order to achieve this and they were actually pretty successful uh they got about a 100,000 people to supply compute um and they they actually broke the record to the world's largest computation ever performed but they had the re-execution problem essentially to guarantee um correctness of this volunteer network they had to D duplicate or triplicate compute and then do use a probabilistic argument to compare uh results before actually Computing the large computation what our CBM is optimized to do our goal is just to prove really really really large statements and so what our CBM is

optimized to do is essentially to do large scale joint collaborative proving and that is where the recursion part comes in uh as a core part of the of the system which is can we essentially grab multiple proofs from multiple different people right and bring them together into a single proof that verifies a whole large confutation and so uh for the Nexus 3 uh we'll see what we'll have you know there are the improvements from the developer experience to multiple parts of the proving stack but there will be components potentially as well on the what you can call like the large scale proof aggregation system um we'll have more details there but I prefer to

keep those I want to hear so when you say proof aggregation system I'm wondering do you have in mind also like a network a Marketplace kind of scenario we've seen a lot of the zkv M sort of point in that direction so I'm wondering if if that's also on your road map we've seen a few of those conversations it has always been our goal here at Nexus essentially to we want to be able to do the largest verifiable computation ever performed that's what we want to do let's say you look 10 backs into the future we would want to say Nexus was able to run and an extremely extremely large computation that has never been seen before and well people talk about

like CK marketplaces CK networks here and there we are concerned about the problem of building a really really really large scale machine a single machine having many people work together as one so we we don't call it like Market or something like that we'll see you know I I don't want to spoil a lot of things in this C podcast uh but let's say that we are concerned about the problem of making the ckvm as powerful as possible through any means as possible that's your focus so you're not focused right now on building a Marketplace could you potentially work with a market place like you talk about

this sort of largest verifiable computation possible a joint collaborative proof but I I guess the proof itself would still ideally be smallish exactly would would like you need a special actor to actually create that exactly a special actor and so uh this actor we call it the orchestrator the orchestrator okay yeah so this is a system that orchestrates compute quite interestingly so in our white paper actually ANM this is all p in our white paper we Define the ckvm as mentioned mathematically using multiple mathematic mathematical components and one of those components is called PCD which stands for proof carrying data which is a generalization of IBC which is mentioned

stands for incrementally verifiable computation so PCD is essentially a distributed incrementally verifiable computation distributed what was it again uh what's the I a distributed increment verifiable computation okay excited so it's like you and Y and me and maybe a few other friends perhaps we can do a computation uh in pieces right and essentially user pieces to combine them together to build like a proof and then keep Computing on it keep Computing keep Computing that's the folding itself is that like each one of us would do one of the folds or like whatever one of these like iterations and then they're combined exactly and then they're

combined and then we can keep combining them and combining them at infinum so to say so actually Anna this is something else that we've been super focused on because I feel like this is something that people don't talk about is the ability to prove unbounded computations so what this means is that the ckvm is able like if you have enough patience and time to prove a really really really large computation in other systems you have to set up a static bound on the computation right you say we going to approve any program up to 100,000 steps if you want to do that you can do it but if you go want to prove like 10 101 you need to either exactly it won't

work you need either a new verifier or two proofs or something like that what we've been concerned of is can we have a verifier that is not only Universal for any program but also Universal for any length of execution and the folding property as well as the recursion exactly allows us to do that we can keep folding and folding and folding and this is the whole uh premise of like incrementally verifiable computation right and if you might see that CK rollups actually fall very nicely in this category right I think C rollups are naturally incrementally computable machines aren't they are they unbounded though do they need unbounded computation well you're going to run

your C rollup for hopefully you know for the whole future of humanity right so you can use traditional recursion to essentially combine find C rollup proofs there are some challenges maybe the recurs aggregated proof needs a different verifier than the proof for the actual execution which is a challenge it would be really nice if CK RS wear essentially just one proof right and that proof was Tiny and it just got updated updated updated updated on every block you just like have a new proof you take the old proof you combine them and that's your new proof that's the the premise of of incrementally verifiable computation right is that you need just

one verifier and you can combine the proofs over and over and over yeah that is sort of like uh her goal to enable this like incrementally machine incrementally computable machine I want to go back to the unbounded computation because it caught my interest which is like what is an example of that maybe that and we can also talk about this re-execution I kind of want to dig into like what that would even look like what's a use case there what's a use case for unbounded computation what would that yeah what kind of application needs that yeah absolutely ethereum ethereum is an incrementally computable machine the evm or any other virtual machine based blockchain system and it would be very nice for example if actually vitalic has been talking about

it he asked at some point what if we all achieved consensus on a proof system let's just say you know there's like a million other what if we decided we synchronized as humans into choosing one right well perhaps if we wanted to choose one it would be one that is potentially number one very simple number two widely understood as you know a scientific breakthrough so to say and number three that is optimized for recursion and incrementally verifiable computation right we would want to have a proof for a block for this proof to be convincing right U hopefully this proof system is very simple and for this proof to be updatable we would want that if we have essentially a proof for Block one

and a proof block two we can just like cheaply merch them together and have a proof for Block one and block two so I would say that our main goal has has been particularly proving really large computations like rollups so to say okay but sorry Daniel I keep trying it's the unbounded computation that I'm trying to understand though it's not the IVC so much so what is that is is ethereum unbounded computation exactly exactly okay that's what you're saying or roll ups use Unbound would need unbounded computation exactly exactly so if you're launching a rollup an L2 and L3 even an L1 uh this machines are essentially running an unbounded computation that

will keep Computing and Computing every day more and more and more and more right one would want to have a proof system that is able to prove unbounded computations without changes to the the universality of the verifier the verifier should remain the same and the proofs should be you know easily aggregatable so the unboundedness also helps in another thing which is on collaborative proving collaborative proving makes a lot of sense if you're proving an unbounded computation because you can keep doing it and keep doing it keep doing it and use computational resources for multiple people and these people you know they might connect they might disconnect but you can just like reallocate computational resources and

keep Computing so it doesn't matter who is doing the computation it can be um let's say stopped for a moment but restarted by any other agent this is a discussion about livess for example I'm I'm wondering if it's useful also to give sort like the original motivation for incremental verifiable computation because that was for an unbounded computation right and and the example was like you know suppose Humanity wants to compute something that will take a 100 years or whatever it will take right you don't know right so that's essentially an unbounded compet M and the question is then you know how do you sort like trust what happened 100 years ago and and why would you trust that the computation has been correct up

to this point in time right and in incremental verifiable computation you sort like do the computation in chunks and once the chunk has completed you spit out the proof right and then you do another chunk and you spit on another proof and those proofs aggregate all the previous proofs yeah right so now know that all the previous chunks of computation are correct and that led to this point where we are now and what the state of the computation is at this time I want to actually just just to clarify there because what it sounds like is more recursion just like recursive proofs like Mina the Mina system where it always had a proof and then it made a new proof with new information and the old proof but in the case of IVC it also

sounds like you're kind of like you're adding lots of different pieces of almost like a partial comp utation of a proof with an existing proof is that what it actually looks like like or is it straight up recursion in the same way so it's simpler recursion actually so so one can achieve recursion in IVC using monolithic snarks there are just some downsides falling systems are optimized for essentially enabling IVC um in a very like cheap fashion there are you know other technical details there as well but the the folks from Mina were like the original ones who propos they didn't call it that way they didn't call it IBC they just called like recr but essentially they essentially proposed

the first blockchain sixn blockchain IVC system yeah that's nice you say that actually yeah I feel like during the IVC boom of last year um I I felt they kind of got like a little bit forgotten and then people needed to remind them that there was a system that did something like this yeah yeah I remember reading the Mina white paper when I was a a and um I had a panel and some months ago with the Mina folks and yeah this is what I was telling like guys you know you were the original ones to propose this and I think this is going to be the future for a long amount of time um we we'll see how people call it but now it's incrementally verifiable

computation right and what technically what we have is an incrementally verifiable Ser knowledge virtual machine cool yeah uh I I would say that another uh topic is it's just like will this proves that we compute for ethereum like convince someone a year into the future or two years into the future we we would want this proofs to be fairly simple like mathematically speaking that it could convince anyone for example like when you say oh I used this random proof system it's like the proof system could be sound etc etc but it's like how do you convince other people that this is correct right such as we had discussed before we believe that a system that

uses like very simple mathematical Primitives it's very simple to understand from a mathematical perspective maybe it's not as efficient but it's simple leads to many advantages in terms of like human synchronization right a lot of ethereum is about synchronizing people right um uh we believe that something like that is important in terms of like standards so to say not standards but more like universally accepted standards for what a proof is and so this is important for the point that I was going to make before about liveness right so like if for some reason there's a company right that is Computing a lot of proofs but then they die or whatever hopefully the proofs are number one easy to understand easy to produce and then anyone can

continue producing those proof so just as just as people are Computing blocks and there there's like block proposers and all of that uh the same right people would compute make proofs and they would propose a proof the proof would get accepted and there's a way to decide on approve this is this is a different topic of conversation that I am particularly very passionate about which is sort of like the future of ethereum like ethereum wasn't designed for Zer doll proving yeah right so what will happen in the next five years of ethereum well we'll see but ethereum is certainly very like here and there very CK unfriendly I would say on the side of

proving and on the side of verific y so well we'll see I'm very optimistic that you know uh the ethereum foundation folks will make changes yeah it's funny because I was I was going to ask you if you if you are solely in the ethereum world or if like as a ZK VM you could be on any chain so yeah have you ever thought of deploying elsewhere that's more ZK friendly this so it's so uh what is the word it's heresy to suggest such a thing I realize but yeah no no no so I I really like ethereum like personally I've been following the ethereum prob since like 2017 but it has huge limitation that for

example it only supports pre-c compiles for BN 254 uh operations and pairings right um and this has been a problem since like two years ago so I asked my advisor Dan Bonet back then when I was s for like hey Dan is this ever going to get resolved and he actually asked vitalic and vitalic just said like probably not anytime soon we're focus on the merge and all of that and so it has been the same for years for example we would want pre- compiles for BLS 12381 so that we could do BLS verification of ethereum U of BLS signatures but that just hasn't been enabled there's been an EIP that has not been enabled we would want other

pre compiles to be able to do other uh different things this would massively simpli fire or proof compression process because for now we're bounded to essentially have a system that makes the proofs compatible with BN to 54 which is not nice yeah yeah yeah I know I've heard this from lots of teams that have worked with the ethereum stack exactly exactly other blockchains um they have their problems as well just because sometimes they just don't have b254 break compile it's just with like worst so you have to deploy a full Ros verifier uh but sometimes those blockchains just happen to be so cheap that maybe doing that is fine there were recently uh some Innovations on the side of Bitcoin and Dogecoin to True right

you saw that right to add an up code for a Groth 16 verifier right and all of those Innovations on the um execution environment is is good so answering your question our system like even though I like in my heart ethereum occupies a special place our system is fully general purpose or verifier can be deployed like anywhere and we in in fact one of the core goals of the Nexus project so to say is to what we call democratize ethereum's execution environment and by that I mean to allow developers to have rollups or other execution environments they're just distinct through the use of promiles and other virtual machine

architectures for example this limitation that we've had on precompile on the evm would be solved if the evm was a CK evm built with the Nexus ckvm oh so you would almost like triple like you'd put yourself on the third level or something no what I mean sorry what I mean is that people have not been able to develop their own pre compiles to the evm and then merge them into the theorem protocol so maybe they have to move it to the L2 exactly like Innovation will probably be faster in an L2 where you can enable new PR compiles because you know you don't have to wait for the ethereum foundation to pass something yeah uh so Innovation will likely improve on that side by just allowing

people to write their own pre pass cool I wanted to add to to what Daniel described for like the blockchain space right so both ethereum but also potentially other chains right I think we should also think beyond the blockchain space right so so our goal is to enable verifiable computation to be everywhere right so if you made verifi ability really cheap right so it was almost at the cost of computing right then you could spread verifiability everywhere right so you could imagine the internet and all the data s like floating around the internet were came with proofs right so so it was all based on verifiable information rather than

just whatever you believe that that the other computers is giving you right yeah um so so I think the end goal right and that's probably going to be many years into the future right is really that you sort like increase the trustworthiness of everything through verifiable computation yeah actually yes there's a few other um like there's Pluto who's doing sort of like the TLs web proof thing there's a few teams they're more they're kind of like we've been describing them closer they're not quite like hardcore they're infrastructure but they're a bit higher up the stack towards like the use case and I do think like Mina in a way going back to Mina I think they also had that vision of being able to prove some like the internet

which is a much bigger picture so I like that you're also thinking about that because I think there's something important like that we do think past blockchain stuff I think interaction the intersection between ZK and blockchain has been epic for the acceleration of ZK it's it's been the funding I think it's also brought a lot to blockchain but yeah I I love the idea that it it sort of even transcends that I mean I think there's a lot of things happening in the application space because what people are doing they're going out and finding these trust angles right you you need to sort like prove something about something yeah exactly right and you have people that are going out and sort like stripping out passport data using

the TLs connection or so like Google account or some information so forth right and proving things about that and it's interesting because this is exactly something that they can do because we have improved the efficiency of zero knowledge proofs right if you tried to do that 10 years ago you would just fail because you couldn't do it you didn't have the performance to do it right but now we have the performance to do it and even that they can take general purpose proofs right and throw them add it right so it's much faster Innovation and prototyping right you don't need to sort like handcraft a proof system that is efficient enough for this application but you can just go out and take a

general purpose and I think it's sort like very interesting sort like what the application space and and the matching Ser knowledge techniques are going to look like right I think we really seeing very rapid improvements in performance right which is going to unlock a lot of things pretty much everybody in our team we are primarily excited about the real world applications of CK and to bring it into industry right that's actually goes back to our initial conversation about verifiable cloud computing right we care about making it like very very professional High degrees of observability sort of like an what you can consider like an elastic Cloud that is highly available highly optimized

very professional that just computes proofs in connection with you know ecosystem partners and so on and so forth which is where the network sort of like discussion comes into the future but bringing verifiable computation to full generality to the internet is our primary goal as a company cool well thank you Daniel thank yens for coming on the show and sharing with us all these things I mean we covered for formal verification Audits and and security all the way to sort of the Nexus system and this verifiable compute what that actually means this the largest verifiable computation that's cool thanks for coming on yeah thank you Anna yeah thanks Anna a pleasure as always all right I want to say thank you to the podcast team Rachel Henrik and

Tanya and to our listeners thanks for listening