Episode 406 - Alex Ozdemir on where Theorem Provers and ZK meet

Transcript

Welcome to Zero Knowledge. I'm your host, Anna Rose. In this podcast, [music] we will be exploring the latest in zero knowledge research and the decentralized web, as well as new paradigms that promise to [music] change the way we interact and transact online. This week, Nico and I catch up with Alex Ozdemir, assistant professor at Georgia Tech, for a discussion about formal verification and theorem proving, specifically in ZK.

We start with a recap of the changing ZK DSL landscape since 2021, the topic he was covering last time we had him on, and how Circom, his compiler infrastructure project, has evolved to support more expressive and efficient ZK proof systems. We then dive into formal verification and theorem proving, discussing the difference between SMT solvers and interactive theorem provers like Lean, how ZK proofs can be used to verify Lean proofs without revealing the underlying code, and the new system ZK-P, a ZK-SNARK for proofs expressed in Lean, allowing a prover to convince a verifier that a Lean theorem is true without revealing the proof itself. We also explore formal verification, the threat

of security theater, and how building verifiably correct systems will be ever more important moving forward. Hope you enjoy. Now, here is our episode with Alex Ozdemir. >> [music] >> Today, Nico and I are here with Alex Ozdemir, professor at Georgia Tech. Hi, Alex. Welcome back to the show. >> Hi, Anna. Good to see you again. Hi, Nico. Nice to meet you, I think for the first time. >> Oh. >> Yeah, great to meet you. Hi, both. Nice to be here. >> Alex, I'm excited to catch up. A little bit of backstory, a few years ago on the show, I did a series on ZK DSLs. You at the same time were doing a lot of kind of work researching all of these ZK DSLs and so we had you on then. I think we

also did a ZK sessions with you a study club like there's a bunch of content that we'll link to but this is actually a few years ago. This is 2021 that we were doing that. I'm very excited to catch up on all of your research that you've been working on but I think maybe a starting point could be those languages. What's happened sort of in the language space for ZK since we last spoke and also let's talk about Circom which was kind of what you were presenting back then. >> Yeah, so I think there's two things to to discuss here. First, what has happened to languages in general >> Okay.

>> and then where does Circom fit into that? And so you know let's start with languages in general. There basically been two parallel and complementary threads of research that have been going on. One is that circuit DSLs have people have continued to build new ones. They've started to explore new computational models for them. Like you know, what is this thing that we're building? Is it really a circuit or is it like a variation of a circuit? Maybe it's a little bit different. And and then also just like can we get these the compilers for these DSLs to be better better user experience. All that has continued and Circom is very much part of that that trend and I I can say later what exactly we've done in Circom to contribute to that.

Simultaneously, there's been a lot of attention on building ZK VMs which are also a language tool for building zero knowledge proofs. They live typically on top of the circuit level. So the implementation of the VM is a circuit and some other things but then people can program on top of that. And that's also been very exciting and the ZK VMs have been getting better and better. And you know, the reason of course that the ZK VMs are really important is because in some sense they make the circuit DSLs and the circuits like an implementation detail rather than an interface that a ZK application developer needs to know about. So So I think that was a little bit unclear, so to put it more clearly,

um with a ZK VM, the application developer doesn't need to know about circuits. The VM developer knows about circuits. The application developer just knows about the VM. >> Those ZK DSLs, you mentioned that there's new ones. Back then, we would have listed Arcworks. I think Noir was already out in 2021. Cairo. What else has happened since then? Maybe I'm missing some from there, too. But yeah, can you share like what are the What are the new ZK DSLs? >> Yeah, so Noir has continued to see a lot of effort go into its compiler. So back when we talked before, the compiler was kind of a a stub that did very little.

And now it's it's certainly by lines of code the biggest of the compilers. Um they put a lot of effort into it. So one another new one is called Clean, like uh cleaning your room. >> Hm. >> And uh this is a DSL a ZK DSL that aims to be verification first. So the goal is not only yeah, to be succinct. >> maybe? Is that what it's standing for? Hey. >> Exactly. This is from ZK [clears throat] Security, by the way. Like that's from my colleague uh Gregor. And a lot of the team, of course. >> Exactly. Exactly. So this So here the goal is okay, we don't just want to describe a ZK circuit, but we also want to verify that that circuit matches our intentions. And we think that a co-design process between the DSL and

the verification tool chain will help. And so that's what what Clean represents. Um so that's another exciting one. It It already sort of existed in in very informal and weird ways in in 2021, but there wasn't much language tooling around it. Was this this idea of building DSLs not for for circuits, but for randomized circuits or for circuits that model interactive proof systems. So this is like you know, we have to to discuss this will take a little bit more time, but to put it simply, you know, what if your circuit, in addition to doing computations and enforcing constraints, could also flip coins? And then you know, you want your circuit to only accept if the property holds. So, if the property doesn't hold, it's okay if the circuit accepts with some very

small probability over these these random coins that you flip. So, this existed in Halo 2, which which existed in 2021. >> Mhm. >> But, there wasn't much like it existed in the proof system support for that, but there wasn't much tooling. And so, that's been something that that people have been exploring in different ways. Like, how does the circuit DSL allow the programmer to use this randomness in their circuit? Um and so, there's been a lot of work on on the language tooling for that, but also then using that to build better ZK applications, getting proving times to be faster for important kinds of properties. >> Nice.

>> In some way, this is something we're already doing with lookups and like permutation arguments, right? These are interactive circuits in a way. >> Exactly. Yeah, yeah. So, these lookups, so you can implement the lookup arguments using these random coins. So, in some sense, random coins subsume the stuff that you can do with lookups. And so, that's like one way that you can do lookups is like you can have support for random coins. But then, another option is say, "Actually, you know, really I don't know if I want random coins in general. I just want lookups." So, then you can bake lookups specifically into the DSL and then random coins become an implementation detail. Although, I would really advocate putting random coins in the language cuz there are lots of cool things that you can do with them.

>> What are these coins that you just described? When you say flip coins, I'm not sure if I know like that isn't really the language we were using back then. What does that mean? >> Yeah, so that particular phrasing really comes out of complexity, where like everything complexity theory, where everything is a bit. And so, if you want randomness, you you flip a coin, heads or tails, and that sets the bit. Uh actually, typically in these circuits, we're working over a finite field. So, really you just sample a uniformly random finite field element. >> Okay. But, are you getting a one and a or zero? Is this or like you're getting one of two options? Like a bit?

>> So, you you'd probably be getting a random element from a finite field. So, like one of 32 to 32 options approximately or 2 to the 26 options. Yeah. >> In our sort of interactive proof IOP language, this is getting a verifier challenge. >> Correct or what do you mean? >> As in you as a prover will do some things. And once you've done that, you can ask for a challenge from the verifier. And using that challenge, you can do more things. So, I'll commit to my tables, I'll get a challenge, and then I'll do a lookup. >> Ah. So, it's like sequential based on certain requests.

