Speaker 1: 0:00

Welcome everybody. This is episode 45 of Helios Horizons with Grigore Rosu from PyQuared. I'll get better at pronouncing that name, but I'm very excited to have him here. We have about an hour of conversations about his past, his present, his future. A brief introduction perhaps. If you don't know, grigore was a NASA engineer, is a professor for computer science at the University of Illinois Urbana-Champaign, is a researcher with an H-index of 67. I had to look up what that meant it's about and maybe Grigore can tell us a little bit more about it. But for the Nobel Prize you're usually in the range between 30 and 70. It's basically how often your works have been quoted by others, how important they are in the general state of cutting-edge research. He's also the founder of Runtime Verification and the founder of Pi Squared, a solver of very, very, very difficult problems that have to do with math, and he may be able to tell us about his love of Pi, which this intro song was about. Welcome to the stage, grigore. How are you?

Speaker 2: 1:23

Thank you. Thank you for inviting me. I'm very impressed that you know about the age index. That's a very academic thing. It means how many papers you have with more citations than that number. So I have 67 papers with more citations than 67. That's what it measures. That sounds like another difficult math problem there. Yes, it's made by academics for academics, to confuse everybody else, for sure.

Speaker 1: 1:56

Yes, very glad to have you here and very excited to talk about some of the things. One of the great privileges I think that we have on this podcast is to hear really amazing stories of people from different walks of life and how they ended up, let's say, generally speaking, in the technology sector. You've had a very interesting, I think, journey and, yeah, I would kind of just love to talk about your personal background a little bit. You obviously must have liked something about math, science, computers. You studied that first in Bucharest I think you are originally from Romania then moved to the US. But take us a little bit through your childhood and what kind of first sparked your interest in science, math and all of that?

Speaker 2: 2:53

Well, I grew up in communist Romania. So, as you know, in Romania the communism was abolished in 89. And that's exactly when I finished my high school, and there wasn't much you could do during communism in Romania. Essentially, you had to choose between some form of science or chess. You could be a great chess player or a gymnast, but that was not for me.

Speaker 1: 3:22

That's very exciting to me. Obviously I love chess.

Speaker 2: 3:26

Yeah, so I chose. I chose mathematics. So that's how I got into mathematics, because what I liked about mathematics was that you only had to learn one thing and do well, right. If you do physics or chemistry, you also have to learn mathematics, right. So too complicated. I just wanted to do one thing, mathematics. But then I I slowly moved into computer science and I did my college at the University of Bucharest in Romania, where I did well.

Speaker 2: 3:56

Computer science was not recognized as a field of science back then. It was an applied mathematics area. So I did the applied mathematics called computer science in college. And then I came to the United States in 96 for a PhD. I did my PhD at the University of California, san Diego, and then in 2000, I worked at NASA for two years in which I realized that I still like the academic life more than having a boat to say so and, you know, following precise government instructions.

Speaker 2: 4:37

So I returned to academia in 2002 here at University of Illinois, urbana-champaign, which is a top school in computer science. That's what attracted me. I really wanted to have very good students and, yeah, in 2010,. Then I started Runtime Verification, which back then was just a company doing formal verification, formal modeling of spacecraft, aircraft, mission-critical software in general. Our clients were NASA, boeing, toyota, these kind of companies, and in 2017, we got into blockchain and, before we knew it, runtime verification became a major security auditing company in blockchain. Actually, vitalik himself contacted us to audit his Casper protocol back then the Viper, and then also Uniswap and the deposit contract and so on and so forth, and yeah, yeah, very interesting.

Speaker 1: 5:41

I want to take you back a little bit, right. So you're at UC doing your PhD, and then you finish the PhD and then NASA calls what is that like? What were they trying to recruit you for? And then what did you actually end up doing at NASA?

Speaker 2: 6:01

So NASA had a very serious problem and still has a very serious problem, which is correctness of software. So, unlike on blockchains, where everybody can attack your protocol, on NASA nobody attacks the protocol, but it can still have errors and by those errors can be catastrophic. Right? So if you have a navigation error in your spacecraft software, then you can lose the whole spacecraft. Right? So if you have a navigation error in your spacecraft software, then you can lose the whole spacecraft. Right? So, hundreds of millions, maybe billions of dollars. And that's what I've done. I used my techniques that I developed during my PhD and before that, mathematically grounded techniques that essentially reduce computation in any programming language to mathematical reasoning. And then you can reason about programs and prove that the programs are correct. Right, Because testing can only take you so far. With testing, you find errors in programs. With formal verification you prove that the programs are correct. Right, so there, are no bugs.

Speaker 1: 7:03

So this is also the name. So runtime verification isn't just the name of your first company, it's also the name of a formal mathematical method. Is that correct?

Speaker 2: 7:14

That is correct, but that comes with a funny story. So when I was at NASA, together with a colleague at NASA, we developed a technique to prove programs correct as they execute. It was a mixture between two very well-established fields testing and formal methods and formal verification. And what we did? We did the following. We said how about this? How about running the program and testing it as it executes at runtime? How about this? How about running the program and testing it as it executes at runtime? And if we see any problem as it executes, let's fix it on the fly. Ok, so we had a list of possible errors and a list of possible fixes and essentially we managed to steer the program so that it always satisfies these requirements. Ok, so this is another way to prove the program correct through testing.

Speaker 2: 8:09

