TLA+入门：从基本原理出发 (buttondown.com)

本文介绍了TLA+的基础数学原理，以及如何用其进行系统建模。文章以银行账户转账为例，逐步讲解如何使用谓词逻辑、时间变量、状态转换等概念描述系统行为。并引入了时间逻辑、Stutter步骤、不变式等关键概念，最终用TLA+语言表达了转账模型和无透支属性。文章还讨论了如何简化模型以提高可验证性，并鼓励读者思考如何扩展模型以支持双向转账。