>> Exactly. And that phrasing is like perfect because, you know, when when we introduce this informally, we say, "Oh, your circuit has random challenges. So, it's a randomized circuit." But, that's not really right because there's this this question about ordering. >> Mhm. >> Um the prover can put in values to the circuit, and you can flip coins, you can you can sample challenges. And you can actually alternate. So, what's really going on here from a theoretical perspective is that this this circuit is now defining an interactive proof system that's public coin. And then the what what happens behind the scenes is that the generic SNARK turns your interactive proof system into a SNARK for the same property.

>> I do realize that I So, you just mentioned, just going back a little bit, you mentioned Halo 2 was a proving system at the time and now kind of has more of a characteristic of a language. I actually was going to ask you about that, too, because all of these teams we knew were doing these workshops on Halo 2. Using Halo 2 sounded like a DSL. But, it's yeah. What what is that actually? Was there other languages involved in Halo 2 or was it actually its own thing? >> Yeah, so this is sort of the classic story in in ZK tooling research, which is that you come up with some cool new proof system that has a cool new capability.

>> Uh-huh. And then you have to make a language that can interface with that, I guess. >> Exactly. [laughter] Exactly. This was the case for libsnark back in the day during the first implementation of Zcash. So, they had the proof system, and then they also had the gadget library. I think they sometimes called the gadget library gadget lib, but sometimes they just called it libsnark as well. >> Mhm. >> So, you know, tool, language, and then again with with Bellman, when they did the Sapling implementation of Zcash, they had Bellman was an implementation of a proof system proof system, but also a gadget library on top of it. So, the language, and then and then this happens again with Halo 2. So, you've got the proof system, you've got the something like a gadget library.

>> And to that you add the joys of open-source development, which means all these teams did different forks of it, different parts of Halo 2, different commitment schemes, etc. So, yeah, it's a chimera with many heads, and God knows what is Halo 2, but thank God for Halo 2. >> [laughter] >> Yeah. >> Wow. We forgot to actually mention one of the OG languages that was used a lot, Circom. Mhm. What's happened with Circom? Do people still use it? Has it has Noir kind of like taken its mantle? >> Circom is still used.

>> Okay. >> Circom is still used, and I I think just by like in terms of like sheer number of projects, it's still the majority. >> Oh, wow. >> And people still write new projects in Circom. I think as a percentage, it's market share is declining a bit just because other languages are also succeeding, and they're adding new projects faster, but but Circom actually frankly is better than ever. They re-implemented their whole compiler tool chain in Rust. They have lots of verification infrastructure for Circom now, and like the Zisk ZKVM. >> Yeah. >> So, this is like a V a VM. Like, it would be totally reasonable for them to not use um a circuit language at all, and just try to like write the constraints themselves, but they don't.

They actually use Circom, and that works very well for them. >> Interesting. It's funny, I actually had ZKVMs as like the final question to this section. You've already brought it up. This idea that like don't ZKVMs kind of make all of this unnecessary? Where are they still being used? Are they necessary? Like, does the ZKVM mean that like developer mindshare application developers are all going to be using standard like standard languages like Rust or whatever is in the ZK-VM or are there still people who feel the need to kind of go into these tools and build yeah with the ZK DSL itself?

>> Yeah, circuits circuits are not going to go away. So, you know, the ZK the advent of ZK-VMs just means that the situation is going to be more complicated and developers are going to have more choices. And so, you know, to think about why circuits won't go away, there's two reasons. One, the VMs are implemented using circuits. So, the people who implement the VMs are still going to need to know this. And [snorts] then the other reason is that the VM imposes significant performance costs in terms of proving time. Because essentially you know, you have your application and instead of getting, you know, the best possible circuit for your application, you are shepherding your application into some instruction set architecture like RISC-V and then you're doing a generic proof about RISC-V. And

this this like level of indirection just ends up being expensive, especially because instruction set architectures like RISC-V were not designed to be efficient for zero-knowledge proofs, they were designed to be efficient for processors. So, that, you know, the abstraction is kind of wrong. So, you know, what this means is that I think we're going to enter a world where for an application developer the easiest approach from an engineering perspective is going to be to use a VM. >> Mhm. >> And if that meets your requirements needs, great. You're you know, you're done right? >> Mhm. >> Under the hood, there are some circuits used in the implementation, but you don't care about that. Of course, sometimes that's not going to meet your performance needs. And so, to give, you know, a reference point, very recently Google put out this library for doing anonymous credentials using ZK. The

library is called Longfellow. Uh Longfellow is definitely not using any ZK-VM. >> Okay. >> their own their their own circuits, yeah. >> I actually wondered another example maybe was like a project like Layer because I think they're a bespoke ZK-VM or ZK-EVM or not even, they're a roll-up or something. They're but they seem to have developed their own circuit. We actually had them on last year. >> Yeah, yeah, exactly. So they're if I remember quite correctly, they're basically operating an order book. So they're operating a marketplace. And yeah, they have like a bespoke circuit slash VM situation that's very good for implementing an order book and order book matching. I actually talked to them. And I actually I think all this randomness stuff that we were mentioning is is quite useful for them already. It could probably be even more useful.

>> And that's written in Plonky2 if I'm not mistaken, which is another one that we can add to the list. >> Oh, wow. >> Yes. >> Have we forgotten any? >> [laughter] >> Probably. >> Probably. We didn't I mean Cairo has it evolved at all? >> A lot. Yeah, absolutely. >> I'm not up to date. Yeah. >> Cairo went from being a a Python-like language to a very Rust-like language. And it's an interesting one cuz it's a DSL, but it sits on top of a VM, right? It's actually like the instructions for the Cairo VM. Hm. So it's a slightly different thing. It's these like, you know, custom VMs that have these custom languages.

>> I want to now talk about Circom and how that has developed. Can you remind us what Circom was and what it has become? What is it? >> Yeah, so Circom um is a compiler infrastructure. So what does that mean? It's it's not a compiler. So it it doesn't have one source language and one target language that it's translating between. Rather really it's a library for building compilers. So it's a common intermediate representation with transformations over that. And instead of having one source language, there are multiple. And instead of having one target, like one particular ZK-Snark or more even just ZK-Snarks in general, it has multiple targets that it has in mind. And the idea is to try to to to

share compiler logic between different source-target pairs. And to to give you a sense, the targets that Circom originally supported included not just the ZK-Snarks. I think specifically we were hooking into Bellman at the time, but but I guess you should think of that as R1CS in general. >> Mhm. >> But also we are compiling to multi-party computation protocols and we are compiling to SMT logical formulas in order to do verification on the programs that were being compiled. We were compiling to integer linear programming constraints in order to solve optimization problems. And then probably after we talked we went on to compile to different homomorphic encryption schemes as well.

