主要观点：作者分享了曾参与的 TLA⁺ 合同经历，合同旨在为客户用 TLA⁺ 规范分布式系统设计，但最终效果未达预期，作者反思此经历并探讨更成功的方式。
关键信息：

• 合同提议：客户希望用 TLA⁺ 审计系统设计，因无内部知识而委托作者短期合同完成，好处包括早期发现问题等。
• 合同执行：作者与团队交流，经历 TLA⁺ 规范过程的起伏，每周会议讨论有价值，但团队对规范理解逐渐不足。
• 问题出现：随着规范复杂度增加，团队热情下降，对作者解释不满，开始更看重规范过程而非最终成果。
• 事后反思：作者认为自己虽完成合同，但所写规范可能不再被看，忽略了思考的重要性，像健身房的叉车只搬运重物。
• 替代方案：Hillel Wayne 建议与团队成员结对编程 TLA⁺ 规范，需客户投入内部时间，否则可能影响 TLA⁺ 行业声誉。
  重要细节：
• 作者接受合同是因擅长且短期报酬高，与团队有多次交流和更新。
• 团队对复杂 TLA⁺ 规范感到困惑，与作者在理解上有差异。
• 作者在 [Antithesis Bug Bash] 看到相关演讲后有深刻感悟。
• 作者表示若再接到此类合同会认真思考使其成功的因素。