Okay, and the funny story is that we were super excited that we submitted the paper to the best conferences, of course, in formal methods and in testing, and our paper was rejected at all these conferences. The formal methods conference said well, this is a testing paper. The testing conferences they said, well, this is a formal verification paper. So we couldn't get the paper in because it was a different category. And then, actually that's an interesting lesson I learned. Then we said let's give it a crazy name, let's call it runtime verification, because testing verification doesn't make sense. So we said let's call it runtime verification.

Speaker 2: 8:41

And we submitted to another major conference and the paper was immediately accepted. Not only it was immediately accepted, but it started a whole new trend, a whole new current in our area of computer science. Now there is an international conference called runtime verification. All the major conferences have topics and sessions dedicated to runtime verification, right? So the lesson I learned is that sometimes you know how you position something can make all the difference. Just the name, just two words. Runtime verification changed everything, which was a bit unfair initially, but I guess that's how people are right they have limited bandwidth. But I guess that's how people are right, they have limited bandwidth.

Speaker 2: 9:24

I agree.

Speaker 1: 9:25

Very, very instructive. And is this also like, was that the first spark to, you know, like for the entrepreneurial journey as well, being there, like okay, we have this thing that kind of nobody can categorize at the moment. It's definitely something that's needed, it's something that's new, bringing two formal methods or well trodden paths kind of together. But now we have a way of of unifying that and applying it and it's going to become immediately useful for very, very, um, you know, interesting use cases and big players, big companies that we can service. What was kind of the, the, let's say, leap from the theoretical research into this practical tool and the business.

Speaker 2: 10:08

Yes, definitely, yeah, definitely. That was the trigger. So I invented this concept in 2001, when I was still at NASA, as I said, with my NASA colleagues, and then, in 2002, I joined university as an academic and I started the company eight years later, runtime verification in 2010. And I started the company eight years later, runtime verification in 2010. And the reason I started the company is because runtime verification had a lot of not only a lot of traction, but also proved to be very practical. You see, in formal verification, usually the joke goes like you know, I use formal verification a few times and each time I use formal verification, I wrote a paper about it, so implying discreetly that these things are not very practical. But, on the other hand, testing is practical because it finds bugs, but testing doesn't prove correctness. So we managed, for the first time, to actually, using runtime verification, prove correctness differently than so. We managed, for the first time, to actually, using runtime verification, prove correctness differently than formal verification. Right, we proved correctness of a system by proving that we do not let the system go wrong, instead of proving the system correct. You see, because we monitored the system, instrumented the system, and each time we saw that it took a wrong path, we corrected it on the fly. That was very appealing to NASA, to Boeing, to Toyota. It's interesting as an academic, I also had grants, academic grants, with many of these important mission critical software developers.

Speaker 2: 11:43

I showed them in academia these results and they said this is very practical, you should do a company. Actually, they encouraged me to do a company. Toyota in particular was my first, uh, our first client around time verification. And uh, toyota said start a company and we'll, we'll sign a contract. All right, that's what I've done. That's why I started the company around time verification that's.

Speaker 1: 12:04

That's so cool, and also, you know, like being able to then go back to your network, like NASA, and have those first real contracts, et cetera. It must have been such a. It's obviously such a luxury, but so great. I also want to talk about one more academic achievement or framework, and because perhaps this also plays a role in what you're doing right now the K-framework and matching logic. Tell us a little bit about what that is. Also one thing that I read I don't know if it's correct is you developed that with a student, which is also, I think, super cool, this sort of, let's say, cross-generational collaboration there? So talk a little bit about the K framework please.

Speaker 2: 12:45

Yes, the student part is Trajan. Trajan was one of my first students and we designed the K framework together. He's an amazing engineer. When I implemented the first version of K and then the second version, he said Grigore, please do theory, let me do the implementation Right, thank you. So the K framework framework I started thinking about it also when I was um at nasa. Um and actually that's one of the reasons I moved to academia I realized that I cannot develop such something so big um at nasa. I needed to have my own research lab with students and postdocs and do it together.

Speaker 1: 13:27

So you're saying NASA limited your research ability because it wasn't big enough?

Speaker 2: 13:31

That's true. Well, yes, and also funding. It's a governmental institution, after all, right, and funding was always scarce and I had to justify everything. I had a group but only three, four people I could work with, and I mean, the group I was part of was large, one of the largest formal methods group, but my group, who I can work with on my problems, was very small. I wanted a bigger group to do things, big things, right. So here is what we realized at NASA when we did formal verification. So here is what we realized at NASA when we did formal verification that actually the models that describe the systems or the programming languages were themselves very ad hoc. Ok, so we were verifying Java programs back then.

Speaker 2: 14:19

But what is Java? If you think about it, that's a very hard question actually. What is Java? Or or what is Python? Or what is EVM? You can say, well, it's whatever this compiler, whatever this tool implements, but that's not rigorous enough and that's why it's not even clear when you find an error. Or when you find an error, people don't fix it because it's not clear what the language is. And I said well, boy, we have a bigger problem here, bigger than formal verification. We need formal definitions of actual things like programming languages in particular. And yeah, there was no way to formalize rigorously what we call now the semantics what is called the semantics well, it's always called the semantics but to have an actual mathematical definition that very rigorously says what the language is, not how it is implemented, because we humans are very good at how, once we know what we are doing, we can do it well and fast and correct and so on. But what? How to say what the programming language is? And there was no way to do it and I started developing the notation initially, then a notation, and another notation and eventually a meta-language. How we call it.

