使用 TLA+ 模型清除错误

August 18, 2023 · 4 min read

ICP Community Member

DFINITY基金会很快就会开始开发一些工具，将 TLA+ 模型链接到实际的 Rust 代码，以解决随着代码随时间修改而出现的模型和代码发散的问题

我们很快就会开始开发一些工具，将 TLA+ 模型链接到实际的 Rust 代码，以解决随着代码随时间修改而出现的模型和代码发散的问题，当然，这些工具一旦投入生产也将立即开源，敬请期待！

今年早些时候，我们强调了将 TLA+ 应用到互联网计算机上的容器智能合约的好处。

TLDR：

1) 直接金钱损失的可能性使得安全性和正确性对于智能合约至关重要；

2) TLA+ 等正式方法总体上提高了系统的正确性和安全性；

3) TLA+ 特别擅长淘汰容器中出现一类非常常见的错误，称为重入错误。

经过一些清理工作后，我们很高兴地宣布我们刚刚开源了所有 TLA+ 模型，您将在 GitHub 上找到以下容器的模型：

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

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

由于 TLA+ 是一种通用建模语言，并非特定于容器，因此我们还将其应用于部分底层互联网计算机堆栈，例如，TLA+ 帮助确保互联网计算机能够顺利迁移互联网身份容器。

TLA+ 首先在迁移设计的早期版本中检测到极端情况，这些情况可能导致互联网身份客户端容器无法干净升级，随后帮助验证修复，该存储库还包括以下模型：

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

就是这样！我们希望您发现这些资源有用，我们期待看到针对社区创建的容器和 dapp 的新 TLA+ 模型，如果您创建了一些，请务必在开发者论坛中让更广泛的 ICP 社区了解。

接下来，我们很快就会开始开发一些工具，将 TLA+ 模型链接到实际的 Rust 代码，以解决随着代码随时间修改而出现的模型和代码发散的问题，当然，这些工具一旦投入生产也将立即开源，敬请期待！

查看技术教程

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