>> Interesting. I was going to ask you if it did sort of like branched out past the ZK cuz it sounds like it. Why why not? >> Yeah. Yeah. Personally the ZK target continues to be the one that's closest to my heart just because out of all these cryptographic technologies the ZK seems to be having the most impact right now. Um and and needs tooling the most for that reason. But but it does do these other things and we continue to do research on how to how to do those other things well. So we we've done lots of research into optimizing compilation for FHE and MPC. >> Cool. I feel like IO is probably too far off but like have you have you I mean is there a language for IO? I feel like I'm I'm getting ahead of myself here but yeah have you even like looked at that?

>> Um so it's not something that I've looked at and I don't think other people have looked at this from a language level although there's a lot of excitement right now on basically taking IO constructions. So not not the compilation problem but the crypto system itself from from theory to practice. So traditionally this is IO is something that the theoretical cryptographers worked on and you know they they don't even really know like how long things take so they can't make things efficient. And so there's some some attention on trying to get more practical constructions. Once that happens then we'll need language level tooling as well.

>> Got it. What is new with Circom though? Cuz I feel like I've seen I don't know if it was a research paper of yours like from just like last year or two years ago. So yeah I'm curious what what was in there? >> Yeah. So Circom has been making a lot of progress on two fronts. One front is functionality like kinds of things that we can compile. And the other front is correctness. How do we know that Circom is correct? As a compiler. And the the functionality point actually relates to something that we were discussing a few minutes ago, which is this idea of in-circuit randomness. So, over a sequence of projects where we were using Circom to do various things, we wanted to use in-circuit randomness

like like everyone else, and we started to ask like, what does it mean to have an automatic compiler that is automatically optimizing how you use randomness? >> Mhm. >> Inside your circuit. And so that's something that that we've been doing in Circom now for about 2 years. And to my knowledge, we're we're like in some sense, the only game in town for this. So, there are lots of languages that will let you use randomness, but Circom is the only compiler that will take how you use randomness and then change it and optimize it. >> What do you mean here? So, let's dig in a little bit. So, it's not that it generates randomness. You already have randomness. How do you use it differently?

>> So, it'll kind of do both things. So, so first of all, maybe your program, your original circuit program, is is actually deterministic. So, it's doing deterministic operations. Maybe it builds an array, it puts some stuff in the array, it gets stuff out of the array. So, Circom will actually come in and look at your deterministic operations, and if if it knows how to, it will replace those deterministic operations with optimized randomized versions. So, it'll like plug in the interactive protocol that does a lookup argument or does a memory argument. And it knows like four different memory arguments, and it will choose the optimal one based off of the size of your memory and the number of accesses.

Maybe you're multiplying matrices, it'll plug in randomized tests of matrix multiplication instead. It will rearrange your lookup tables and like range checks. So, it'll add randomness even if you're not using it already. >> Oh, cool. >> But then, the second thing is once it's added all this randomness, or once it's looked at the randomness that you've added yourself, it will try to use that randomness better. And and what do we mean by that? Maybe you you know, in your program you've got a thousand challenges. But maybe just 10 will do because maybe some of it some different components of your program can actually share challenges. Circe will reason about that. Maybe you know, you get some challenges and then the prover commits to some more stuff and you get some more challenges. And and you know, there

actually many rounds of challenges. Circe will try to figure out if some of those rounds can actually be combined. Sometimes they can, sometimes they can't. So it'll rearrange the implicit interaction structure of these challenges. So this this stuff is all like very new and like we don't totally know the limits of what kinds of optimizations are sound. Um but that's something that we've been exploring in Circe. How how can you optimize not circuits but optimize interactive proofs? >> And I guess this is where proving correctness becomes even more important, right? >> Yeah, yeah. And that's that's the other thing that we've been working on which is how do we know that Circe is correct?

Um and so we started asking that question basically from the very beginning. >> And this you're talking about like that the compiler has acted the way it's supposed to? Or is it like it are you are we talking a little bit like in the direction of formal verification or and actually a question here like are you proving at the end of it that it's acted correctly or you trying to prove beforehand that this is going to act correctly? >> Yeah, both of those approaches So let's let's break that down. So yeah, this is formal verification. That's the goal. The compiler is a piece of software.

There is some specification often implicit of what it should do. We want to know that it's doing that. And for compilers when you verify them, there are two dominant approaches. One approach is I think what you were referring to as verifying before. And what this means is verifying that the compiler as a piece of software is correct. For any program that you give it, it will compile it correctly. There's also verifying after which we often call translation validation. And this in this approach you don't verify the compiler once and for all, but you modify the compiler. You instrument it so that as it compiles, it also creates a program-specific proof that it compiled the particular program that you gave it correctly.

>> Mhm. >> So if the compiler succeeds in an execution, it will output not only target code, but it will also output a proof in some language that that target code matched your original program. >> Mhm. >> So that's the latter approach, which is translation validation. >> Okay. I wanted to just do a quick throwback to a recent episode, actually I think it was our last or yeah, two episodes ago, where we had Benedict on and we were talking about ZK and how because of the structure of a ZK proof, if the [snorts] verifier accepts a proof, it kind of like you don't have to do as much verification to how the proof was generated.

I mean, I maybe I'm being a little vague on the on this explanation, but in the case of a compiler, are you [snorts] in like the like the translation validation you just talked about, can you do something similar where it's like if the output is correct and accepted, then you know that the input worked well enough? Or in the case of compilers, is it more complicated and you actually need to test in different ways? I'm making a bit of a funny comparison here, I realize, cuz I'm talking about a proof system and a language and engineering question, but yeah.

>> Yeah, that's a really good question. I So I think the natural like formalization of this question is saying, okay, the compiler has some input source and an output target. When we do translation validation, when we output a proof that the target is correct, is that proof a proof of a stand-alone theorem about the target, that the target is correct on its own? We don't even really care what the source was. >> Yeah. >> Or are we instead proving that the target matches the source? >> Mhm. >> Right? So, if we're proving that the target matches the source, then of course the source also has to be correct.

>> Yeah, yeah, yeah. >> You know, it has to be a correct implementation of some predicate that's relevant to your application. Uh basically across the board Well, actually people do a little bit of both of these, to be frank. But the more common approach is to verify that the target matches the source. And And the reason is if you wanted to prove that the target is correct on its own, like what does that really mean? Like Like really it's more about like you want to know that the target matches the intent of the application. >> Mhm. You're trying to understand that this like from point A to point B, whatever happened in the middle happened the way you expected it to. And you're not just trying to get point B to land on something.

