Catching design bugs before code: formal models in Alloy
· 10 min read
Most of our nastiest bugs were never typos. They were a state machine that looked right in the PR, passed its tests, and then met a customer doing something perfectly reasonable that nobody had drawn on the whiteboard. A Playground stuck in an error state forever. A chat that vanished because a healthcheck flapped. A runtime launched on a Marquee that hadn't been funded.
So we started writing down the hard lifecycles in Alloy, a relational modeling language, and letting a solver do the part humans are worst at: trying every small, weird combination of states and asking "does your invariant actually hold here?" Often it doesn't — and the solver tells us exactly which world breaks it.