WEBVTT

NOTE Sentence-level transcript of https://www.youtube.com/watch?v=lRa9sPaMyy4

NOTE One cue per sentence. Cue ids are the line anchors on /transcripts/lRa9sPaMyy4.html. A cue ends where the next begins, or 2 s after its last word.

s1
00:00:01.309 --> 00:00:03.309
[music]

s2
00:00:12.880 --> 00:00:16.360
Coding agents are generating more code than ever.

s3
00:00:16.360 --> 00:00:21.360
Builders are generating hundreds and thousands of PRs every week.

s4
00:00:21.360 --> 00:00:24.360
How do you know that this is correct?

s5
00:00:24.720 --> 00:00:26.760
Using LM as a judge for the code?

s6
00:00:26.760 --> 00:00:29.120
Well, that's probabilistic.

s7
00:00:29.120 --> 00:00:30.320
Tests?

s8
00:00:30.320 --> 00:00:33.480
They only check some inputs, not all.

s9
00:00:33.480 --> 00:00:37.680
Human code review doesn't scale to match agent speed.

s10
00:00:37.680 --> 00:00:42.320
None of these can say for all inputs the code is correct.

s11
00:00:42.320 --> 00:00:44.560
Formal verification can.

s12
00:00:44.560 --> 00:00:45.800
Hi, I'm Varun Pant.

s13
00:00:45.800 --> 00:00:51.320
I build AI products at AWS leading teams at in formal verification.

s14
00:00:51.360 --> 00:00:56.040
Formal verification provides mathematical proof that code is correct.

s15
00:00:56.040 --> 00:00:57.720
For all inputs.

s16
00:00:57.720 --> 00:01:05.840
You write what correct means, which is the specification, and a formal verification tool proves that your code satisfies it.

s17
00:01:05.840 --> 00:01:10.800
If the proof passes, it holds for every possible input.

s18
00:01:11.920 --> 00:01:13.920
How do you use this?

s19
00:01:13.920 --> 00:01:18.960
Well, one way is back driven development, for example, with Kiro.

s20
00:01:19.200 --> 00:01:23.280
You write what the specification is, which is what correct means.

s21
00:01:23.280 --> 00:01:32.360
Either you write it formally, for example, directly in Lean, or you write it in natural language, and you let the AI auto formalize it.

s22
00:01:32.360 --> 00:01:33.960
Now, this is really important.

s23
00:01:33.960 --> 00:01:36.360
You then validate the specification.

s24
00:01:36.360 --> 00:01:41.040
So, either the human reviews it, or you test that it holds on some inputs.

s25
00:01:41.040 --> 00:01:43.920
And this is important because the specification is upstream.

s26
00:01:43.920 --> 00:01:47.680
It's a living, breathing artifact that the builder interacts with.

s27
00:01:47.680 --> 00:01:49.400
You want this to be correct.

s28
00:01:49.400 --> 00:01:52.920
Everything else is downstream from this.

s29
00:01:52.920 --> 00:01:57.640
The AI coding agent then goes and implements from the specification.

s30
00:01:57.640 --> 00:02:03.960
And the formal verification tool proves that the implementation matches the specification.

s31
00:02:04.680 --> 00:02:09.960
So, humans own the specification and machines own the code and proof.

s32
00:02:10.840 --> 00:02:14.360
Lean is a programming language and a proof assistant.

s33
00:02:14.360 --> 00:02:17.920
It is the same language for the definitions and proofs.

s34
00:02:17.920 --> 00:02:20.480
There's no translation layer.

s35
00:02:20.480 --> 00:02:23.920
It is implemented in Lean, which means it's very extensible.

s36
00:02:23.920 --> 00:02:24.880
And this is important.

s37
00:02:24.880 --> 00:02:27.400
It has a small trusted kernel.

s38
00:02:27.400 --> 00:02:31.680
Proofs can be exported and independently checked.

s39
00:02:33.520 --> 00:02:39.280
So, here's an example of a Lean file which has both the code and proof in the same language.

s40
00:02:39.280 --> 00:02:44.400
At the top, you'll see the code, which is a function that reverses a list in Lean.

s41
00:02:44.400 --> 00:02:47.920
So, reverse of one, two, and three gives three, two, and one.

s42
00:02:47.920 --> 00:02:51.000
And right in the middle, you'll see a theorem.

s43
00:02:51.000 --> 00:02:52.920
This is the proof.

s44
00:02:52.920 --> 00:03:04.280
And 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.

s45
00:03:04.280 --> 00:03:05.440
How do you do this?

s46
00:03:05.440 --> 00:03:09.360
You have something called as tactics which do the work, which we'll get to in a second.

