I can't wait to show this to my manager next time he asks why it's taking three weeks to build a simple CRUD app.

"Look, if this guys TLA+ logic struggles to model a 1,500-year-old game without crying over a French pawn-capture rule, you can't expect me to integrate Stripe billing without a few state invariant violations."

Payments have a gargantuan amount of possible transitions and invariants that are far from trivial to encode.