上周在 OOPSALA '25 上，我们的 Act 开发者展示了 CheckMate 的改进版，这是一个用于正式验证区块链协议博弈论安全性的自动证明器。 简而言之：该工具检查协议中的激励是否使作弊不值得。

协议需要三种安全性： • 加密：你的密钥/密码强吗？ • 实现：代码中是否有漏洞？ • 博弈论：激励是否一致，以至于作弊没有好处？ 最后一点至关重要，但常常被忽视。

博弈论安全性是确保即使是理性、自私的参与者也更倾向于遵循规则——因为偏离规则的成本高于收益。 这就是安全性的“经济学”。

CheckMate 正式且自动地使用 SMT 求解器证明博弈论安全性。本文介绍了一种组合的“分而治之”算法，能够扩展到数百万个节点，交错进行模型生成和分析以提高效率。

这为什么重要： 我们现在可以自动、正式并大规模地证明区块链协议的激励机制使得作弊变得不理性——在部署之前。