Yoichi Hirai (zkSecurity) - Your guide to formal verification when machines write Lean proofs

Hello. I'm Yoichi. I work at ZK Security now. I have some reputation about wearing things on stage. I think that's how you get invited to events.

Um this is for the Beast mode. Uh the Beast mode is not uh furry thing. Trust me. Um I will talk about formal verification. I will make very specific suggestions based on the current events.

Um formal verification is about getting correct software implementations. But the scenery is changing because uh computers have started writing mathematical proofs that check proof assistant that passes the checkers in the proof assistants like Lean. Um this trend has hit the headlines so far in the pure mathematics only. But similar ideas can be used for similar techniques can be used for program verification as well. So this has changed the economy of getting correct software implementation.

And then I'll tell you about this. So this talk is mostly about having ways to check that your software implementation does what you expect. Not necessary like not everybody needs to check all the software you use. But there has to be an access accessible accessible way to do that. Um this is a sovereignty thing.

Open source is one component. So you have the source code that helps. But usually the implementation is so big that you don't want to read it all. And even after you read it all um you don't get much confidence because it was just so big. So um I will be talking about strategies to make the situation better.

Um to be honest the amount of efforts will never go to zero. And you don't get an absolute guarantee. But I'll talk about the best way that seems to work currently. I will try the method I'll be presenting. And that's the only edge I have.

I did something like this 9 years ago in Paris. That was also in Ethereum conference that some of you attended. I talked about formal verification of Ethereum smart contracts. Um so I was saying that the EVM is so simple that you can prove programs correct and that's useful. Um that was in February of 2017.

And after several months EVM Ethereum virtual machine was specified in uh formal verification framework called K framework. The spec is called K EVM. It is still being developed and used by company called Runtime Verification in some parts of the activities. Another company called Certora was founded a year later and they are also developing and using a formal verification tool for EVM smart contracts. People from both companies are around if you are attending this offline.

So you can talk to them. Um I have not been involved in these companies directly. But the thing is I called the technological trend right? And I'm going to make another prediction at the end of this talk. But I'm going back a little bit.

Um here's a title of a talk in 2003 by Leslie Lamport. Leslie Lamport got Turing Award for distributed consensus work. And that's being used you know that line of work is being used in the in the consensus layer of Ethereum today. The title of the talk was The Future of Computing Logical Biology. These are two ways of dealing with computer systems.

One is logical. Logic starts from the first principles and use deductions to get uh properties that you want of your system. Biology the other way biology is biological biology kind of approach is used when the system is too complicated to understand. And the Lamport noticed that words like viruses are used in computer attacks. So like he noticed these biological ways are creeping into computer science.

Lamport's talk starts like this. In the late '60s Boole uh Floy and Hoare discovered the concept of program correctness. Some people initially working on program correctness thought that in the future everyone would prove that their programs were correct. Programming errors would then disappear. And this has not happened.

After 50 years there are still bugs. Why aren't people proving their software correct? There was a blocker until maybe October September October last year. Why people didn't prove their software correct? It was just number of person years.

Look at the examples like there's a proven correct C compiler called CompCert. It took three person years until the first version. There's Okay, there are people um doing formally verified compilers. But nobody has ever like created a proven correct C++ compiler. Well, nobody has made a proven correct Rust compiler.

So many major languages don't have proven correct compilers. There are people building a proven correct compiler for Viper a smart contract language. And I think you can hear about this after this talk in the another stage. But it's not yet the mainstream common practice. Another example is uh proven correct hypervisor.

Hypervisor is uh small operating system that can run multiple virtual machines on top of it. There's a family of hypervisors called L4 and there's one formally verified one called seL4. It took 22 person years of effort to implement and and prove it correct. There's an ongoing effort to port this to other machine architectures and to maintain it and so on. But it's a massive effort.

The situation changed greatly last year. Um I just took this from a video. But this this is a slide from Harmonics Alex Best. The talk was done last year in December. And Harmonics is a company providing an AI agent that can turn math papers into proofs in Lean proof assistant.

And there are hobbyists and the mathematicians who are using Harmonics tools to um check mathematical results in the proof assistant Lean. This can help expanding the boundary of human knowledge. But when I think about program verification um the usual proofs in program verification is much simpler much more repetitive than contemporary math. So I have an answer to this question. Um computers can prove theorems.

What's next? One of the next things is to use this new theorem proving ability to um check the software correctness. There's another company called Math Ink. This company is also developing AI agents that can help translating math results into the Lean proof assistant. Um here we are seeing posts about a world of mathematical abundance.

Or uh in the limit formal verification will be too cheap to meter. Math Ink has chosen careful formulation by saying in the limit. Um I'm showing you that there are businesses doing automatic theorem proving. And they are very confident that the the technology will be cheaper. I tried some AI tools and the coding bots and Aristotle's harmonic, too.

These tools are already useful for writing proofs about software implementations. This changes the economics a lot. But we have to be careful. Um this is not the end of my talk, just half. Um when something gets cheaper, something else gets becomes the new bottleneck.

