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

AI Engineer · 10 min · 137 sentences · from YouTube's caption track

Each timecode opens YouTube at the start of that sentence. Line anchors (#s42) are the cue ids in the WebVTT, and every line carries its start and end seconds. All transcripts has every talk, and the whole corpus as one file.

1. 00:01[music]
2. 00:12Coding agents are generating more code than ever.
3. 00:16Builders are generating hundreds and thousands of PRs every week.
4. 00:21How do you know that this is correct?
5. 00:24Using LM as a judge for the code?
6. 00:26Well, that's probabilistic.
7. 00:29Tests?
8. 00:30They only check some inputs, not all.
9. 00:33Human code review doesn't scale to match agent speed.
10. 00:37None of these can say for all inputs the code is correct.
11. 00:42Formal verification can.
12. 00:44Hi, I'm Varun Pant.
13. 00:45I build AI products at AWS leading teams at in formal verification.
14. 00:51Formal verification provides mathematical proof that code is correct.
15. 00:56For all inputs.
16. 00:57You write what correct means, which is the specification, and a formal verification tool proves that your code satisfies it.
17. 01:05If the proof passes, it holds for every possible input.
18. 01:11How do you use this?
19. 01:13Well, one way is back driven development, for example, with Kiro.
20. 01:19You write what the specification is, which is what correct means.
21. 01:23Either you write it formally, for example, directly in Lean, or you write it in natural language, and you let the AI auto formalize it.
22. 01:32Now, this is really important.
23. 01:33You then validate the specification.
24. 01:36So, either the human reviews it, or you test that it holds on some inputs.
25. 01:41And this is important because the specification is upstream.
26. 01:43It's a living, breathing artifact that the builder interacts with.
27. 01:47You want this to be correct.
28. 01:49Everything else is downstream from this.
29. 01:52The AI coding agent then goes and implements from the specification.
30. 01:57And the formal verification tool proves that the implementation matches the specification.
31. 02:04So, humans own the specification and machines own the code and proof.
32. 02:10Lean is a programming language and a proof assistant.
33. 02:14It is the same language for the definitions and proofs.
34. 02:17There's no translation layer.
35. 02:20It is implemented in Lean, which means it's very extensible.
36. 02:23And this is important.
37. 02:24It has a small trusted kernel.
38. 02:27Proofs can be exported and independently checked.
39. 02:33So, here's an example of a Lean file which has both the code and proof in the same language.
40. 02:39At the top, you'll see the code, which is a function that reverses a list in Lean.
41. 02:44So, reverse of one, two, and three gives three, two, and one.
42. 02:47And right in the middle, you'll see a theorem.
43. 02:51This is the proof.
44. 02:52And this theorem prover approves a property which says that reverse of A plus B is in fact reverse of B plus reverse of A. And this holds for every possible input.
45. 03:04How do you do this?
46. 03:05You have something called as tactics which do the work, which we'll get to in a second.
47. 03:09And the kernel, remember the small trusted kernel?
48. 03:12That checks the work.
49. 03:16A good analogy to understand the Lean proof assistant is that of chess.
50. 03:20So, in chess, your goal is to checkmate the opponent.
51. 03:23And you make a bunch of moves.
52. 03:24You move the knight, you move the bishop.
53. 03:27Similarly, in Lean, you have a bunch of tactics which are your moves.
54. 03:32And it's the same chess board.
55. 03:34It's interactive.
56. 03:36You want to prove the goal, the theorem, checkmate.
57. 03:39And you're kind of going down a tree.
58. 03:42So, you're traversing the tree, you're trying different tactics.
59. 03:45Maybe for some goals, you're not able to prove it, so you backtrack and then you try another a branch of the tree.
60. 03:51Very similar to chess.
61. 03:53And finally, you get a goal that hopefully proves the theorem, and then that small independent kernel confirms and checks it.
62. 04:03The kernel catches the mistake.
63. 04:05So, here's an example at the top where an incor- incorrect proof is rejected immediately.
64. 04:11And you only need to trust the small kernel.
65. 04:14The good thing is that you can have multiple independent kernels.
66. 04:17You yourself can actually go write one.
67. 04:19It's completely open source.
68. 04:20You have kernels in C++, Rust, Lean.
69. 04:23That's uh a link to the Arena Lang where you can go and add a kernel.
70. 04:30So, let's look at some examples where you can put this to practice.
71. 04:35The first one is having the specification and code both being in Lean.
72. 04:41Now, this is open source Andreo.
73. 04:44AI converted zlib, which is a C compression library, to Lean.
74. 04:47Now, granted this happened over a week or so.
75. 04:52But, kind of going back to our specification methodology that we mentioned where you had specification at the top and then verification for the code, we'll kind of see the same thing here.
76. 05:03So, the natural language specification says that you decompress the output of compress returning the original data.
77. 05:11And then, you have an AI that generates the formal spec.
78. 05:14Now, remember this is important.
79. 05:16Checking the specification is key.
80. 05:19After you do that, the AI goes and writes your code in Lean, and then generates these helper lemma subgoals, and proves the theorem.
81. 05:28And at the bottom, you can see that it's verified with that small independent kernel.
82. 05:34So, what you just saw was that AI decomposed the problem into lemmas, which are subgoals.
83. 05:39It proved each of them using tactics.
84. 05:41Remember the chess moves that we were making?
85. 05:44And it assembled it into a final theorem.
86. 05:47Checkmate.
87. 05:49And the kernel checked it.
88. 05:51And this particular example had 32,000 lines of proof.
89. 05:54So, it was pretty big.
90. 05:58Let's take another example.
91. 05:59What if you have code in Rust?
92. 06:01Well, you can write the functional specification of it or the model in Lean.
93. 06:06An example of that is Cedar.
94. 06:08Cedar is an open-source authorization policy language, which is used by AWS verified permissions and access.
95. 06:15The specification of Cedar is written in Lean.
96. 06:19The production code runs in Rust.
97. 06:22Why is this important?
98. 06:23Because let's take an example.
99. 06:25You have forbid Trump's permit.
100. 06:27You want to make sure that for any forbid policy being satisfied, the request is always denied.
101. 06:32This is key.
102. 06:36Here 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 run differential random testing
103. 06:45to check that both of those for the same inputs give the same output.
104. 06:50And there's about 100 million differential random tests uh run nightly.
105. 06:54No version ships until this is satisfied.
106. 06:59Let's take another example.
107. 07:01What if you have code in Rust and you want to deductively verify with Lean or solvers?
108. 07:07Before we go there, let's quickly talk about this new term solvers.
109. 07:10So, remember we spoke of Lean being this chessboard interactive where you're making a bunch of moves trying to checkmate.
110. 07:17A solver is a calculator, a very powerful one.
111. 07:21You feed in a formula and it returns an output.
112. 07:25In this case, satisfiable or unsatisfiable.
113. 07:30So, an example of this is Verus, also an open-source tool.
114. 07:35It uses this solver, this very powerful calculator, Z3.
115. 07:39And if folks are familiar with adding annotations, it's kind of similar to that where you can add specifications in the form of that.
116. 07:47And the code is in line.
117. 07:50So, you see these two requires and ensure keywords, that's what we call a pre and post condition.
118. 07:56What must be true before and what must be true after.
119. 08:01And this is a static check.
120. 08:02It's enforced by the verifier and erased at runtime.
121. 08:05So, almost like ghost code.
122. 08:09Another example of this is Eneus, which uses the mid-level intermediate representation for Rust and does a functional translation to Lean.
123. 08:18And right after that, you use the same theorem prover, the same chessboard that we spoke of.
124. 08:26Now, you may be asking, well, what if I have any programming language?
125. 08:32We at AWS have been working on an open-source tool called Strata.
126. 08:37This is work in progress, but the idea is that you can have any programming language and you yourself can create what we call a dialect.
127. 08:46Think of this like a compiler.
128. 08:47You have a high-level intermediate representation and you lower it down to a low-level intermediate representation, which is what Strata core is.
129. 08:55Now, this is written in Lean.
130. 08:58After you have all of these programs talking in the same language, which is the Strata core, you can dispatch it to any of the engines.
131. 09:05For example, the Lean proof, remember the chessboard, or the very powerful calculator, SMT solvers, or model checkers.
132. 09:17So, you can get started with this today.
133. 09:19You 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,
134. 09:29which is very important, and then you can let your coding agent implement it and your formal verification tool prove it.
135. 09:38So, hopefully in this brave new world, we have software and systems that are not probably correct, but probably correct.
136. 09:46Thank you.
137. 10:01[music]