Speaker 2: 15:40

Now took shape the K framework, and we call it K because everything. Well, initially we wanted to call it C, but C was taken because everything in K starts with the letter C. But it's basically mainly related to a concept in programming languages called continuations and that's what inspired the K framework. Basically, the K framework is like a meta programming language in which you can implement other programming languages, but the nice thing about it is that once you implement a programming language in K, that K gives you a menu of buttons like interpreter, compiler, program verifier, runtime verifier, model checker right and you push that button and the K-Framework generates the tool automatically for you, and very efficiently actually, from the actual mathematical definition of the programming language. And to give you a feel for it, because whenever I tell people about this they say, oh, it must be dead slow. Tell people about this, they say, oh, it must be that slow.

Speaker 2: 16:47

Actually, at this point we have a formal semantics of EVM and with the interpreter, the interpreter button of the K framework for EVM. When we push it on the EVM semantics, we get an interpreter which we call KEVM, which is actually comparable let's not say faster, but comparable in performance with GET, which is the most popular interpreter for EVM. So performance is not the issue anymore. But what is nice about it is that the K framework is actually a mathematical framework. So the programming language, evm in that case, is an actual mathematical definition with axioms. You know, same like Euclidean geometry or algebra group theory, right? So same like those. Programming language becomes a set of axioms and logic, which logic is a set of proof rules that allows you to do reasoning. Actually, that's matching logic. Matching logic is the logic underlying the K framework that allows you to do reasoning about programs, about any programs in any programming languages. And the beauty of matching logic is that it is very, very compact, very small. You can write it on a napkin. That's how small it is.

Speaker 1: 18:01

Yeah.

Speaker 2: 18:02

I mean quite amazing. And why it's important to be small is because at some point you'll have to ask yourself what do I trust? What can I trust here? So of course you'll have to trust the mathematical definition of the programming language. But then if I give you a mathematical proof, like a program execution executed correctly, why should you trust it? Right? So that's when you reduce everything to mathematical proofs and now you check the mathematical proof. But to trust the mathematical proof you have to trust the logic in which that mathematical proof is written. Because if you have a logic in which zero equals one, then that logic is meaningless. And that's why it's important for the logic to be small.

Speaker 1: 18:42

And I feel we'll probably get back to that and something called proof of proof and all of this stuff that you guys are doing at PiSquare in a little bit. But you already mentioned EVM and Ethereum and also your customers for runtime verification becoming some of the well-known blockchains. What was your first encounter with blockchain? Do you remember sort of like a moment when you first heard about maybe Bitcoin or Ethereum I don't know what it was for you and then kind of like when you grasped what that concept actually meant and what kind of sucked you into, you know, perhaps wanting to build with it, on it and for it?

Speaker 2: 19:22

So there are two defining moments. So first, I heard of so first of all, I heard of blockchain very late. I started in 2017 or so, but I think one year before that, 2016,. I heard it from a student of mine. You may know his name, his name is Philip Dayan, so now he's the founder of Flashbots and he was a student of mine and also working at runtime verification at the same time and he told me Grigore, there is this interesting thing called Bitcoin. You may want to look into it. It's pretty cool. And I didn't get a chance to look into it.

Speaker 2: 19:59

And then a bug, a major bug in Ethereum happened, and he got super excited about how interesting that bug was and he presented it to the entire company and to me in particular, and I said, ok, this is super cool, actually. So then I also realized that this is an excellent area where we can apply everything. We know all the programming language, semantics, the formal verification, the K framework, everything runtime verification. And then, very, very shortly after, I received a message from Charles Haskington asking if we could exactly that, if we could use our techniques to do formal verification of Ethereum contracts. Then my first reaction was who is Charles Hawkinson? So I checked him out a bit and I said, okay, he's legit. Then we started working together with IOHK. They gave us several grants to formalize programming languages in the K framework and then do formal verification of different properties.

Speaker 2: 21:08

And that's how we ended up doing security auditing and runtime verification, actually thanks to those grants. And then Vitalik also gave us some grants to formally verify Casper he has the protocol Casper in Viper back then Then also to formally verify Uniswap, and so, basically, and the deposit contract also that allow you to move funds from proof of work Ethereum to proof of stake Ethereum. So I think Grand Tide Reduction was literally the first company in the Web3 space that brought formal verification right. It's the highest assurance level of security auditing. I didn't even know what security auditing meant back then. I just thought it would be a form of verification. And then other people called us security auditors. Okay, then we are security auditors, yep, so that was our entry in blockchain. And then it was a wild ride.

Speaker 2: 21:59

Once we started doing blockchain, we had fewer and fewer contracts in other areas. We still continue to work with NASA. Nasa was a continuous customer for runtime verification. We had fewer and fewer contracts in other areas. We still continue to work with NASA. Nasa was a continuous customer for runtime verification, but we kind of dropped almost all the others for blockchain.

Speaker 1: 22:17

Because things were getting faster in blockchain. Charles, being one of the first people that you met in blockchain, was that something that really helped you get over any concerns that you like? I mean, it came from a smart student that worked for you that you respected, so I assume you didn't really have, like all of these oh, it's a scam, it's like just money laundering. All of these preconceived notions probably never, yeah.