>> Exactly. Yeah, yeah, yeah. So, for sure you want to link application to target. And it's just not really clear how to get compilers to do that very well, cuz compilers are designed to understand the source code, not the application. >> Mhm. >> So, it sort of makes more sense typically to go source So, application to source code. Those two things are supposed to correspond to each other, and then source code to target. >> Got it. >> Yeah. >> By the way, I'll plug a recent blog post by my colleague Uchi that talks about this and saying, "Let's just verify the target against the application. And on the way to the target, let's not even have compilers that we trust. We can have, you know, LLMs go crazy, write assembly code if they want.

And then we go and verify that code against our spec of what we want the application to do." >> Mhm. >> That's a very interesting and fun way to think about it. >> When you talk about formal verification in the Cerci context, what kind of work are you doing? Are you doing both of those approaches? Are you focused on this formal verification and spec and and like building it from that point perfectly always? Are you taking chances? >> [laughter] >> So, what we did with Cerci is actually it's it's quite specific. So, we looked at So, we actually did the verify before. Verify the compiler once once all, but we did this only for for one pass in the compiler, specifically the pass that massages everything into finite field elements. So, this this

type mapping. We did that because those passes are often incorrect. So, we thought there would be bugs, and indeed we found a few before we were able to verify that that pass. But but also because basically our belief was when we started this project, this was back in Oh my god, like 20 21 2022. Whatever kind of verification you're doing, you need like underlying tools for like SMT solvers for for reasoning about the correctness about verification in general, and those tools didn't exist. So, it's sort of like whatever path you choose at a verification level, you're going to need to build those tools, and those tools will probably be useful for many different kinds of verification. Yeah, so so we did the verify once and for all, but like in some sense really this the goal was to build out the basic foundational

infrastructure to enable all of this. >> Cool. Do you have to do for every So, cuz you mentioned the different types of languages, tools, like you're compiling, you're moving from one thing to another. You also mentioned MPC, and that you were doing some homomorphic encryption. I'm just kind of wondering here is like do you have to re formal verify each one of those things? Is there like a overarching commonality between all of these that you can just do once? I'm just trying to figure out the effort needed here to spec everything first.

>> Yeah, so this is like another appeal of the compiler infrastructure approach, which is you know, the infrastructure is in some sense a bag of transformations, and every particular compiler will use some subset. >> Oh. >> And if you verify one of those transformations, and it's useful for multiple compilers, then they both they both benefit. >> Oh, cool. >> But also every every compiler probably does have, you know, some special transformation that's just specific to that compiler, so you'll have to verify that. And and for what it's worth, this this first verification project we did in CirC was for this finite field encoding pass, which is very specific to ZK. So, that's that's a pass that we probably would not re- we would reuse it for different kinds of zero-knowledge proofs, but we

wouldn't reuse it for, say, multi-party computation. >> I did not realize that that is how like compilers work or Circom works. I don't know if all compilers work this way where it's this bag of transformations and you choose depending on the system. Are most compilers more like historically, were they more specific, like single line from this to this? >> Historically, yeah. Yeah. >> Okay. >> But but certainly now, yeah, basically every big compiler is more of a bag of transformations because even if even if, you know, you say, "Oh, I just have a compiler, it's not a compiler infrastructure."

Like, yeah, but you probably want to run on ARM and also x86. So, you know, really everybody does have multiple targets in mind. Sometimes they really only have one source, but but almost everybody has multiple targets in mind. >> So, now let's dive into what it what you have to do to actually formally verify, like these individual transformations in the bag of transformations. I'm curious what this like work even looks like. >> Yeah, so usually the first task So, in verification, there are always two tasks. One, you actually have to specify. You have to say So, verification means showing that my code does what it's supposed to do.

First, you have to know what it's supposed to do. And this actually is quite hard. So, in the case of the compiler, usually that means saying very specifically what the semantics, what the meaning of an input program is in general, like what what the input programming language is, and then also saying what the output programming language is, and saying what it means for those two things to match. So, that's step one. And then step two is you have to prove that your compiler's code is is meeting that specification. So, for any input program, it will output an output program that matches the input.

>> Mhm. >> Specification, verification, those are like the two the two phases. >> So, you mentioned the SMT solvers, where do they come into play in this pipeline that you're describing? >> The second the second phase. >> Yeah. >> The verification. >> Yes. >> Mhm. Let's define SMT. We did talk about it on the show. I honestly I'm still a little confused about what it actually is. It's What does it stand for again? It's like uh >> [gasps] >> an odd collection of words that don't tell me very much. What does it stand for?

>> I'll tell you what it stands for, but also I'll say what I think it should stand for. >> Okay. Okay. >> [laughter] >> So, it stands for satisfiability modulo theories. >> Guys. >> [laughter] >> This is why like it kind I kind of blank on it as well. I'm like, but I don't know Is it like a list of directives? Is it a Is it a tool? Is it a library? Is it a Is it a program? Like I'm so lost what this >> [laughter] >> Is it like a concept? >> Yeah.

>> So, so yeah, an SMT is really two things. It's a tool and it's also an interface to the tool. The tool tells you whether a mathematical theorem expressed as a formula is true or false. Is it a tautology or or is not. >> Okay. >> So, is this formula true for all inputs? And so, you know, for example, a formula might be might express the fact that when I feed when I execute my program, it doesn't segfault. It doesn't crash. Is that true for every input to the program or not? So, the SMT solver is the tool that answers this question.

And SMT is also in some sense like a language for formulas that you would input into the solver. And sometimes people will refer to the language as SMT lib, SMT library, which is just a specification essentially for how you write down formulas. >> Now, what do you think it should be called? >> Yeah, I think it should be called satisfy ability modulo types. >> Oh. So replacing theories with types? >> Yes. Yes. >> Okay. >> And I I am here to tell you that, you know, theories is like arcane logic speak for for different mathematical types.

>> This breakdown of SMT as a solver tool and SMT a language, does that same breakdown exist for Lean? Like I kind of want to compare them maybe here just to understand what is Lean. Because is Lean like a program or tool or a language? >> I think this whole like interface tool distinction can be made for like almost any piece of software to some extent. >> Okay. >> But I think it's a lot less useful for Lean. And and I'll I'll I'll say the reason too. SMT solvers and SMT is about automatic theorem proving. You write down your formula, the tool automatically proves it. Lean is an interactive theorem proving tool, an ITP as opposed to an ATP, automatic theorem prover.

>> Okay. >> And when you're doing interactive theorem proving, you don't need a strong a separation between the tool and the language that you use to talk to it. It makes a lot more sense to conflate these two. Like so so for example, like we it's we have like one Lean proof checker. When you look at the kernel, there's a few different implementations, but for the most part there there's one piece of of software that's the Lean tool chain. >> Is this something you built or just generally there is only one piece of software that is the Lean tool chain? >> Yeah, there's one and it's maintained by I guess now the Lean FRL.