s47
00:03:09.360 --> 00:03:12.360
And the kernel, remember the small trusted kernel?

s48
00:03:12.360 --> 00:03:15.120
That checks the work.

s49
00:03:16.200 --> 00:03:20.040
A good analogy to understand the Lean proof assistant is that of chess.

s50
00:03:20.040 --> 00:03:23.200
So, in chess, your goal is to checkmate the opponent.

s51
00:03:23.200 --> 00:03:24.800
And you make a bunch of moves.

s52
00:03:24.800 --> 00:03:27.600
You move the knight, you move the bishop.

s53
00:03:27.600 --> 00:03:32.880
Similarly, in Lean, you have a bunch of tactics which are your moves.

s54
00:03:32.880 --> 00:03:34.720
And it's the same chess board.

s55
00:03:34.720 --> 00:03:36.040
It's interactive.

s56
00:03:36.040 --> 00:03:39.959
You want to prove the goal, the theorem, checkmate.

s57
00:03:39.959 --> 00:03:42.000
And you're kind of going down a tree.

s58
00:03:42.000 --> 00:03:45.040
So, you're traversing the tree, you're trying different tactics.

s59
00:03:45.040 --> 00:03:51.200
Maybe for some goals, you're not able to prove it, so you backtrack and then you try another a branch of the tree.

s60
00:03:51.200 --> 00:03:53.880
Very similar to chess.

s61
00:03:53.880 --> 00:04:02.520
And finally, you get a goal that hopefully proves the theorem, and then that small independent kernel confirms and checks it.

s62
00:04:03.520 --> 00:04:05.480
The kernel catches the mistake.

s63
00:04:05.480 --> 00:04:11.160
So, here's an example at the top where an incor- incorrect proof is rejected immediately.

s64
00:04:11.160 --> 00:04:14.680
And you only need to trust the small kernel.

s65
00:04:14.680 --> 00:04:17.320
The good thing is that you can have multiple independent kernels.

s66
00:04:17.320 --> 00:04:19.079
You yourself can actually go write one.

s67
00:04:19.079 --> 00:04:20.640
It's completely open source.

s68
00:04:20.640 --> 00:04:23.760
You have kernels in C++, Rust, Lean.

s69
00:04:23.760 --> 00:04:30.400
That's uh a link to the Arena Lang where you can go and add a kernel.

s70
00:04:30.680 --> 00:04:35.040
So, let's look at some examples where you can put this to practice.

s71
00:04:35.040 --> 00:04:41.360
The first one is having the specification and code both being in Lean.

s72
00:04:41.760 --> 00:04:44.000
Now, this is open source Andreo.

s73
00:04:44.000 --> 00:04:47.560
AI converted zlib, which is a C compression library, to Lean.

s74
00:04:47.560 --> 00:04:52.360
Now, granted this happened over a week or so.

s75
00:04:52.720 --> 00:05:03.520
But, 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.

s76
00:05:03.520 --> 00:05:11.000
So, the natural language specification says that you decompress the output of compress returning the original data.

s77
00:05:11.000 --> 00:05:14.440
And then, you have an AI that generates the formal spec.

s78
00:05:14.440 --> 00:05:16.280
Now, remember this is important.

s79
00:05:16.280 --> 00:05:19.080
Checking the specification is key.

s80
00:05:19.080 --> 00:05:28.760
After you do that, the AI goes and writes your code in Lean, and then generates these helper lemma subgoals, and proves the theorem.

s81
00:05:28.760 --> 00:05:34.400
And at the bottom, you can see that it's verified with that small independent kernel.

s82
00:05:34.480 --> 00:05:39.560
So, what you just saw was that AI decomposed the problem into lemmas, which are subgoals.

s83
00:05:39.560 --> 00:05:41.640
It proved each of them using tactics.

s84
00:05:41.640 --> 00:05:44.640
Remember the chess moves that we were making?

s85
00:05:44.640 --> 00:05:47.760
And it assembled it into a final theorem.

s86
00:05:47.760 --> 00:05:49.080
Checkmate.

s87
00:05:49.080 --> 00:05:51.440
And the kernel checked it.

s88
00:05:51.440 --> 00:05:54.680
And this particular example had 32,000 lines of proof.

s89
00:05:54.680 --> 00:05:57.960
So, it was pretty big.

s90
00:05:58.840 --> 00:05:59.960
Let's take another example.

s91
00:05:59.960 --> 00:06:01.640
What if you have code in Rust?

s92
00:06:01.640 --> 00:06:06.720
Well, you can write the functional specification of it or the model in Lean.

