[
  {
    "startMs": 1309,
    "text": "[music]"
  },
  {
    "startMs": 12880,
    "text": ">> Coding agents are generating more code"
  },
  {
    "startMs": 15040,
    "text": "than ever."
  },
  {
    "startMs": 16360,
    "text": "Builders are generating hundreds and"
  },
  {
    "startMs": 18680,
    "text": "thousands of PRs every week."
  },
  {
    "startMs": 21360,
    "text": "How do you know that this is correct?"
  },
  {
    "startMs": 24720,
    "text": "Using LM as a judge for the code? Well,"
  },
  {
    "startMs": 26920,
    "text": "that's probabilistic."
  },
  {
    "startMs": 29120,
    "text": "Tests?"
  },
  {
    "startMs": 30320,
    "text": "They only check some inputs, not all."
  },
  {
    "startMs": 33480,
    "text": "Human code review doesn't scale to match"
  },
  {
    "startMs": 35640,
    "text": "agent speed."
  },
  {
    "startMs": 37680,
    "text": "None of these can say for all inputs the"
  },
  {
    "startMs": 40240,
    "text": "code is correct."
  },
  {
    "startMs": 42320,
    "text": "Formal verification can."
  },
  {
    "startMs": 44560,
    "text": "Hi, I'm Varun Pant. I build AI products"
  },
  {
    "startMs": 46800,
    "text": "at AWS leading teams at in formal"
  },
  {
    "startMs": 49320,
    "text": "verification."
  },
  {
    "startMs": 51360,
    "text": "Formal verification provides"
  },
  {
    "startMs": 53240,
    "text": "mathematical proof that code is correct."
  },
  {
    "startMs": 56040,
    "text": "For all inputs."
  },
  {
    "startMs": 57720,
    "text": "You write what correct means, which is"
  },
  {
    "startMs": 59480,
    "text": "the specification, and a formal"
  },
  {
    "startMs": 61760,
    "text": "verification tool proves that your code"
  },
  {
    "startMs": 64080,
    "text": "satisfies it."
  },
  {
    "startMs": 65840,
    "text": "If the proof passes, it holds for every"
  },
  {
    "startMs": 68400,
    "text": "possible input."
  },
  {
    "startMs": 71920,
    "text": "How do you use this?"
  },
  {
    "startMs": 73920,
    "text": "Well, one way is back driven"
  },
  {
    "startMs": 75400,
    "text": "development, for example, with Kiro."
  },
  {
    "startMs": 79200,
    "text": "You write what the specification is,"
  },
  {
    "startMs": 81320,
    "text": "which is what correct means."
  },
  {
    "startMs": 83280,
    "text": "Either you write it formally, for"
  },
  {
    "startMs": 85160,
    "text": "example, directly in Lean, or you write"
  },
  {
    "startMs": 87560,
    "text": "it in natural language, and you let the"
  },
  {
    "startMs": 89360,
    "text": "AI auto formalize it."
  },
  {
    "startMs": 92360,
    "text": "Now, this is really important. You then"
  },
  {
    "startMs": 94320,
    "text": "validate the specification. So, either"
  },
  {
    "startMs": 96800,
    "text": "the human reviews it, or you test that"
  },
  {
    "startMs": 99440,
    "text": "it holds on some inputs. And this is"
  },
  {
    "startMs": 101480,
    "text": "important because the specification is"
  },
  {
    "startMs": 103360,
    "text": "upstream. It's a living, breathing"
  },
  {
    "startMs": 105080,
    "text": "artifact that the builder interacts"
  },
  {
    "startMs": 107080,
    "text": "with. You want this to be correct."
  },
  {
    "startMs": 109400,
    "text": "Everything else is downstream from this."
  },
  {
    "startMs": 112920,
    "text": "The AI coding agent then goes and"
  },
  {
    "startMs": 114520,
    "text": "implements from the specification."
  },
  {
    "startMs": 117640,
    "text": "And the formal verification tool proves"
  },
  {
    "startMs": 120120,
    "text": "that the implementation matches the"
  },
  {
    "startMs": 121960,
    "text": "specification."
  },
  {
    "startMs": 124680,
    "text": "So, humans own the specification and"
  },
  {
    "startMs": 126760,
    "text": "machines own the code and proof."
  },
  {
    "startMs": 130840,
    "text": "Lean is a programming language and a"
  },
  {
    "startMs": 132680,
    "text": "proof assistant."
  },
  {
    "startMs": 134360,
    "text": "It is the same language for the"
  },
  {
    "startMs": 136640,
    "text": "definitions and proofs. There's no"
  },
  {
    "startMs": 138600,
    "text": "translation layer."
  },
  {
    "startMs": 140480,
    "text": "It is implemented in Lean, which means"
  },
  {
    "startMs": 142480,
    "text": "it's very extensible. And this is"
  },
  {
    "startMs": 144320,
    "text": "important. It has a small trusted"
  },
  {
    "startMs": 146200,
    "text": "kernel."
  },
  {
    "startMs": 147400,
    "text": "Proofs can be exported and independently"
  },
  {
    "startMs": 149680,
    "text": "checked."
  },
  {
    "startMs": 153520,
    "text": "So, here's an example of a Lean file"
  },
  {
    "startMs": 156280,
    "text": "which has both the code and proof in the"
  },
  {
    "startMs": 158160,
    "text": "same language. At the top, you'll see"
  },
  {
    "startMs": 160720,
    "text": "the code, which is a function that"
  },
  {
    "startMs": 162720,
    "text": "reverses a list in Lean. So, reverse of"
  },
  {
    "startMs": 165080,
    "text": "one, two, and three gives three, two,"
  },
  {
    "startMs": 166720,
    "text": "and one."
  },
  {
    "startMs": 167920,
    "text": "And right in the middle, you'll see a"
  },
  {
    "startMs": 169840,
    "text": "theorem. This is the proof."
  },
  {
    "startMs": 172920,
    "text": "And this theorem prover approves a"
  },
  {
    "startMs": 175480,
    "text": "property which says that reverse of A"
  },
  {
    "startMs": 177320,
    "text": "plus B is in fact reverse of B plus"
  },
  {
    "startMs": 179560,
    "text": "reverse of A."
  },
  {
    "startMs": 180920,
    "text": "And this holds for every possible input."
  },
  {
    "startMs": 184280,
    "text": "How do you do this? You have something"
  },
  {
    "startMs": 186040,
    "text": "called as tactics which do the work,"
  },
  {
    "startMs": 187840,
    "text": "which we'll get to in a second. And the"
  },
  {
    "startMs": 189640,
    "text": "kernel, remember the small trusted"
  },
  {
    "startMs": 191400,
    "text": "kernel?"
  },
  {
    "startMs": 192360,
    "text": "That checks the work."
  },
  {
    "startMs": 196200,
    "text": "A good analogy to understand the Lean"
  },
  {
    "startMs": 197959,
    "text": "proof assistant is that of chess. So, in"
  },
  {
    "startMs": 200400,
    "text": "chess, your goal is to checkmate the"
  },
  {
    "startMs": 202280,
    "text": "opponent. And you make a bunch of moves."
  },
  {
    "startMs": 204800,
    "text": "You move the knight, you move the"
  },
  {
    "startMs": 206440,
    "text": "bishop."
  },
  {
    "startMs": 207600,
    "text": "Similarly, in Lean, you have a bunch of"
  },
  {
    "startMs": 210519,
    "text": "tactics which are your moves. And it's"
  },
  {
    "startMs": 213800,
    "text": "the same chess board. It's interactive."
  },
  {
    "startMs": 216040,
    "text": "You want to prove the goal, the theorem,"
  },
  {
    "startMs": 218880,
    "text": "checkmate. And you're kind of going down"
  },
  {
    "startMs": 221440,
    "text": "a tree. So, you're traversing the tree,"
  },
  {
    "startMs": 223440,
    "text": "you're trying different tactics. Maybe"
  },
  {
    "startMs": 225320,
    "text": "for some goals, you're not able to prove"
  },
  {
    "startMs": 227239,
    "text": "it, so you backtrack and then you try"
  },
  {
    "startMs": 229280,
    "text": "another a branch of the tree. Very"
  },
  {
    "startMs": 231519,
    "text": "similar to chess."
  },
  {
    "startMs": 233880,
    "text": "And finally, you get a goal that"
  },
  {
    "startMs": 235920,
    "text": "hopefully proves the theorem, and then"
  },
  {
    "startMs": 237960,
    "text": "that small independent kernel confirms"
  },
  {
    "startMs": 240120,
    "text": "and checks it."
  },
  {
    "startMs": 243520,
    "text": "The kernel catches the mistake. So,"
  },
  {
    "startMs": 245640,
    "text": "here's an example at the top where an"
  },
  {
    "startMs": 247800,
    "text": "incor- incorrect proof is rejected"
  },
  {
    "startMs": 250040,
    "text": "immediately. And you only need to trust"
  },
  {
    "startMs": 252520,
    "text": "the small kernel."
  },
  {
    "startMs": 254680,
    "text": "The good thing is that you can have"
  },
  {
    "startMs": 256000,
    "text": "multiple independent kernels. You"
  },
  {
    "startMs": 257480,
    "text": "yourself can actually go write one. It's"
  },
  {
    "startMs": 259239,
    "text": "completely open source. You have kernels"
  },
  {
    "startMs": 261359,
    "text": "in C++, Rust, Lean. That's uh a link to"
  },
  {
    "startMs": 265160,
    "text": "the Arena Lang where you can go and add"
  },
  {
    "startMs": 268320,
    "text": "a kernel."
  },
  {
    "startMs": 270680,
    "text": "So, let's look at some examples where"
  },
  {
    "startMs": 272880,
    "text": "you can put this to practice. The first"
  },
  {
    "startMs": 275600,
    "text": "one is having the specification and code"
  },
  {
    "startMs": 278680,
    "text": "both being in Lean."
  },
  {
    "startMs": 281760,
    "text": "Now, this is open source Andreo. AI"
  },
  {
    "startMs": 284320,
    "text": "converted zlib, which is a C compression"
  },
  {
    "startMs": 286400,
    "text": "library, to Lean. Now, granted this"
  },
  {
    "startMs": 288520,
    "text": "happened over a week or so."
  },
  {
    "startMs": 292720,
    "text": "But, kind of going back to our"
  },
  {
    "startMs": 294680,
    "text": "specification methodology that we"
  },
  {
    "startMs": 297080,
    "text": "mentioned where you had specification at"
  },
  {
    "startMs": 298880,
    "text": "the top and then verification for the"
  },
  {
    "startMs": 300720,
    "text": "code, we'll kind of see the same thing"
  },
  {
    "startMs": 302880,
    "text": "here. So, the natural language"
  },
  {
    "startMs": 304480,
    "text": "specification says that you decompress"
  },
  {
    "startMs": 306880,
    "text": "the output"
  },
  {
    "startMs": 308200,
    "text": "of compress returning the original data."
  },
  {
    "startMs": 311000,
    "text": "And then, you have an AI that generates"
  },
  {
    "startMs": 313680,
    "text": "the formal spec. Now, remember this is"
  },
  {
    "startMs": 315200,
    "text": "important. Checking the specification is"
  },
  {
    "startMs": 317600,
    "text": "key."
  },
  {
    "startMs": 319080,
    "text": "After you do that, the AI goes and"
  },
  {
    "startMs": 321320,
    "text": "writes your code in Lean, and then"
  },
  {
    "startMs": 323400,
    "text": "generates these helper lemma subgoals,"
  },
  {
    "startMs": 326160,
    "text": "and proves the theorem."
  },
  {
    "startMs": 328760,
    "text": "And at the bottom, you can see that it's"
  },
  {
    "startMs": 330480,
    "text": "verified with that small independent"
  },
  {
    "startMs": 332400,
    "text": "kernel."
  },
  {
    "startMs": 334480,
    "text": "So, what you just saw was that AI"
  },
  {
    "startMs": 336200,
    "text": "decomposed the problem into lemmas,"
  },
  {
    "startMs": 338200,
    "text": "which are subgoals. It proved each of"
  },
  {
    "startMs": 340360,
    "text": "them using tactics. Remember the chess"
  },
  {
    "startMs": 342960,
    "text": "moves that we were making?"
  },
  {
    "startMs": 344640,
    "text": "And it assembled it into a final"
  },
  {
    "startMs": 346480,
    "text": "theorem."
  },
  {
    "startMs": 347760,
    "text": "Checkmate."
  },
  {
    "startMs": 349080,
    "text": "And the kernel checked it."
  },
  {
    "startMs": 351440,
    "text": "And this particular example had 32,000"
  },
  {
    "startMs": 354000,
    "text": "lines of proof. So, it was"
  },
  {
    "startMs": 355800,
    "text": "pretty big."
  },
  {
    "startMs": 358840,
    "text": "Let's take another example. What if you"
  },
  {
    "startMs": 360320,
    "text": "have code in Rust? Well, you can write"
  },
  {
    "startMs": 362280,
    "text": "the functional specification of it or"
  },
  {
    "startMs": 364080,
    "text": "the model in Lean."
  },
  {
    "startMs": 366720,
    "text": "An example of that is Cedar."
  },
  {
    "startMs": 368720,
    "text": "Cedar is an open-source authorization"
  },
  {
    "startMs": 371000,
    "text": "policy language, which is used by AWS"
  },
  {
    "startMs": 373240,
    "text": "verified permissions and access."
  },
  {
    "startMs": 375880,
    "text": "The specification of Cedar is written in"
  },
  {
    "startMs": 378400,
    "text": "Lean. The production code runs in Rust."
  },
  {
    "startMs": 382320,
    "text": "Why is this important? Because"
  },
  {
    "startMs": 384360,
    "text": "let's take an example. You have forbid"
  },
  {
    "startMs": 386560,
    "text": "Trump's permit. You want to make sure"
  },
  {
    "startMs": 388600,
    "text": "that for any forbid policy being"
  },
  {
    "startMs": 390400,
    "text": "satisfied, the request is always denied."
  },
  {
    "startMs": 392800,
    "text": "This is key."
  },
  {
    "startMs": 396320,
    "text": "Here you can see the example of what I"
  },
  {
    "startMs": 397680,
    "text": "was talking about, which is you have the"
  },
  {
    "startMs": 399800,
    "text": "Rust production code and you have the"
  },
  {
    "startMs": 401560,
    "text": "functional specification in Lean, and"
  },
  {
    "startMs": 403720,
    "text": "you run differential random testing to"
  },
  {
    "startMs": 405840,
    "text": "check that both of those for the same"
  },
  {
    "startMs": 407520,
    "text": "inputs give the same output."
  },
  {
    "startMs": 410120,
    "text": "And there's about 100 million"
  },
  {
    "startMs": 411120,
    "text": "differential random tests uh run"
  },
  {
    "startMs": 413080,
    "text": "nightly."
  },
  {
    "startMs": 414960,
    "text": "No version ships until this is"
  },
  {
    "startMs": 416520,
    "text": "satisfied."
  },
  {
    "startMs": 419680,
    "text": "Let's take another example. What if you"
  },
  {
    "startMs": 421800,
    "text": "have code in Rust and you want to"
  },
  {
    "startMs": 423480,
    "text": "deductively verify with Lean or solvers?"
  },
  {
    "startMs": 427360,
    "text": "Before we go there, let's quickly talk"
  },
  {
    "startMs": 429000,
    "text": "about this new term solvers. So,"
  },
  {
    "startMs": 431080,
    "text": "remember we spoke of Lean being this"
  },
  {
    "startMs": 433160,
    "text": "chessboard interactive where you're"
  },
  {
    "startMs": 435080,
    "text": "making a bunch of moves trying to"
  },
  {
    "startMs": 436640,
    "text": "checkmate."
  },
  {
    "startMs": 437960,
    "text": "A solver is a calculator, a very"
  },
  {
    "startMs": 440600,
    "text": "powerful one. You feed in a formula and"
  },
  {
    "startMs": 443960,
    "text": "it returns an output. In this case,"
  },
  {
    "startMs": 446400,
    "text": "satisfiable or unsatisfiable."
  },
  {
    "startMs": 450919,
    "text": "So, an example of this is Verus, also an"
  },
  {
    "startMs": 453600,
    "text": "open-source tool."
  },
  {
    "startMs": 455200,
    "text": "It uses this solver, this very powerful"
  },
  {
    "startMs": 457400,
    "text": "calculator, Z3."
  },
  {
    "startMs": 459560,
    "text": "And if folks are familiar with adding"
  },
  {
    "startMs": 462480,
    "text": "annotations, it's kind of similar to"
  },
  {
    "startMs": 463920,
    "text": "that where you can add specifications in"
  },
  {
    "startMs": 466560,
    "text": "the form of that. And the code is in"
  },
  {
    "startMs": 469720,
    "text": "line. So, you see these two requires and"
  },
  {
    "startMs": 472240,
    "text": "ensure keywords, that's what we call a"
  },
  {
    "startMs": 474840,
    "text": "pre and post condition. What must be"
  },
  {
    "startMs": 477160,
    "text": "true before and what must be true after."
  },
  {
    "startMs": 481240,
    "text": "And this is a static check. It's"
  },
  {
    "startMs": 482880,
    "text": "enforced by the verifier and erased at"
  },
  {
    "startMs": 485000,
    "text": "runtime. So, almost like ghost code."
  },
  {
    "startMs": 489480,
    "text": "Another example of this is Eneus,"
  },
  {
    "startMs": 492560,
    "text": "which uses the mid-level intermediate"
  },
  {
    "startMs": 494720,
    "text": "representation for Rust and does a"
  },
  {
    "startMs": 496840,
    "text": "functional translation to Lean. And"
  },
  {
    "startMs": 498880,
    "text": "right after that, you use the same"
  },
  {
    "startMs": 500280,
    "text": "theorem prover, the same chessboard that"
  },
  {
    "startMs": 501919,
    "text": "we spoke of."
  },
  {
    "startMs": 506240,
    "text": "Now, you may be asking, well, what if I"
  },
  {
    "startMs": 508919,
    "text": "have any programming language?"
  },
  {
    "startMs": 512159,
    "text": "We at AWS have been working on an"
  },
  {
    "startMs": 514560,
    "text": "open-source tool called Strata. This is"
  },
  {
    "startMs": 517640,
    "text": "work in progress, but the idea is that"
  },
  {
    "startMs": 520840,
    "text": "you can have any programming language"
  },
  {
    "startMs": 522840,
    "text": "and you yourself can create what we call"
  },
  {
    "startMs": 524720,
    "text": "a dialect."
  },
  {
    "startMs": 526160,
    "text": "Think of this like a compiler. You have"
  },
  {
    "startMs": 528280,
    "text": "a high-level intermediate representation"
  },
  {
    "startMs": 530240,
    "text": "and you lower it down to a low-level"
  },
  {
    "startMs": 531960,
    "text": "intermediate representation, which is"
  },
  {
    "startMs": 533920,
    "text": "what Strata core is. Now, this is"
  },
  {
    "startMs": 536280,
    "text": "written in Lean."
  },
  {
    "startMs": 538080,
    "text": "After you have all of these programs"
  },
  {
    "startMs": 540600,
    "text": "talking in the same language, which is"
  },
  {
    "startMs": 542120,
    "text": "the Strata core, you can dispatch it to"
  },
  {
    "startMs": 544760,
    "text": "any of the engines. For example, the"
  },
  {
    "startMs": 546920,
    "text": "Lean proof, remember the chessboard, or"
  },
  {
    "startMs": 549280,
    "text": "the very powerful calculator, SMT"
  },
  {
    "startMs": 551240,
    "text": "solvers, or model checkers."
  },
  {
    "startMs": 557560,
    "text": "So, you can get started with this today."
  },
  {
    "startMs": 559760,
    "text": "You can go to Lean in in your browser"
  },
  {
    "startMs": 562480,
    "text": "with the link I pasted, and you can pick"
  },
  {
    "startMs": 565080,
    "text": "your most critical code,"
  },
  {
    "startMs": 567000,
    "text": "write what correct means, which is the"
  },
  {
    "startMs": 568520,
    "text": "specification, which is very important,"
  },
  {
    "startMs": 571120,
    "text": "and then you can let your coding agent"
  },
  {
    "startMs": 572800,
    "text": "implement it and your formal"
  },
  {
    "startMs": 574080,
    "text": "verification tool prove it."
  },
  {
    "startMs": 578560,
    "text": "So, hopefully in this brave new world,"
  },
  {
    "startMs": 581120,
    "text": "we have software and systems that are"
  },
  {
    "startMs": 583160,
    "text": "not probably correct, but probably"
  },
  {
    "startMs": 585640,
    "text": "correct. Thank you."
  },
  {
    "startMs": 601951,
    "text": ">> [music]"
  }
]