>> Okay, like that okay, that is what Lean exists as. Okay. >> Yes. But for SMT solvers, there's a common interface and there's like 10, 12, there's lots and lots of different solvers that all meet the same interface and you can choose the one that's performing best for your the theorems that you want to prove. So you know, the the fact that the in the case of SMT, the interface actually allows you to multiplex between different solver implementations. That means that thinking about the distinction between the solver and the interface is much more useful because there are actually many solvers. Um and in the case of Lean, that's less true.

Now now of course interaction, you know, and and automation both are valuable and so both SMT SMT allows some kind of interaction and Lean allows many kind of automation. So in some sense the two approaches do meet in the middle, but they start from opposite sides. >> Mhm. Last year we had an episode on a project called Acorn, which is a theorem prover utilizing AI. And that was where like for me I was introduced kind to Lean for the first time. I it was not a world I had been part of. But in in that episode we were kind of comparing this system to Lean. So I you know, I've still been a little bit unclear on how to actually use Lean.

But I do want to sort of bring in just also this AI part because last year Acorn was doing something different from these SMT or Lean things in using AI. I have a few questions actually after what I just said. A, what is the category of Lean and SMT? And B, are they actually using AI now? >> Yeah, great. Yeah, so SMT and Lean are both theorem proving technologies. So that's the category. >> Yeah. >> SMT being the automatic theorem proving and and Lean being the interactive theorem proving. And you know, the goals are different. On the on the ATP side, you want automatic proofs. You get big solvers, huge pieces of the software that are doing the automation. On the Lean side, you're okay with we'll say

manual proofs, although they try to they try to automate as well. And what you want is like a tiny trusted code base that's checking those proofs. So you can have real certainty when you say that a theorem is true, it's true. So that's that's what they are. So theorem provers. >> Yep. >> Yeah, and do they use AI? So actually SMT solvers like I mean traditionally they were considered AI research, not statistical, not machine learning, but they they were AI like they were AI research and then they still are. Now, they're even using some statistics internally. Although, I think that you should think of them as as fundamentally not based on statistics. Fundamentally much more based on search and and logic.

>> What would you mean by that? In terms of statistics, are you talking like statistical probabilities? So, like it would be like this is most likely true, but not entirely true. Is that sort of what you mean by statistics? >> Yeah. Yeah, I guess statistics statistics is in some sense like what gives you a machine learning, right? So, So, I mean machine learning is the approach to AI where, you know, we don't know how something works. You know, we want we want we want to be able to solve a problem, but we don't really know the underlying dynamics. And instead, we're going to define a statistical model. We're going to look at a lot of data, and we're going to fit our model to the data, and then we're going to use that to approximate the system that we're trying to solve. And that having this

model Yeah, good. So, so that's kind of what I mean by statistics. Like we're fitting a model to the data. And if you take like a machine learning class, this will be like the first lecture. This view of like, okay, you've got something in the world that gives you data. You're going to define a model. You're going to fit the model to the data. >> Mhm. And it won't 100% nail it every time, but you're going to get a threshold where you're happy enough with this result. >> Yes. >> But now go back to like sort of theorem proving. And you say it's using some statistics. Does that mean like we're like 95% certain this is correct? >> So, the theorem provers never give up on correctness. They always insist when they output true, that thing needs to be true 100%.

>> Okay. >> But in order to say that something is true, they have to find a proof. And that's like a search problem. You have to figure out how to prove it. And they're okay with using statistics and potentially machine learning to guide the search for the proof. >> Oh, I see. Okay. To find it. >> Yes. >> I've been also trying to figure out like where they getting where they like they these theorem provers, where are they getting all of this information? Do they have like a big database? Do they have access to all mathematical information online ever? Like I'm kind of trying to understand where it could even draw these things from.

>> Yeah. Are you thinking about like in general, like if we're trying to do math and using a theorem prover, like how does the theorem prover know about math? Or you thinking more like if you're trying to do machine learning and you're trying to build an AI-based proof search? We're going to need Machine learning always needs data. It's like one of the axioms. Where did that data come from? >> No, it's the I think it's the first one actually. It's It's Maybe I'm thinking about it wrong, but I'm sort of thinking about this SMT as a tool that will like you're going to put something forward and it I'm assuming will like check what you've put forward against other things.

Where are those other things? >> I think you should think of this as different for SMT and Lean. >> Okay. >> So in Lean, Lean will provide a language that allows you to define math. So you can define what is a set. You can define what is a natural number. You can define real numbers as sets of integer Yeah, it's Yeah, that's a rationals I guess. Some human needs to like write down the mathematical definitions in the language and that's how Lean knows about like what the basic mathematical objects are. So some human does that translation. Yeah. And the idea of Lean is to express like lots of very sophisticated mathematical objects since the humans write very sophisticated definitions.

And the SMT world, it's a little bit different in that the goal is to automate proof search. So they express only simpler mathematical concepts. So Actually, we would express all the things that I just said, but like like cohomology or something. Like people define that in Lean. They don't define that in SMT. And so there's a someone at some point writes down different They call them theories. This is where this comes in. They define different mathematical types for SMT. And then the SMT solvers are built to search for proofs for theorems that involve those types. >> I see.

>> So in some sense, in both worlds, a human at some point writes writes this down. But in Lean, we imagine like continuously writing new definitions, teaching Lean about new mathematical objects. And we don't expect Lean to find proofs for us. In the SMT world, you would write definitions when you know a proof search procedure for them. So, you have a much smaller set of definitions, but you have very strong automation. >> So, you did say we don't expect Lean to find proofs for us, but this is, you know, sort of tying back to Acorn. I guess that's the idea there, right? Is like instead of having humans do Lean proofs, let's put an LLM and let it try to do the thing.

>> Hm. >> Yeah, exactly. So, so Lean, you know, the Lean software on its own, it doesn't promise to find proofs for you. It gives you a language for defining things and a language for checking proofs. And it also gives you a meta-programming language for expressing proof search procedures. >> Mhm. >> And then people come in on top, and they try to build those proof search procedures. And maybe that proof search procedure uses a language model, maybe it uses some kind of machine learning. People also spend a lot of time building proof search procedures that that don't use statistics or machine learning, but are just classical, but very effective. And this is the way, you know, I mentioned earlier that, you know, ITPs and ATPs have this gap, but really they both want to bridge the gap. This is the way that that Lean-based systems bridge

the gap is that people build proof search on top of Lean. >> Hm. >> Mhm. Uh so, if you hear about like tactics, that's when people talk about tactics, they're talking about proof search procedures in Lean. >> So, should we think of pure ITP, interactive theorem provers as actually like user theorem provers? Like, it's people doing the theorem proving. >> Yeah, maybe so. >> And then we have a whole spectrum all the way to fully automated. >> Yeah. And I mean, the people actually just bridge these things so as well. So, for example, people will have Lean tactics that create SMT formulas for something that you want to prove in Lean, and then they ship that formula over to the SMT solver.