Speaker 1: 22:41

And then Charles, as somebody who himself, you know, respects science quite a bit, to put it mildly was probably a good encounter for this. Let's say, scientific application, also of blockchain right, like something where it was really a new technology to be applied, where not only did you find a great use case for the systems that you had developed, but a way to expand them and perhaps make them even more effective. In this public ledger, I don't know Was there something where it kind of clicked that this is where you would want to focus in the future when you encountered that technology.

Speaker 2: 23:21

I knew it right away that what we do would immediately apply to blockchain, because it was really a field in desperate need, actually, of formal verification and formal modeling. I had another student at the same time well, a bit later, yilong Li, who founded MegaEth, actually, and he was also working in the same office back then with Philip and myself, and it was pretty clear that there was a lot of interesting I don't know interesting ideas around, and I could see it in their eyes, sparks and all that you know that you see in good, exciting students when they're excited about interesting intellectual problems. I think I fell for it because of them, but also because of Charles Harkinson, who actually, once it was clear that we can use our techniques for blockchain, he actually came to Urbana-Champaign. He came to us and spent a few days together back then, together with a few other folks from IOHK, and then at that moment I think I realized that maybe this thing is bigger than I think.

Speaker 2: 24:42

Yeah, and I was still skeptical about the whole field. I just said, ok, it's a good application domain for what I do. But then I got somehow sucked in. I started using the protocols, we started receiving requests to do formal verification of different protocols, and then I started playing with these protocols. Before I knew it, I was hooked right, and now I'm also hooked.

Speaker 1: 25:06

So yeah, that that's very interesting to me. This, this idea of like the, let's say, the philosophical underpinning of blockchain, right, like it's one. It's a very interesting technology. That's that's one thing. But then this idea of decentralization, uh, ownership and and all of these, um, you know, cypherpunk ideas that are really imbued in this concept of what it is, is that something you know again, like it sounds like you kind of went into the technology first and then learned about those underpinnings later, but, like, is this something that's now also become very important to you?

Speaker 2: 25:43

Or is this just, let's say, say, a technology where you can apply and um, no, no, I'm all in, also philosophically, um, and actually I'm much more in than my children, for example um, I, I really believe in it. I think this is the future of money, um, everything, future of us, um, it's um, I'm only what I. What I'm not super sure is what kind of blockchain is the right answer, or what kind of blockchain technology is the right answer. I think that's still a moving target, but I'm definitely all in that this is the way to go for us as a species, at least in the shorter term.

Speaker 2: 26:24

One thing that you mentioned, which I'm not entirely sure is so critical, conceptually, for me at least, is decentralization. I know it's very important to many people, but to me, decentralization is just a mechanism, right, it allows us to achieve what we want, right, and I think what we want from blockchains are the good old safety and liveness properties which we can dive into, but this is what we've done since forever in formal methods. And then, additionally, the payment system capability right, so, um, I can pay, you know, peer-to-peer um and um, my payment is safe, actually, not only pay, but I can also execute any programs. And that is safe, meaning that it's all verifiable and public, right, so I can verify it, I have the program, I have the programming language, I can verify it. And then also, liveness means that things keep happening. Right, like censorship would be the opposite of you.

Speaker 2: 27:25

I'm not censorship right Like censorship would be, you know, the opposite of you. Want no censorship, right, in order to have a life system, and I think we cannot. So, yeah, so decentralization helps with all of this, but you see, those are more important as properties, but of course, they are harder to explain to cyberpunks, as you call them, and other enthusiasts. Right, but I think, as far as we can be sure that the payment or an execution of a program is done correctly, that is like 90% of the job done. And the blockchains do that and how they do that, by having a decentralized network of validators that validate that, and now you know that it is correct because you don't have to trust any one party. Great, but there could be other ways to do it and I think there will be in the future and they are being developed as we speak. You know, like these CK proofs and so on. Yeah, let's, I mean, we also developed it in Pi Square.

Speaker 1: 28:27

Exactly Great segue. I was going to say let's talk about Pi Squared and what led you to now found a company. That I believe is sort of like, let's say, a continuation of runtime verification in some ways, but then tackles a set of new problems. So what was sort of the first impulse, impetus that made Pi Squ squared, an idea in your head, and then how did you go about actually founding it and, kind of like, what problems are you solving with it?

Speaker 2: 28:58

So I mean, I think, well, okay, so for us, for me, having a programming language, semantics, which means a mathematical definition of the programming language, is the religion. I think that is a must and not having it I think it's irresponsible, right, Because then you cannot talk about correctness, you cannot talk about truth, you cannot. It's just, you know, hand-waving without such a formal definition. And in runtime verification we made that also very practical, to the point that we could actually do formal reasoning about smart contracts and protocols and everything. But one thing that we learned at runtime verification is that no matter how good the programmers are, there are still errors. Errors lurk everywhere. You know errors in protocols, errors in code, errors in compilers, errors in interpreters, Errors, errors, errors, errors. And you know I shouldn't complain because it was good business for runtime verification, Right? So that's what brought us clients. But on the other hand, I had my own ambition to do things right. I think I accomplished my academic career. Well, there's still more to do, but I was very happy with my academic career. I just wanted to have an impact also in the real world and to do things right. And that came hand in hand with lots of engineering improvements of the K framework. Because when we realized that wait a minute we can actually generate an interpreter, that is, a mathematical prover, from a programming language semantics, EVM in particular which is comparable in performance with actual ad hoc, manually implemented interpreters for the same language that have bugs, because that's what we've done in RR verification we found bugs in those. Then I said wait a minute. So then why should we do things any other way? Why should we take the risk to implement manually in an app manner language when we can shoot two birds with one stone? I think that's how the proverb goes, I'm not sure Right? So basically, have an actual formal definition of the programming language and an implementation generated from it. And when we generate implementation from the definition this is what we call correct by construction, right, Informal verification, informal methods when there is nothing to formally verify, nothing to prove.

