The Proof Must Go On: Formal Methods in the Theater of Secure Software Development(…)
summary
Predicts full-stack proof frontends within a decade that combine binary and high-level proofs, and widespread minimal verified components that become pluggable building blocks; expects a verified C standard library in 10–15 years via compiler flags that auto-swap safe modules into billions of devices; proposes corporate consortium (Google, Intel, AMD, Nvidia, TSMC) funding hardware specs; and hypothesizes a loop‑invariant discovery ~30 years out that makes deep verification automatic enough to embed into CI and sharply reduce large-scale cybercrime.
AI-written summary · about
chapters (19)
- 0:00Formal methods introduction
- 2:15Defining trust in software
- 5:49What are formal methods
- 8:18Historical roots of formal methods
- 10:50Industry adoption drivers
- 13:38Software crisis solutions
- 16:53Cold War secure languages
- 17:58Program analysis evolution
- 20:23Cyber crime pressure adoption
- 23:52Academic-government-industry cycle
- 31:16Next 30 years of formal methods
- 33:47Top-down vs bottom-up verification
- 36:37Full stack proof frontends
- 38:04Minimal verified components
- 40:36AI and hardware verification challenges
- 41:41Hardware specs and corporate collaboration
- 44:07Education reform mandates
- 45:12Loop invariant discoveries
- 46:59Summary and closing
related talks
01h 04mSoftware Verification meets Real-World Cryptography
01h 00mKeynote: Bringing Verified Cryptographic Protocols to Practice
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
18mState Proofs and Transaction Verification
01h 17mProof-Carrying Code For the Age of AI: Machine-Checked Guarantees from(…)
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
33mApplicable and Achievable Formal Verification
01h 25mIntroduction to Verifiable Computing