>> Hm. >> Um and the SMT solver solves it, finds a proof, and then they'll ship the SMT proof back into Lean, and they'll like build a Lean acceptable, like they'll use the SMT solution to build a Lean acceptable proof. So, that now Lean is convinced. So, another way you bridge the gap is actually just interfacing the two tools, not just like conceptually trying to behave more like each other. >> So, I want to wind back a little bit to what we were saying about theorem proving. At one point you mentioned a few things that define theorem proving, SMT, Lean, and then you mentioned statistics. I sort of have gone down that rabbit hole, but let's like sort of wrap that up and bring it back to what else it is because I think it's it's definitely more than that.

>> Yeah, yeah. So, so yeah, so to sort of like recap, I guess now we have the right language for saying how machine learning and statistics fit into theorem proving. >> Mhm. >> You know, that the theorem provers, as we said, for them truth is absolute. They'll never tell you that a theorem is true if it's not. But, in order to to say that a theorem is true, they have to search for and find a proof of the theorem. And search is a really hard problem, and one of the tools that theorem provers use, both Lean-based tools and SMT-based tools, is they'll use statistical reasoning, machine learning, in order to try to do a better proof search. So, they'll learn, oh, you know, if a theorem looks like this, then this is the kind of proof that I should look for most of the time.

>> Nice. >> So, maybe at least this is a good time to ask you, I see you've been doing a lot of work in SMT solvers yourself. Can you tell us a bit more about what you've been up to? >> Yeah, of course. So, this relates to something that we were saying, which is, you know, in the context of an SMT solver, adding a new type, adding a new theory, adding a new domain of mathematical reasoning is kind of a big thing cuz you don't just need to define the type. So, let's say, you know, in the context of cryptography, finite fields are king. Basically, everything is a finite field. People talk about elliptic curves, they're finite fields. The theorem the finite fields, you know, elements, right? Okay.

So, so finite fields are are big deal. And if you want SMT to be useful about reasoning about finite fields, then you need to not only define what a finite field is, but also come up with a good proof search procedure for them. And so, that's that's what I was been working on for the last few years. So, writing down the definition of finite fields, which is very easy, but then coming up with proof search procedures for proving things about finite fields. And uh written a number of papers with different proof search procedures that you All these are motivated by Oh, we have some ZK system we want to verify. What's a good proof search procedure that allows us to to verify systems of that kind?

>> Is this for one specific SMT solver, or is this something that can plug into all solvers? Like how how does this work? How does this world look like? >> Yeah, so I mean I did my research in the context of an SMT solver called CVC5 that we built at Stanford. But what are the I think one of the best things about this research that I was doing is it got a lot of other people excited. So, CVC5 is no longer the only solver that's useful for reasoning about finite fields. So, there are some people in Vienna who built like sort of like a one-off solver just for finite fields that's very nice.

Uh Yices is another big SMT solver that supports lots of different types. It supports finite fields as well now. Recently, the Costa group in Spain built a bespoke solver for finite fields as well that's quite exciting. So, you know, this is what we mentioned earlier SMT is one interface many solvers. You know, CVC5 was the the first effective solver in this domain, but now there are lots which is really great. And the idea is that they're interoperable. >> Mhm. >> CVC5, is that you sort of mentioned if it's about reasoning about finite fields, can it be used then to prove like to verify the ZK systems as they're being built? Like is that one of the use cases, or is that the main use case?

>> That's That's why we did it. I I think that you could actually use it for verifying other kinds of cryptography as well that are field based. Um but we built it There was a real need for ZK and there weren't other approaches at the time. So, that's that's what we focused on. >> Cool. I want to go back you had sort of mentioned earlier this idea of like proving ZK systems or using ZK to prove systems. And so, yeah, I'm just sort of wondering like what you just described in CVC5, this is proving ZK systems. This is using this SMT to or like what do you call it an SMT like instance? No, what is an SMT >> solver >> solver? Okay.

To make sure that a ZK system is acting correctly, that it's formally verified. Do you also like when you're talking about adding ZK to proof systems, would you still is this still within the SMT world or is that something else? And I I don't want to step too far outside of the formal verification if we're not ready, but I'm just kind of curious if it's like is it part of a formal verification process to use ZK to proof systems? >> So, it depends on how the computer system is built and on who knows what and on whether like your computer system itself has some secrets or some intellectual property associated with it. But sometimes in the context of or we believe that that in the context of formal verification sometimes there will

be secrets. And so you'll want not just proofs of the correctness of the software, but you might also want privacy preserving proofs of the correctness of the software. >> Ah. What would that look like? Would that be like an algorithm that you're trying to protect? Like is it What is the IP in this context? Cuz it's not it's not the input, I'm assuming. It's like the construction or something. It's a piece of the construction, right? >> Yeah. Yeah, exactly. So, this is to to be clear, that this whole direction, the the kind of software that it has in mind is proprietary software. So, this is very different than open source.

>> Mhm. >> When open source works, it's great. Like I'm a huge fan of open source. All my work is open source, but like right now, we're using Riverside to to film this or to record this podcast. Uh and I'm not really Riverside specifically, but I would I would bet dollars to donuts that Riverside Riverside >> Not open source. No. Definitely not. Well, as far as I can tell. Yeah. >> And here I am running it on my iPad and I hope it's not stealing my secrets. I hope it's [snorts] not like wrecking my iPad. >> does have your access to your camera and audio and microphone. >> [laughter] >> Yeah.

>> Yeah, and I hope that that those uh multimedia streams are going to your engineer, to Henrik, and not to Riverside HQ. >> Yeah. Well, I mean it's sitting on their server for sure, but >> So so anyways, if if the software that you're trying to verify is proprietary, then that means that there are some secrets associated with it. And what I would love is for Riverside to be able to come to me and be like, "Hey Alex, here is the proof that our software is not doing bad things with your data." >> Yeah, yeah. >> And you know, that now you can be confident that that that your data is being protected. And you know, of course if they're willing to show me their source code and do formal verification, like standard formal verification will work if they can show me their source

code. But if they're not willing to do that, then perhaps zero-knowledge formal verification would suffice. >> Interesting. But here, how do you prove how do you prove it's not doing something bad? Can't it only just prove what it does? >> Yeah, that's a great question, and that's kind of like the question that launched this whole thing. So it's like people have been doing zero-knowledge proofs for a long time, and they always prove things like I run this program >> Yeah. >> and it gives you this thing, right? >> Yeah. >> Yeah, it tells you about an execution of the program, not all executions. So like what does it even mean to to write a proof that all executions >> Or the what's the other the it's like the opposite of do it's >> the non-execution.

