本文提出 CheckMate 框架，用于全自动化的博弈论安全分析，特别关注区块链技术。CheckMate 将协议建模为博弈，并分析其博弈论安全性，即激励兼容性和拜占庭容错性。该框架要么通过提供防御策略证明协议是安全的，要么给出所有可能的攻击向量。对于不安全的协议，CheckMate 还能在存在的情况下给出使协议变得安全的最弱前置条件。CheckMate 实现了博弈论安全在一阶线性实数算术中的可靠且完备编码，从而将安全分析归约为可满足性求解。此外，CheckMate 还自动化了算术项上高效的分情况处理。实验表明，CheckMate 具有良好的可扩展性，能够分析包含数万亿策略的博弈，这些博弈对比特币闪电网络的阶段进行了建模。该研究的核心贡献在于将博弈论安全推理转化为自动化的求解问题，为区块链协议的安全验证提供了一种新的形式化方法。适合对形式化验证、区块链安全、博弈论应用感兴趣的研究者和安全工程师阅读。