Project Everest: Perspectives from Developing Industrial-Grade High-Assurance(…)
summary
Project Everest produces a verified TLS stack and crypto suite rather than promises: it yields 1.3 million lines of F source that build in two hours, emits EverCrypt/HACL/Vale crypto deployed in Firefox, Python, Windows and Azure, and discharges roughly 66,000 SMT queries for ~600,000 proof obligations. It supplies Low*, Vale, EverParse, Caramel transpiler, and Pulse/Steel logics; most components run in production, some handshakes remain unproved but a two‑week agent produced a 120k‑line Pulse handshake proof prototype.
AI-written summary · about
chapters (13)
- 0:00Project Everest intro
- 3:56Verified TLS stack overview
- 5:19Everest’s design principles
- 6:44Co-developing tools and apps
- 10:36Verified crypto algorithms
- 12:21Attack surface hardening with EverParse
- 13:43Verified TLS implementations
- 14:47Language and app co-design
- 16:30High-assurance cost effectiveness
- 17:11AI-assisted verification breakthrough
- 19:16Agentic program verification takeaways
- 20:41Future of verification tools
- 22:48Call to action
related talks
01h 04mSoftware Verification meets Real-World Cryptography
01h 00mKeynote: Bringing Verified Cryptographic Protocols to Practice
29mVale: Verifying High-Performance Cryptographic Assembly Code
39mKeynote: Towards High-Assurance Cryptographic Software
41mFormally Verifying Everybody's Cryptography
47mHigh-Assurance Go Cryptography
50mTurbo Eureka
01h 19mCrashing Drones and Hijacked Cameras: CyberTrust Meets CyberPhysical