>> Dan and I might have mentioned this. I don't know if it was on the air or in a conversation around this, which is like proving you didn't do something is really hard. >> It really is. Yeah, yeah. So in to answer the question of how to do that, we have to forget about ZK for a second and just think, okay, forget about privacy. How do I know that a program is buggy? How do I know that a program is correct? To know that a program is buggy, all I need is an input. I take the input, I run the program, bad thing happens, I can observe a bug, like the program crashes. Great. How do I know that a program is correct? Much harder. Uh you do formal verification. I write down, for example, a lean theorem that expresses the correctness of the program. For all inputs to this program,

it will never send your secret data to um the adversary servers. >> Mhm. >> And then I come up with a proof of that theorem. Uh well, perhaps a lean proof. So, that's what formal verification is all about. It's about proving things for all executions, for no execution, knowing knowing that the program is always safe. And so, you know, in some sense, like what we want to do is we want to be able to in zero-knowledge prove that this lean proof exists. >> Mhm. >> So, the idea is like if I'm running when I run Riverside, they're going to send me Riverside, like the binary, and they're also going to send me a theorem.

They're going to say this binary will never do X, Y, and Z. >> Wow. >> And I also want So, so, you know, we've got a theorem, and I want to know that the theorem is true. >> Yeah. >> And the question is how can they write a proof of the truth of that theorem without revealing secrets that they might want to protect, like how their software is designed? >> Mhm. So, it's almost like you write the software, maybe start with the spec actually, you write the spec of what it's supposed to do. Somehow, something extracts from that what it will do and what it won't do. Cuz what you're trying to understand is what it won't do, right? You're trying to make sure a guarantee that it won't do something malicious.

>> Yes. >> And then there's a proof made about that won't do feature. >> Yes. And let's say they do that in Lean, and Riverside does that. So, they've got the proof now, but I I don't have the proof. So, how they they want to convince me >> Yeah, and then you make it ZK. Got it. >> So, is it just a zero-knowledge proof of a Lean proof? >> Exactly. That's That's what we're trying to do. Zero-knowledge proofs of Lean theorems. >> Okay. I have a bit of a spicy question about formal verification. The way I've understood this is like you create a spec, and then you create the software, and then you prove that it's right. But software is big.

And like there's lots of softwares that work together. And is it possible, say you were malicious, and you still want to have this formal verification stuff, can you hide in formal verification? Like is there a line through that that could be like obfuscated, but still show some sort of formal verification that it acts the way it's supposed to act. I don't know if this is like maybe there's no use case where this would ever happen and like this is not an attack vector, but I just yeah, I just wondered if there's like it would be almost like hiding with with the sense of security. Like you'd have the badge of a you know, verification and yet there's something awful happening, but on purpose. Like I I

think a lot of times formal verification is used because the developers themselves want to ensure to themselves that this is acting right. But yeah, is there a way to hide something in it? >> Yeah, so in a formal sense, no. There's no there So these formal verification tools, they always like insist that if they say a theorem is true, the theorem is true. And they're they're pretty good at doing that. But if you know, let's say that I'm I'm an an adversary and I'm trying to do what you say, the way that I'm going to do it is I'm going to write the wrong theorem. And I'm going to try to convince you that the theorem is the right theorem. So So for example, you know, maybe my computer system has like five servers and I'm going to write a really great description, a really great

theorem about what four of those servers do. And my theorem is going to say sometimes they send the data to the fifth server, but the theorem isn't going to say anything about what the fifth server does with that data. >> Okay, but you're going to still be able to prove that those four servers do what they say they're going to do. >> Yeah, yeah. So these theorems, you know, these specifications, they really have to be thought about. >> Mhm. >> So you know, formal verification, it means you no longer have to think about the code, you no longer have to think about the implication, but you do have to think the implementation, but you do have to think about the theorem. And you need to think about what the specification is and whether it really captures everything that you care about. >> So there are also tricks that you can do

to have a passing proof of something that's not really formally verified or not a true theorem. For example, including an axiom that is false. >> Yeah. >> So you start with the false premise. >> Mhm. >> You write a theorem that will, you know, make you look great and then you get a proof that this theorem is fine. So yeah, there's always there is a way to do security theater through formal verification and we've seen some recent cases in the community. >> Oh, really? >> Yeah, yeah. Nadeem Kbeissi has been very vocal about certain cases. Shout out to him and this his great work. But yeah, it's it is tricky, and this is why I was going to ask you, Alex, about verifying during a zero-knowledge proof of Lean proof. How do you avoid these pitfalls

of, you know, wrong proofs or proofs that, you know, sneak in wrong things? >> Yeah, so so when you do a zero-knowledge proof of a Lean proof, you're hiding the Lean proof, but you're not hiding the theorem. So, you're not going to be hiding the axioms that they're using. And and these these kinds of examples that you're mentioning, that's always the flavor. The flavor is always the theorem is wrong, you know? Cuz you know, when you talk about an axiom, an axiom is a hypothesis under which the theorem is true, part of the theorem, right? So so this in this approach, we never hide what is being proved, and that's that's where people can engage in this kind of security theater by proving something that's not is the wrong thing, or as you were mentioning, maybe something that's not even meaningful, because if the hypotheses are false,

then it means nothing. So I I guess I think of the whole like zero-knowledge thing as kind of orthogonal to this question of of whether the theorem is is correct. And I think this question of like, "Hey, how do we stop people from constructing or like how do we detect if someone's writing down a theorem that's not right?" I think that's a really interesting research question for for sure. >> By the way, is there a succinctness element? You've been talking about ZK and the privacy aspect. Are Lean proofs big, and is does it make sense to make them shorter? >> Yes, they are big. And and yes, it might make that make sense to take that. So, there is a succinctness aspect. Here, it's something that we're really still trying to understand, because like scalability and like how big the Lean proofs are and how fast they can be

checked is already a huge priority for the Lean project. And like for getting, you know, they're not they're not using cryptography, but they're using systems techniques to try to to improve performance. But maybe cryptography could help, too. I you know, ZK-SNARKs proofs are like 200 bytes. So, you know, potentially it's useful to them. >> Ah, but then the question becomes what happens with some this error, you know? If you ever get something that goes wrong, then the whole of mathematics breaks down, you know, or like the whole of formal verification breaks down. >> Some some logicians are worried about this kind of stuff. Yeah, cuz you know, it's true. We we don't actually have a proof, right? We have a proof that, you know, somebody solved a hard problem or your theorem is true.

>> So, I feel like we still haven't actually dug into ZK-Pi. Like we sort of mentioned it I don't know, 20 30 minutes ago is like the reason that we're actually diving into this topic. But yeah, what is ZK-Pi? How does it fit into all of this? >> It's exactly the system that we've been describing. So, ZK-Pi is to ZK-Snark. So, it's a prover and verifier and set up. And the prover takes in a Lean theorem and a Lean proof and it outputs a very small number of bytes. And the verifier, which is the ZK proof, the verifier inputs the ZK proof and the Lean theorem and and says, "I'm convinced or I'm not convinced."

