Speaker unverified: commitment

Transcript context

…... strengthened the proof. So now we've gone from, uh, a v- we, we had what was a valid conclusion. We still have the same conclusion, but we didn't realize that we were holding that conclusion for less than fully solid reasons, and now we feel that we do have fully solid reasons. Is that right? The latter. The latter. It's something that we call assumption accounting, so you're almost like an accountant, like looking at, like, how that thing is built. And generally, you would hope that every single sort of logical premise that your result is dependent on has been checked, or even better, has been stated. I think in this case, and during the other formalization process, while the result is safe and sound, there is an implicit assumption that was sort of never made explicit, and you actually need to do quite a lot of mathematical work to make that explicit. So in a way, we, we caught that issue and then we patch it. So people thought, think about verification as something that's like a, sort of like a stamp for perfection, right? There's actually huge amount of value in just, like, bug hunting. Uh, you're able to basically figure out, like, what is a counterexample, and then you can even try to patch it or, or you can try to do other modifications to, to the proof. And that actually has, the flip side of that, I think, has a lot of commercial value. Specifically, you can imagine finding counterexamples which result in bugs in hardware. Uh, this will be something that, uh, is quite interesting to various hardware designers. Uh, we're working with some, uh, early design partners on that. There are also, for example, the same sort of dynamic happening in software. If you're able to identify, uh, you know, bugs in large code bases and you're able to prove, uh, or patch the bug, and if you're, for example, in the smart contract setting, uh, there are bug bounties. People have awarded lots of money. Uh, not saying that we will go and pursue those, but people in the kind of smart contract space are generally very keen on the idea of using, um, a certain prover-based software verification system to try to figure out whether they can verify smart contracts, and specifically ca- catch bugs in this contract. Because what, what happens of each, each pretty big notorious bug is people lose money. Real money's being put in. Mm-hmm.…

Stored transcript either side of the excerpt. The highlighted words are the published quote; the surrounding text is unedited source, never generated.