Ask Me Anything with Byron Cook
summary
Amazon shows how formal methods move from prototype to production: teams prove the KMS protocol, verify an in‑house TLS stack called s2 and ship a service that uses Zelkova and Access Analyzer to catch misconfigured IAM and network policies. Engineering uses tools that work out of the box (Soufflé, CBMC/CMC, VCC, SMT solvers) while eight developers write and verify Daphne proofs on production code. Roadmaps include distributed SMT/model‑checking across thousands of machines for linear speedups.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 1:30How did you succeed at Amazon
- 4:56How hard was it to convince engineers to use formal methods
- 8:14How do you see the formal methods space
- 12:28How are you using these tools
- 14:24Do we have tools now
- 18:35More and more features are moved to configuration
- 21:51What research problems excite you
- 22:46What are you working on now
- 26:15Why did you choose industry over academia
- 28:14Why did you join Microsoft
- 31:10Past research
- 33:36Worklife balance
- 36:51Wish for the community
related talks
57mResearch on Different Time Horizons (and an Example with Machine-Checked Proofs)
21mMassive proofs for the masses
59mProving the correctness of AWS authorization
59mProvably secure authorization
46mVerifying code using automated reasoning
12mTool Talk: KLEE
56mProof Assistants At the Hardware-Software Interface
16mThe Morello ISA semantics, proof, and test generation