>> So, it's You should think of ZK-Pi like, yeah, it's this level of interaction on top of Lean that adds zero knowledge to the proofs and also compresses them. >> Can you tell us a bit more, Alex, about sort of the main challenges that went into constructing ZK-Pi? Like was it straightforward, you know, write a ZK proof of what Lean does or is there like difficulty? How did you make this efficient? >> Yeah, so so I think there's two things to say here. One is the core technical challenge that ZK that needed to be solved to make ZK-Pi and then like roughly how did we we solve that challenge? And you know, our goal, of course, is to verify Lean proofs. But you know, this topic of like how do you verify proofs, old topic in logic, people have lots of thoughts about how to do this. And the

dominant view of what it means to check a proof and the the view that Lean adopts is um something called the Curry-Howard correspondence, which yeah, is named for some old logicians. And it it says the way that you should view proof checking is that you should reduce proof checking to type checking. Like in the programming languages sense, like is my program well typed? And you need sufficiently advanced a sufficiently complicated type system, so think like Haskell but even more complex. These type systems are are called dependent type systems. So Lean uses a dependent type system called the calculus of inductive constructions.

And so so basically like inside you know Lean is like a big piece of software, but at the core it it's reducing the truth of your theorem to the well typedness of a calculus of inductive inductive constructions program. And what Zk-Pi does, what it used to do, is prove in zero knowledge that a dependent program is well typed. And you know, how do we do that? Like you know, maybe that's a little bit too detailed for for today, but you know, suffice it to say that like the classic ZK techniques of have the prover provide things and and and then check them instead of trying to compute them yourself, use randomness to optimize data structures.

All of this came came into came into um in doing this. >> in some of that work we talked about earlier in the episode on bringing in the randomness, using it in an effective way. >> Yeah. >> Is it a standalone proving system? Does it sit on top of something else? >> Yeah, so Zk-Pi actually it was like the I mentioned that you know, the reason that we started caring about randomness in zero knowledge circuits was was because we were solving various zero knowledge problems and and needed it. Zk-Pi was the first the first problem like this for us personally. So so we needed randomness in a proof system. So we had to define what that meant and come up with a proof system. So we have one, it's called Mirage Plus. It's got some security theorem that says if your circuit encodes an interactive proof

that is sound and complete for some language, then the ZK-Snark. So So you had that and then you had Serene on top of that and then you had Zk-Pi implemented on top of Serene on top of this proof system. >> So the underlying proving system is this Mirage? >> Right. Yeah, Mirage Plus is the name of that system. And then you should think of the Mirage Plus as construction as being similar to the Halo 2 construction and similar to the Mirage construction which came before it, which is based on Groth16. >> Okay. >> I guess the innovation there was that nobody People have been using this in-circuit randomness for a long time, but nobody had ever like said formally what it was supposed to do or like when I have a snark for randomized circuit, what does that mean? So, I guess Mirage Plus comes with a security theorem that

captures what that means. >> It's cool. I'm surprised I haven't heard that much about this. Like, it's almost it sounds like a cool technique that could be incorporated into some of these other systems. This and this is sort of an example system that did that. >> Yeah. So, I know that people have been sort of mimicking this interaction in-circuit by sort of taking challenges in circuit. They'd sort of hash plenty of data, get a challenge, and then do a randomized check. >> Okay. >> In this case, you're sort of doing it inside your circuit and it's quite expensive, whereas what Alex is describing makes this interaction sort of, you know, a first-class citizen of your proof system and of your circuit rather than like shoehorned into it.

>> Huh. >> Yeah. And I mean, Halo 2 does this. This is This is They They don't have like a security theorem to my knowledge that that matches, but but you know, I imagine that that one could write down the theorem and that it would be true and we could prove it. And you know, Halo 2 is going to be a better choice for many projects than Mirage Plus cuz Mirage Plus is based on Groth16 and it's got this pure per-circuit trusted setup. So, you know, good for an academic project, but probably if you're building a system, you don't want to incur those additional trust requirements. >> Got it. >> Doing one of these ceremonies. Yeah. >> Yes, those trusted ceremonies, they've been purged.

>> [laughter] >> Right? >> Yeah, yeah. So, for example, even us, when we were doing research on how to use this for anonymous credentials, we we built another proof system for these randomized circuits called Dorian, which is basically a modification to Spartan, which doesn't have these trusted setups. >> Alex, I feel like we've had a chance to cover part of your research. I actually know that you've also done work on collaborative snarks. Your Your name has popped up on lots of papers that we have featured in ZK mesh, our kind of collection of links that we share every month. But, I am curious and we don't have too much time here, but what kind of thing are you focused on today? Would you say this is the core of your focus?

Do you have some sort of threads that you're exploring? >> Yeah, I'm I'm always interested in insecure computation in in all its forms. So, everything related to zero knowledge, multi-party computation. It's not a specific app, sorry. But, >> [laughter] >> maybe be a little bit more specific. I think one thing that I I tend to think about a lot when we're when there's a secure computation system is, you know, when you have secure computation, you have security properties. But, you also have circuits, randomized circuits, VMs at different levels of the stack. You often have different computational models. Sometimes, I feel like these models are understudied. The cryptographers aren't really positioned well to study them because they don't think about programming languages. The programming languages people don't

understand the cryptography. So, like the model like they they don't even know they don't have any intuition about how to define the model cuz like the model sometimes involves randomness and other things that they don't like. So, I spend a lot of time thinking, you know, this whole randomized circuits thing is that lately we've been thinking about like shuffling in multi-party computation for secure statistics. That's another example. Like maybe shuffling there is part of the model. Even the collaborative proofs, there I guess, you know, it's like, "Oh, actually we're going to keep the computational model the same, but we want different security properties." So, you know, yeah, we want like, you know, distributed secrets instead of centralized secrets.

>> Very cool. I like that. It's like a through-line through the work we've just discussed and also the work before and maybe the work to come. So, yeah, thank you for doing this deep dive into theorem proving and letting me ask a lot of questions that I've had about what these things are, how they could work, how they're evolving, how they hit ZK, yeah, and how important they're probably going to become. Yeah, thanks so much. >> My pleasure. And you know, I think it's great that ZK is is really starting to touch a number of deployed systems in the world and and that just makes this kind of verification more important. So, the the more people that know it and understand it the better. I'm I'm so happy to be here.

>> Yeah, thank you both. This was incredibly enlightening. Like you said, Anna, the difference between theorem provers like Lean and SMTs for me is something that was always very hazy and today has made it incredibly clear. So, thanks a lot, Alex. >> Cool. I want to say thank you to the podcast team, Rachel, Henrik, and Tonya, and to our listeners. Thanks for listening.