Formal Specification and Taming Other People's Tech
summary
Formal specifications model a production email service with a small shared provider that uses Redis-backed token bucket rate limits and a retry queue. Model checking exposes that large user-triggered blasts — from hundreds to hundreds of thousands of messages — fill the retry queue, cause long delays and midnight pages, and risk deleting legitimate verification emails. Specs drive design changes: per-email-type buckets, an HTTP publisher front end, and a deletion policy; the models find concrete unsafe states and guide fixes that work in production.
AI-written summary · about
chapters (7)
- 0:00Introduction to formal specs
- 5:05Real-world use case
- 9:57Specifying the email service
- 17:20Impossible vs undesirable states
- 22:40Challenges with loops
- 27:41Practical tips for specs
- 30:08Q&A and closing
related talks
47mA Deep Specification for Dropbox
46mKeynote: Formal Verification? No, Formal Reasoning!
46mDesign for errors - An introduction to Domain Modeling with a bit of Arrow
23mStop Making LLMs Deterministic: A Spec-Driven Software Factory
34mDistributed Systems - What Can Go Wrong and How to Get It Right
22mThe New Code
40mEverything Will Flow
40mFour Diseases