Summary
Engineers at AWS adopted TLA+ (a formal specification language by Leslie Lamport) to specify and model-check designs for DynamoDB, S3, EBS, and internal lock managers. They found real bugs — including subtle edge cases in replication protocols that testing had missed. Critically, the engineers were not formal methods specialists; they learned TLA+ on the job and found it practical enough to use on production systems under deadline pressure.
What it means for our work
This is the closest precedent for what we’re building. AWS proved that working engineers — not academics — can use formal specification to find real bugs in real systems. The gap they identified (the learning curve of the notation and tooling) is exactly what Z Spec aims to close. If AWS engineers could learn TLA+ and get value, we believe Claude can make Z equally accessible — handling the notation while the engineer focuses on what the system should do.