So, let's step back a little bit and see what can be the bottleneck. This is a whole picture of formal verification. The aim of formal verification is to make sure that the reality matches the expectation. But So, whichever tool you use, you needed to describe the reality using the tool. And the expectations in the tool as well.

Um those descriptions are called models. I don't like the word choice of the word here. So, models usually look like just program code. Sometimes they uh logical formulas, sometimes they are programs that obtain a way like the models in the reasoning tool is code. Um the models needed to be accurate for the whole process to be useful at all.

So, now what's getting cheaper the what's getting cheaper is this comparison of models in the reasoning tool. That's getting cheaper. So, the new bottleneck is somewhere else. Um So, what are the bottleneck? The big biggest biggest thing you can control is the choice of the reality you choose you reason about.

Um I don't think the real world as a whole is a good target of formal verification because the uh totality of the real world is messy enough. That's too messy. So, the reality you choose, the domain of reality you choose first needs to behave with some predictable regularity. Um the reality can behave deterministically or non-deterministically, but even if it's non-deterministic, um the set of outcomes needs to be known in advance for any logical reasoning tools to be useful. Another thing is the choice of the expectation.

If the expectation is written in a language that requires a judge to interpret, it might not be a suitable problem for reasoning tools. Um So, here's a problem. Maybe this is the most important thing here. Like So, the there are like very popular programming languages like C++ or there are like popular CPUs like Intel's CPU or ARM's CPU. Um These things usually These things have sometimes thousands of pages of specifications like modern CPUs have tens of thousands of pages.

So, if somebody like translates these big specifications in a proof assistant and tell me this is the specification of the CPU, then uh first I don't trust it and you know, I don't want to read through all the 10,000 pages and compare that to some code, either. And even if I do that, um I will have a very difficult time convincing other people that this is the translation of that big thing. Um this will will be the biggest bottleneck. So, my goal here is that everybody can learn and put reasonable efforts to check that programming language is described correctly in a proof assistant. So, we have to watch out the complexity of programming language.

So, we need a reality with lean interface. Um I can I will show you some good examples that seem to work. The first example is the Ethereum virtual machine, EVM. Um EVM is simple enough. And from very early days, the EVM has multiple implementations and they have been compared against each other on the real network test network and using the test suites.

So, when you create a new model of EVM or implementation of the EVM, you can compare your model against the actual implementations using many ways. And that helps a lot. But there there are already like professional companies doing this, so I won't go into much detail. Um the thing with EVM is the expectations are a little bit difficult. Like there are many many different kinds of attack attack situations that you have to be aware about.

So, writing the correct expectation for EVM smart contracts is not very straightforward. This requires domain knowledge and oversight. The second example is the uh arithmetic circuit for succinct arguments and zero-knowledge proofs. Here, the reality consists of polynomial equations. And the proof assistants know a lot about polynomial equations already because people have been doing mathematics on proof assistants.

Also, um people use arithmetic circuits for like hash function or virtual machine or something that can be um described mathematically easily enough. And after that, you can benefit from the coming mathematical abundance. Zcash is doing a project about this called Lean. It's supported by the Ethereum Foundation. Other teams are doing similar efforts.

So, this area is popular right now. The last example I have is RISC-V. RISC-V is a CPU architecture. It's very simple. Maybe it's simpler than EVM.

So, it's possible to implement or specify RISC-V in a proof assistant. It's better yet because the official RISC-V specification has been translated into Lean and this has been also supported by the Ethereum Foundation. And once you code up your expectation of what your RISC-V program would do like maybe the Ethereum virtual machine, then you also benefit from the coming or already existing mathematical abundance. Um I'm doing a project about this called it's called EVM ASM. And this might be useful for the Beast mode Ethereum.

It's a way to It's It's a proposal to scale Ethereum using the uh succinct arguments. I promised I will make a prediction. My prediction is that there's a new stack of proven correct software. It's vibe coded assembly plus vibe proofs on your proof assistants or theorem provers. And yeah, this will be useful for system programming, operating systems, cryptographic implementations.

Uh EVM ASM is a first good to go, I think. I think this approach will spread to spread to wider area of software development. That's all. Um please ask me questions. I mean, I can ask my voice in the mic.

Better? Yeah. Sorry, just first of all, thank you very much. It's It was a really fun talk. For this last point, can you elaborate a bit more on what your stack looks like here?

If you can, of course. How much of this is custom? How much of these tools are uh tools that are that will be available to others? Like what's your balance? Do you think general purpose models would, for example, work well here or do you need to do your own uh fine-tuning {slash} your own stack building?

So, um this combination like writing assembly code and proving them in a proof assistant has been around for maybe maybe four decades or something. And So, when I when I started this EVM EVM ASM project, I told the coding bot to like give me uh RISC-V program verification framework and have a look at this paper. And it did that. It made some mistakes, but you know, the separating conjunction or the separating logic should be separating, but it was not separating or something like that, but you know, once I tell it to fix the um you know, mistakes, it was also already So, yeah, at the moment I'm doing it in a very custom way. I mean, that's the way to get a very like simple setup.

But, probably as this approach gets popular things will be standardized a little bit. I guess it's about to be time. Maybe one quick question is possible, maybe not. Last chance, I think. Thank you very much.

[applause]