s93
00:06:06.720 --> 00:06:08.720
An example of that is Cedar.

s94
00:06:08.720 --> 00:06:15.880
Cedar is an open-source authorization policy language, which is used by AWS verified permissions and access.

s95
00:06:15.880 --> 00:06:19.280
The specification of Cedar is written in Lean.

s96
00:06:19.280 --> 00:06:22.320
The production code runs in Rust.

s97
00:06:22.320 --> 00:06:23.280
Why is this important?

s98
00:06:23.280 --> 00:06:25.480
Because let's take an example.

s99
00:06:25.480 --> 00:06:27.720
You have forbid Trump's permit.

s100
00:06:27.720 --> 00:06:32.800
You want to make sure that for any forbid policy being satisfied, the request is always denied.

s101
00:06:32.800 --> 00:06:35.120
This is key.

s102
00:06:36.320 --> 00:06:45.680
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 run differential random testing

s103
00:06:45.680 --> 00:06:50.120
to check that both of those for the same inputs give the same output.

s104
00:06:50.120 --> 00:06:54.960
And there's about 100 million differential random tests uh run nightly.

s105
00:06:54.960 --> 00:06:58.520
No version ships until this is satisfied.

s106
00:06:59.680 --> 00:07:01.440
Let's take another example.

s107
00:07:01.440 --> 00:07:07.360
What if you have code in Rust and you want to deductively verify with Lean or solvers?

s108
00:07:07.360 --> 00:07:10.960
Before we go there, let's quickly talk about this new term solvers.

s109
00:07:10.960 --> 00:07:17.960
So, remember we spoke of Lean being this chessboard interactive where you're making a bunch of moves trying to checkmate.

s110
00:07:17.960 --> 00:07:21.720
A solver is a calculator, a very powerful one.

s111
00:07:21.720 --> 00:07:25.360
You feed in a formula and it returns an output.

s112
00:07:25.360 --> 00:07:29.440
In this case, satisfiable or unsatisfiable.

s113
00:07:30.919 --> 00:07:35.200
So, an example of this is Verus, also an open-source tool.

s114
00:07:35.200 --> 00:07:39.560
It uses this solver, this very powerful calculator, Z3.

s115
00:07:39.560 --> 00:07:47.840
And if folks are familiar with adding annotations, it's kind of similar to that where you can add specifications in the form of that.

s116
00:07:47.840 --> 00:07:50.120
And the code is in line.

s117
00:07:50.120 --> 00:07:56.640
So, you see these two requires and ensure keywords, that's what we call a pre and post condition.

s118
00:07:56.640 --> 00:08:01.040
What must be true before and what must be true after.

s119
00:08:01.240 --> 00:08:02.720
And this is a static check.

s120
00:08:02.720 --> 00:08:05.440
It's enforced by the verifier and erased at runtime.

s121
00:08:05.440 --> 00:08:08.640
So, almost like ghost code.

s122
00:08:09.480 --> 00:08:18.760
Another example of this is Eneus, which uses the mid-level intermediate representation for Rust and does a functional translation to Lean.

s123
00:08:18.760 --> 00:08:24.320
And right after that, you use the same theorem prover, the same chessboard that we spoke of.

s124
00:08:26.240 --> 00:08:32.159
Now, you may be asking, well, what if I have any programming language?

s125
00:08:32.159 --> 00:08:37.320
We at AWS have been working on an open-source tool called Strata.

s126
00:08:37.320 --> 00:08:46.160
This 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.

s127
00:08:46.160 --> 00:08:47.760
Think of this like a compiler.

s128
00:08:47.760 --> 00:08:55.760
You have a high-level intermediate representation and you lower it down to a low-level intermediate representation, which is what Strata core is.

s129
00:08:55.760 --> 00:08:58.080
Now, this is written in Lean.

s130
00:08:58.080 --> 00:09:05.720
After 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.

s131
00:09:05.720 --> 00:09:14.600
For example, the Lean proof, remember the chessboard, or the very powerful calculator, SMT solvers, or model checkers.

s132
00:09:17.560 --> 00:09:19.760
So, you can get started with this today.

s133
00:09:19.760 --> 00:09:29.480
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,

s134
00:09:29.480 --> 00:09:37.120
which is very important, and then you can let your coding agent implement it and your formal verification tool prove it.

s135
00:09:38.560 --> 00:09:46.400
So, hopefully in this brave new world, we have software and systems that are not probably correct, but probably correct.

s136
00:09:46.400 --> 00:09:48.600
Thank you.

s137
00:10:01.951 --> 00:10:03.951
[music]