Speaker 2: 31:41

Correct because it's been generated to be correct, correct because it's been generated to be correct. And when we realize that we can actually have correct by construction tools, in particular interpreters, execution engines, generated directly from the formal, semantics, mathematical definition of the programming language. That's how blockchain should be developed. That's how blockchain should be developed. That's how we should reduce all this informal notion of computation to the very rigorous and well-understood notion of mathematical proof, and if we can do that, then the problem of verification of computation reduces to verification of mathematical proofs. And one interesting thing about mathematical proofs is that they are a lot harder to come up with than to verify, than to check. You probably remember from school, right? So the hard part was to come up with the solution in your math plus right, not to not to check it. To check it, you can check it quickly. So that's what happened actually. Once we did that, we realized that we can have very, very simple, robust and fast verifiers of computation by reducing computation to mathematical proofs and then having verifiers for mathematical proofs.

Speaker 2: 33:20

That idea came in 2019-2020, two or three years after we started runtime verification doing blockchain audits. I talked to several people, including Charles Haskinson, actually, who was a big fan of the idea, and, yeah, so we realized that this is a whole new domain, a whole new business actually, which diverges a bit from runtime verification, because it goes into execution, into one execution, not all executions, right. With runtime verification, it goes into execution, into one execution, not all executions. With runtime verification, it proves that all executions are correct, but now we only care about one execution, the one that's taking place, and it made sense from many different aspects business, legal to just spawn a new entity, and that's what we've done. That was about one year ago, in early 24, early 24. We raised our first round in February no in Q1, okay, 24. And yeah, and here we are now.

Speaker 1: 34:21

Yeah, I mean that also must have been an interesting journey, and I want to go back to, similarly to runtime verification. It seems like you had basically the luxury of having some people in this space already that liked this solution, that believed in, let's say, this concept and this ZK proof, proof of proof this mathematical construct underpinning an actual, let's say, execution and making it I don't know correct, by default, almost. I'm sure this is mathematically wildly incorrect language that I'm using here, but semantics right. So talk a little bit about who you're working with, what kind of problems, like concrete problems you're trying to solve that exist in the blockchain space now.

Speaker 2: 35:08

So, first of all, we are a very new company. We just started, right, just one year, but we already formed several partnerships with blockchain major some of them major players and what we offer is basically two things combined together right, the super fast payment system and I'll get back to that and then also super fast settlement layer, but a settlement layer that goes through correctness. Okay, so if you have any claim, any computational claim, which is true in our view, if you make any claim that is true, you should be able to come up with a mathematical proof. If you cannot, then there is no reason to trust the claim. Once you have a claim that comes with a mathematical proof, now we verify that proof and then we settle the claim. We verify that proof and then we settle the claim. Think of it as a database of truths like Wikipedia with verified facts. Wikipedia where you have a checkmark for the fact which says verified. But these facts, these claims, can be, in particular, executions of programs In any programming languages.

Speaker 2: 36:26

In particular, for example, one of the claims that we use a lot are blocks in Ethereum. So an Ethereum block is a claim that says that you go from state one to state two with this block of code, which is the block, block of code, which is the block, and what we do. We verify that using the K framework, the matching logic, all this reasoning that we told you, and that happens very fast, so at speed comparable to actually running the block with Get. So you see so now, instead of running. So this gives ideas. Right, how to develop new architectures of blockchains? Right, because you can imagine how you have a very fast execution engine or execution layer whose only job is to generate that S1 and S2, the state before and after the block. That becomes a mathematical statement, a claim, and the proof of that now can be constructed with a K-framework and verified at the same time using the formal semantics. And if you do that, and suppose that you can do that very fast, now you have an actual mathematical proof, which is even better than zero-knowledge proofs. We'll get to zero-knowledge proofs as well.

Speaker 2: 37:49

Zero-knowledge proofs are not as precise as mathematical proofs. Now you have a mathematical proof that that block was executed correctly and, moreover, that that proof has been checked and passed the check, so it's correct. So now you know that that block is correct, you see? So, in particular, if you're an optimistic rollout, let's say, and you generate such a block right, and that is verified mathematically. Suppose that it takes I don't know 300 milliseconds right Now you know with certainty, maximum certainty, that nobody can fight any fraud or any incorrect execution, any error in that block. So you can finalize it, so you can get nearly instant finality in an optimistic rollout if you use these techniques under the hood, which is also what they get with zero knowledge proofs, but not much less latency than with zero knowledge proofs. Yeah, fascinating, there's so many interesting sectors.

Speaker 1: 38:45

