Proofs in the Wild: What’s done today? What’s close? What’s far?
Date:
Proofs and other formal methods technologies are great, but the vast majority of systems deployed today are built without them. We’ve recently seen a few green shoots, for example in hardware, crypto, and big cloud providers. In my role as a PI at Galois, I’ve led a lot of commercial and government formal methods projects. This talk will look at three questions: how are proof technologies actually used in the wild today? What might be close to viability, for example with AI assistance? And what seems far off, even with AI?