Your Code Has Bugs. Lean4 Has Proofs: Formal Verification for Engineers — Varun Pant, AWS

Why none of the usual checks clear agent output

00:12Coding agents are generating more code than ever. Builders are generating hundreds and thousands of PRs every week. How do you know that this is correct? Using LM as a judge for the code? Well, that's probabilistic. tests. They only check some inputs, not all.

00:29Human code review doesn't scale to match agent speed. None of these can say for all inputs the code is correct. Formal verification can hi varun pant. I build AI products at AWS leading teams at uh in formal verification. Formal verification provides mathematical proof that code is correct for all inputs.

00:51You write what correct means which is the specification and a formal verification tool proves that your code satisfies it. If the proof

Specifications humans own, proofs machines own

01:06passes, it holds for every possible input. How do you use this? Well, one way is specdriven development. For example, with Ko, you write what the specification is, which is what correct means. either you write it formally for example directly in lean or you write it in natural language and you let the AI autoformalize it.

01:32Now this is really important you then validate the specification. So either the human reviews it or you test that it holds on some inputs and this is important because the specification is upstream. It's a living breathing artifact that the builder interacts with.

01:39You want this to be correct. Everything else is downstream from this. The AI coding agent then goes and implements from the specification and the formal verification tool proves

Lean as one language for code and proof

02:00that the implementation matches the specification. So humans own the specification and machines own the code and proof. Lean is a programming language and a proof assistant. It is the same language for the definitions and proofs. There's no translation layer.

02:18It is implemented in lean which means it's very extensible and this is important. It has a small trusted kernel. Proofs can be exported and independently checked. So here's an example of a lean file which has both the code and proof in the same language.

02:33At the top you'll see the code which is a function that reverses a list in lean. So reverser one two and three gives 3 2 and one. And right in the middle you'll see a theorem. This is the proof. And this theorem prover proves a property which says that reverse of a plus b is in fact reverse of b plus reverse of a.

02:56And this holds for every possible input.

Tactics, theorems, and the chess analogy

03:04How do you do this? You have something called as tactics which do the work which we'll get to in a second. And the kernel remember the small trusted kernel that checks the work. A good analogy to understand the lean proof assistant is that of chess.

03:16So in chess your goal is to checkmate the opponent and you make a bunch of moves. You move the knight, you move the bish bishop. Similarly in lean you have a bunch of tactics which are your moves and it's the same chess board. It's interactive.

03:33You want to prove the goal, the theorem checkmate. And you're kind of going down a tree. So you're traversing the tree. You're trying different tactics. Maybe for some goals you're not able to prove it. So you backtrack and then you try another branch of the tree.

03:48Very similar to chess. And finally you get a goal that hopefully proves the theorem and then that small independent kernel confirms and checks it.

A small kernel you can independently rebuild

04:03The kernel catches the mistake. So here's an example at the top where an incorrect proof is rejected immediately and you only need to trust this small kernel. The good thing is that you can have multiple independent kernels. You yourself can actually go write one.

04:14It's completely open source. You have kernels in C++, Rust, lean. That's uh a link to the arena lang where you can go and add a kernel. So let's look at some examples where you can put this to practice. The first one is having the specification and code both being in lean.

04:41Now this is open source andreal AI converted zib which is a c compression library to lean. Now granted this happened over a week or so but kind of going back to our specification methodology that we

Rewriting zlib into Lean, and 32,000 lines of proof

04:57mentioned where you had specification at the top and then verification for the code. We'll kind of see the same thing here. So the natural language specification says that you decompress the output of compress returning the original data and then you have an AI that generates the formal spec.

05:12Now remember this is important. Checking the specification is key. After you do that the AI goes in writes your code in lean and then generates these helper lema sub goals and proves the theorem. And at the bottom you can see that it's verified with that small independent kernel.

05:34So what you just saw was that AI decomposed the problem into lemras which are sub goals. It proved each of them using tactics. Remember the chess moves that we were making and it assembled it into a final theorem checkmate and the colonel checked it.

05:43And this particular example had 32,000 lines of proof. So it was pretty big. Let's take another example. What if you have code in Rust? Well, you can write the functional specification of it or the model in lean. An example of that is Cedar.

06:06Cedar is an open-source authorization policy language which is used by AWS verified permissions and access. The specification of Cedar is written in lean. The production code runs in Rust. Why is this important? Because let's take an example.

06:22you have forbit trumps permit. You want to make sure that for any forit policy being satisfied, the request is always denied. This is key. Here you can see the example of what I was talking about which is you have the Rust production code and you have the functional specification in lean and you

Cedar: Lean semantics, Rust in production

06:44run differential random testing to check that both of those for the same inputs give the same output. And there's about 100 million differential random tests uh run nightly. No version ships until this is satisfied. Let's take another example.

06:59What if you have code in Rust and you want to deductively verify with lean or solvers? Before we go there, let's quickly talk about this new term solvers. So remember we spoke of lean being this chessboard interactive where you're making a bunch of moves trying to checkmate.

07:15A solver is a calculator, a very powerful one. You feed in a formula and it returns an output. In this case, satisfiable or unsatisfiable. So an example of this is Varys, also an open source tool. It uses this solver, this very powerful calculator Z3.

07:30And if

Solvers, preconditions, and code erased at runtime

07:40folks are familiar with adding annotations, it's kind of similar to that where you can add specifications in the form of that. And the code is in line. So you see these two requires and ensure keywords. That's what we call a pre and post condition.

07:49What must be true before and what must be true after. And this is a static check. It's enforced by the verifier and erased at runtime. So almost like ghost code. Another example of this is enius uh which uses the mid-level intermediate representation for rust and does a functional translation to lean.

08:17And right after that you use the same theorem prover the same chess board that we spoke of. Now you may be asking well what if I have any programming language. We at AWS have been working on an open-source tool called starter. This is work in progress but the idea is that

Bringing any language into the same core

08:40you can have any programming language and you yourself can create what we call a dialect. Think of this like a compiler. You have a highle intermediate representation and you lower it down to a low-level intermediate representation which is what strata core is.

08:49Now this is written in lean. After you have all of these programs talking in the same language which is the startup core, you can dispatch it to any of the engines for example the lean proof remember the chessboard or the very powerful calculator SMT solvers or model checkers.

09:17So you can get started with this today. You can go to lean in in your browser with the link I pasted and you can pick your most critical code. Write what correct means which is the specification which is very important and then you can let your coding agent implement it and your formal verification tool prove it.

09:38So hopefully in this brave new world we have software and systems that are not probably correct but provably correct. Thank you.