I think that we could less latency right than with your knowledge proofs. Yeah, fascinating. I mean, there's so many interesting sectors I think that we could explore there. We have like about 15 minutes left and I have a lot more questions to ask you, so I want to just maybe hone in on one maybe use case, or perhaps it's even not Like with the rise of AI and you know, agents perhaps being one of the most interesting use cases for blockchain. You know autonomous entities sort of executing things. Is this something that you guys are thinking about with Pi Squared as well?

Speaker 2: 39:21

Oh, yes, very, very much, very much. We actually have partnerships in place with three major AI agent companies and I cannot mention them now because I want to have a surprise later when we launch our DevNet and both of these problems are solved perfectly by the Pi Squared network. One is payment systems. Okay, so they need micropayments, they need lots of payments, very fast payments. We'll very soon live in a world where there will be millions of agents, maybe billions of agents right, working for us in parallel at the same time, and they need to pay each other, right. So blockchains are too slow for that. Even if you have a blockchain that does say 100,000 transactions per second because there is some anecdotal evidence that some blockchain can do that Well, even that is too slow for these agents because now they will have to pay each other. If you have a billion agents at the same time, you have to wait hours for our agent only to stay in line, basically Because on the blockchain, the block, the philosophy of blockchain is chain, meaning a total order of transactions and blocks. Now, that's an optimization, how to make things a bit faster, but the chain is the big problem, because now you force all the agents to stay in line right, also with many other applications, and many agents are completely unrelated. You know, if an agent makes you know a request for a service from another agent, now they have a causal dependence, so they have to wait after each other. But most agents will be independent. They will do their things in parallel and there is absolutely no conceptual or technical or engineering reason right to wait for each other in line. And that's exactly what we do with Pi Squared. We have this concept of a settlement layer. So, first of all, the payment system will allow all these agents to pay themselves very fast.

Speaker 2: 41:35

It's based on an algorithm called FastPay, which is a pretty new protocol. It was, I think, published in 2020. It's an alternative to Bitcoin. It's an amazing paper. I love that paper. I'm super excited about this paper Not written by me, but all respect for the authors of that paper Because what they show?

Speaker 2: 41:57

They show that you can have a payment system which is provably correct meaning no double spending, okay Without enforcing a total order on messages, right? So Bitcoin had this amazing revelation that if we totally order all the transactions, then we'll avoid double spending. Yes, but that's a huge price to pay. So FastPay avoids completely that problem, which is amazing. It's so inspiring that we decided to build our infrastructure, extending that protocol right.

Speaker 2: 42:28

So our network, decentralized network of validators, basically has accounts same like blockchchains, and there is a payment system based on, on fast pay, but there is no chaining, no total order, no block chain per se, um, but you can also settle programmatically.

Speaker 2: 42:49

You also have smart contracts, but they do, you know, they defer the work to actually different programming languages running with the K framework and so on, but what's important is that they can settle computations done by agents and states of agents.

Speaker 2: 43:05

Okay, so an agent can say, hey, I've done this computation, this inference, and I have a proof that I've done the inference correctly, right, using this program that you trust on your data, that is yours, so you can now trust the inference, so it's verifiable, which, remember, that's what we want from blockchain verifiability, right, and the payment system. So both payment system and verifiability are now supported. And again, what is super important here, and very, very important for AI in particular, is that all these settlements of different states or different claims made by different agents are completely independent of each other, so they can be handled completely in parallel and the whole architecture scales horizontally, so there is no notion of tps, no notion of you know um, if you need more claims, first of all you don't have transactions, we have claims. If you need more claims per second, then you add more validators, right. So, horizontally, a horizontal scalability. And yeah, I was going to ask about the PPS question.

Speaker 1: 44:14

Basically, it sounds like this ceases to be a major issue because, again, like you were just saying, you just add validators that don't add blocks. Though Can you explain that a little bit, Like it's not a block, Sorry, they add blocks but they're not in the chain.

Speaker 2: 44:33

Let me explain. Take mathematics we have mathematical theorems. Okay, I can verify. So if you give me proofs of mathematical theorems, I can verify all these theorems and their proofs completely independently of each other. Okay, so of course, this doesn't answer your question directly. But now let's take a blockchain where you have blocks Block one, block two, block three, right, so these blocks? There is an execution layer. Okay, take MegaEth, for example. Megaeth we love the project MegaEth. It's super fast, very clean. By the way, it's funded by Yilong Li.

Speaker 1: 45:12

Your student. You're a blockchain founder factory yourself.

Speaker 2: 45:16

Well, yeah, I mean, they did better work than I did in Web3, but you know we are coming slowly behind, right? So take MegaEats MegaEats is super fast, right? 20,000 more transactions per second Each block. Of course, k will not keep up with it, right? So that would be unreasonable to hope in the near future. But the nice thing is that MegaEats will generate all these claims. Basically, each block is a claim, but this is important it has the stage before and after, right, because MegaEats already explored, executed those transactions at its amazing speed, right, and it generated all the states before and after. So now each claim, block one, block two, block three. Now they become completely independent of each other. You see, I don't have to wait for block one to be verified before I verify block two. No, I can verify them in parallel because I already have the states, and this is the philosophy of the entire decentralized network. So anybody can generate such claims as far as they come, with all the evidence to verify them. They are verified and settled and there is no dependence whatsoever.

Speaker 2: 46:37

