Latest / Deep End Era. Engineering with Sankalp
The Thirty Five Step Bug: Formal Methods in Industry
Fictional payments engineer Ottilie Brandt is paged at 3 a.m. for a replication bug that should be impossible. With her colleague Benedikt Achebe she brings formal methods into her company. We cover safety and liveness properties, a worked race-condition example, TLA+ and the TLC model checker, state explosion and the small-scope hypothesis, Amazon's 2015 CACM paper and its 35-step DynamoDB bug, theorem proving and the seL4 microkernel proof, SAT/SMT solvers, Zelkova and Infer, verified compilers, Alloy, P, Raft, Rust tools, verified cryptography, railway and avionics use, the limits, and…
The skinny
The skinny isn't ready yet — notes appear once the transcript is processed.