ℹ️ Community wiki: share your company's use of refined/dependent types, effect systems, or linear types in prod. Please include language, team size, and outcome.

ℹ️ AWS found that engineers "more readily grasp the concept and practical value of TLA+" when it's framed as "exhaustively testable pseudo-code" — avoiding the word 'formal' entirely. Good ammo for your next team meeting.

ℹ️ Since 2011, engineers at AWS have used formal specification and model checking to help solve difficult design problems in critical systems. TLA+ helped AWS find subtle bugs in S3, DynamoDB, EBS, and an internal distributed lock manager, as well as verifying several optimizations.

ℹ️ CompCert is the first commercially available optimizing compiler that is formally verified, using machine-assisted mathematical proofs, to be free from miscompilation. The executable code it produces is proved to behave exactly as specified by the semantics of the source C program. The CompCert compiler was recently qualified for the MFC_NG of ATR 42/72 aircraft; for the first time, certification credits for compliance with DO-178C, DO-333, and DO-330 could be claimed for critical avionics software from compiler usage.

ℹ️ PracticalPurr spent 6 months sneaking Idris2 into a backend microservice team of 9. Full writeup with metrics. Spoilers: the type-level state machines were a hit; compile times were not.

ℹ️ Engineers from entry-level to principal have been able to learn TLA+ from scratch and get useful results in two to three weeks — that's your time-to-value argument right there.

ℹ️ Modeling a key commit protocol for the Aurora relational database engine in P and TLA+ allowed AWS to identify an opportunity to reduce the cost of distributed commits from 2 to 1.5 network roundtrips without sacrificing any safety properties.