By complete deliberate design, we didn't want to have any. You know that there are some efforts to extend blockchains to work with partial orders instead of total orders on transactions. That's great, but we want to drop completely any ordering, so now we have zero ordering on claims in our decentralized network. You see what we don't offer, though? We do not offer the likeness part, because you know that's not our job, so we kind of defer that to blockchains like MegaEth or others, right? So they do great. They do an amazing job at sequencing in the smartest possible way, being fair, avoiding censorship and so on. They may prove that that can be a claim. Actually, you can claim that I didn't censor anything.

Speaker 2: 47:27

These are all the claims, all the transactions and so on. We only focus on verifiability, right and payment, and this is perfect, also for agents, right? So from Pi Square's perspective, there is little to almost no difference between an AI agent or a blockchain, a layer one or a layer two or, for that matter, a high-speed trading platform or Coinbase or Hyperliquid right, For us, all of these will generate claims and will claim a new state based on some computation. It's done from a previous state. That's what we do with blocks. That's what agents do. You move from one state to another in a provably correct way, and that's what we do. We verify those proofs and then we settle whatever they say, provided that it checks. So we are like two-thirds of a blockchain, but that allows us to completely this, completely unchain. You know the concept completely eliminate the bottleneck that comes with total ordering unchained blockchains, what?

Speaker 1: 48:34

what a fascinating and like mathematically rigorously applied concept, and this was something um I I also wanted to ask, like this this is very interesting, this conversation, in the sense that for you, or with you there, there really isn't a big difference between, let's say, the the research part and then the innovation that comes perhaps more with the entrepreneurship aspect of it. It's like so interesting to see this merge, and we also learned that you've had some students that have started their own businesses, and very, very successfully. So is there some advice that you could give to people out there? So is there some advice that you could give to people out there? Like you know, you have a finding and especially I'm talking really like academics or students that have great ideas how to turn those into businesses and perhaps even, like you know, apply science a little bit more in this entrepreneurship space.

Speaker 2: 49:37

I think it is much, much harder than it sounds, and actually I think the higher, the more educated you are and you know, the more advanced you are as a scientist and as a researcher, the higher your age index is in order to know what age index means the harder it is. And why is that? It's because of the analytical nature of researchers and scientists, right. So in business, you have to take quick decisions and, even if they are not the right decision, you have to take quickly some decision and move on to the next thing. You have to take quickly some decision and move on to the next thing. And you have to be driven by the actual needs coming from the real world, from clients, customers, partners, and not and this is very important and not from what you believe is the right problem to solve, because we tend all of us to fall into our comfort zone, and for a researcher or a scientist, the comfort zone is to have a very hard and difficult problem to solve. That's what they've been trained to do, that's what they love to do. That's what I love to do when I wake up in the morning. Trust me, I'd rather prove a mathematical CRM than think of how to make a partnership with a new company that I know we need to make a partnership with, right, um. But so what you need to learn is to unlearn, um, all, all the, all the hard stuff, right, and to realize that that that, uh, what you need to be successful with a company is to take decisions quickly and the right decisions. So the more you have to think about a decision, I think, the clearer it should become to you that probably you're not on the right path. And also there is another which is hard to explain, but I'll just tell you two words and then we can build from there. It's called premature optimization, right? So that's actually one of the big traps that smart people fall into. I've seen it over and over and over again and I fall myself into that trap over and over and over again. That trap over and over and over again, right?

Speaker 2: 51:54

Because you have to solve a problem and instead of understanding the problem from the outside and having the strength to not dive into the interesting guts of the problem before you really understand the problem well, we don't have that power, right? We just immediately see something super interesting in that problem and dive into it. You know, take another piece of paper, another paper and another coffee and you realize that half a day is gone and that's the life of a scientist, which we love, I love. But in business you have to, you know, in entrepreneurship you have to go top down, understand the problem and realize that finding the actual solution to the problem so answering the how part, once you understand the what, for highly educated researchers and scientists, that's the easy part.

Speaker 2: 52:46

I know it sounds weird but it's really the easy part. Once you know exactly what you need to do, that's easy. How to do it, because we've been trained to do that. So I would strongly recommend um researcher scientists to join forces with somebody you know who is a bit more into the business, marketing side of things, right, and to listen. That's also important, to listen to these people yeah, very interesting.

Speaker 1: 53:12

um, I have a. I mean so many things that we didn't get to talk about, but I want to bring it back just quickly, because you mentioned NASA still being one of your clients today and I wonder about how you think about this nexus of the blockchain and space industry. I mean, I'm sure you know, but is NASA exploring that? Do you see that kind of like coming together in terms of like, maybe even interplanetary communication as a settlement layer between different I don't know space-time concepts, etc? I think it's two of these.

Speaker 2: 53:50

That's a premature optimization. So first of all, we have to solve the problem with airspace, right? So the old aircraft, air traffic systems and so on, those you know, should definitely use blockchain, and I think they started to look into it. And then we move on to the, you know, to the spacecraft. But, yes, nasa is interested in principles. So is Boeing, right, in blockchain. They even, I think, gave me a grant at university to explore blockchains in aviation, but it was all mostly about recording and settlement. Right, they wanted to settle the important decisions that were taken, you know, like the black box they have in airplanes, you know like the black box they have in Airplace, but, you know, in a way that is verifiable and, you know, provable, because in litigation, if an accident, there is an accident, right, you have to prove that you've done everything right.

Speaker 1: 54:46

Maybe the pilot you know did everything right, Especially when you're Boeing these days. Yeah.

