Here I’ll talk about a type of TLA⁺ contract I’ve worked on a few times, and why it didn’t work out as well as hoped. I’m not trying to torpedo other peoples’ contracts here - I just hope to share this experience so others can structure their TLA⁺ contracts differently, hopefully leading to greater success for both parties and industry usage of TLA⁺ as a whole. The proposal The contract proposal goes like this: a client wants to build a distributed system, and has read that TLA⁺ is effective at modeling such things. Conventional wisdom holds that it’s always cheaper to catch bugs earlier in the development pipeline, and what’s earlier than the design stage? However, they don’t have any in-house TLA⁺ knowledge and are unsure about whether they want to invest in training or hiring. Instead, they email me a proposal: could I do a short 1-3 month contract where I specify their system in TLA⁺ for them? The benefits of this setup are generally reasoned as follows: