使用 TLA+ 模型清除错误

今年早些时候，我们强调了将 TLA+ 应用到互联网计算机上的容器智能合约的好处。
TLDR：
1) 直接金钱损失的可能性使得安全性和正确性对于智能合约至关重要；‍
2) TLA+ 等正式方法总体上提高了系统的正确性和安全性；‍
3) TLA+ 特别擅长淘汰容器中出现一类非常常见的错误，称为重入错误。
经过一些清理工作后，我们很高兴地宣布我们刚刚开源了所有 TLA+ 模型，您将在 GitHub 上找到以下容器的模型：

• NNS 和 SNS 治理（重点关注与账本容器的交互）
• ICP 账本（专注于区块归档）
• ckBTC 铸币器
• SNS 交换容器

我们希望这些模型为您提供现实生活中的示例，并帮助您创建自己的容器模型，此外，我们还分享了一个配套的深入技术教程来指导您完成此过程，本教程提供了如何在 TLA+ 中对容器的特性进行建模的一般策略：

• mynosefroze.com/blog/2023-08-09-tla_for_canisters

由于 TLA+ 是一种通用建模语言，并非特定于容器，因此我们还将其应用于部分底层互联网计算机堆栈，例如，TLA+ 帮助确保互联网计算机能够顺利迁移互联网身份容器。
TLA+ 首先在迁移设计的早期版本中检测到极端情况，这些情况可能导致互联网身份客户端容器无法干净升级，随后帮助验证修复，该存储库还包括以下模型：

• 人群聚会 dapp 的连接建立子协议
• 互联网计算机共识算法的安全特性
• 互联网身份迁移过程
• 子网分割过程

就是这样！我们希望您发现这些资源有用，我们期待看到针对社区创建的容器和 dapp 的新 TLA+ 模型，如果您创建了一些，请务必在开发者论坛中让更广泛的 ICP 社区了解。
接下来，我们很快就会开始开发一些工具，将 TLA+ 模型链接到实际的 Rust 代码，以解决随着代码随时间修改而出现的模型和代码发散的问题，当然，这些工具一旦投入生产也将立即开源，敬请期待！
获取 TLA+ 模型的开源代码

查看技术教程

了解有关互联网计算机的更多信息：internetcomputer.org，在 Twitter 上关注技术：@DFINITYDev，开始在互联网计算机上构建。

作者：Ognjen Maric翻译：Catherine

-    往  期  推  荐    -

你关心的 IC 内容

技术进展 | 项目信息 | 全球活动

长按关注 IC 微信公众号

掌握最新资讯

＊添加小助手微信 comiocn 进交流社群