Speaker 2: 54:52

Right, right, right, right. So I would say that this will grow organically.

Speaker 1: 55:08

To be honest, I think we'll have a new generation of blockchains which could be pretty different from the block, being mindful of your time here, um, but the next five, ten years, sort of like, where do you see blockchains heading like? You're mentioning perhaps even a different way of of computing? You've mentioned a lot of interesting, um, different ways of constructing the whole infrastructure. Where do you see it, you know, heading both technologically and then perhaps in in how it's going to be applied in the near and midterm future?

Speaker 2: 55:40

So I can, you know, I can tell you what I aim for with you, know, with Pi Squared and you know with our team. Right? So we believe in an interconnected world. Right, in a unification of value and not fragmentation. Right? So this concept of total value locked is so wrong because it goes against. We propose a different concept. We call it total value unlocked.

Speaker 2: 56:09

Right, so once blockchains settle right on our settlement layer, blockchains settle on our settlement layer, then each application will have access to all the liquidity and all the value on all the different chains, and not only chains, but also AI agents or other Web2 applications that also want verifiability for their claims, like a centralized exchange, for example, could want that. And that's how I believe. I think it will be an organic growth and a slow transition into an interconnected world, an interoperable world, where the programming language that is being used, or the particular chain on which you have your tokens, or the particular AI agent that acts on your behalf, all this will live together. But for all these we still need verifiability. I'm firmly convinced that you cannot avoid verifiability, because without verifiability is not Web3. And you need the payment system, but it's more general than payments. It's more like a digital asset system. Right, because there's the fundamental thesis of Web3 that your assets are yours, you hold them, you control them and you can transfer them, of course.

Speaker 2: 57:34

So I think that these are the two fundamental pillars that I don't think will change, which is payment Blockchain is a payment system and is a verifiability layer settlement layer, but we see all kinds of creativity on the other side of lightness how to use these features, how to execute, how to generate interesting ideas, how to hallucinate, even interestingly Right. So all of these will be open and we don't have to limit them. I think honestly. I think the blockchains they are today, they are pretty rigid, Right, Because of the total ordering. So the more you look into this problem, the more you realize that it's not that necessary and at the same time, it is very limiting on the other hand.

Speaker 1: 58:30

Yeah, I mean very, very interesting takes there. Last, very last question for you, one like what's next for you for Pi Square, of course? And then also, you know, where do you want to be in the next decade or so? What's the legacy you kind of want to leave with in the blockchain space, or maybe in science? Are you looking for that Nobel Prize?

Speaker 2: 58:57

I don't think I can get a Nobel Prize, first of all because Nobel Prize doesn't go in computer science or mathematics, so I missed the opportunity, so no.

Speaker 1: 59:04

Yeah, you chose the wrong path there in the beginning in Romania, not the physics.

Speaker 2: 59:10

Nobel is not the only award. Yeah, that's true, that's not important. What's important is, as you said, to have a legacy to you know, to feel that you've done something meaningful. And I think, in science, to me, matching logic is the, you know, the climax, because I searched for it all my career. It is the smallest possible logic that you can have that is expressive enough to capture as logic reasoning. Right, any computation in any programs, in any programming languages, and more than that, basically, anything that is true, provably true, can be proved and verified using matching logic. So that's and, of course, the key framework that led to it and the key framework is based on it. They kind of go together. So that would be in science, Now in blockchain, what I just told you previously.

Speaker 2: 1:00:00

I would like, in five years or so, to have, you know, a different view not super different, but still different view of decentralization, where we do use decentralization to verify truths, right, because you don't want to have only one verifier, right For something that becomes forever a truth. You want to have decentralization there, to have more opinions, more. Even if you have a ZK proof, even if anything, you still, once you settle it and you say, this is from now on, absolute truth, then you need decentralization there, but I think that is the only place where you really need decentralization, or we should enforce decentralization. So, yes, what I'd like to do in the Web3 space is to, together with my team because this is a big, big effort is to launch this network decentralized network of truths and payment, a payment system, basically an infrastructure for decentralized assets and transfer of them and settlement, and then to hopefully see more and more blockchains, ai, agents, other applications integrate with it, because I believe in interconnectivity and interoperability.

Speaker 2: 1:01:25

So mathematics unifies everything right. In mathematics, it doesn't matter if you use Pythagoras theorem to prove a trigonometry problem or an algebra problem. They are all true. It doesn't matter that they are in different languages once they are proved, so same should be in Web3. The programming languages should be only some notations that are useful to express certain things in a certain way, but no more, no less than that. Interoperability should come for free and everything should be connected. That's what I believe.

Speaker 1: 1:01:59

Yeah, thank you so much, grigore. It was a really interesting conversation. I wish we had more time where, like, maybe we'll have you back sometime very soon when you guys are fully launched on mainnet or something, we'd love to talk a little bit more about what you're doing and everything you've achieved along the way. Yeah, thank you so much for taking the time. Thank you for inviting me. Pleasure, thank you everybody for listening. This was Helios Horizons, episode 45, with Grigore Rosu of Pi Squared and Runtime Verification. Some very interesting thoughts on how mathematical proof can really enter and alter the course of blockchain and technology. Yeah, thank you again so much, gregore, and talk very soon. Thank you all, bye, bye, until next time.

Speaker 2: 1:02:46

Bye, bye.