主要观点：作者发表了两篇关于利用模型检查器验证容错分布式算法属性的技术论文，强调应采用多种工具提升协议正确性和安全性，重点探讨了模型检查的价值及存在的问题，认为仍需更好的模型检查器。
关键信息：

• 作者为Igor Konnov，标签有 specification model-checking tlaplus quint apalache SMT，ChatGPT 为博客文章的第一位审稿人。
• 发表的两篇论文：ChonkyBFT: Consensus Protocol of ZKsync和Exploring Automatic Model-Checking of the Ethereum Specification。
• 测试的价值：确保系统有至少一个有用执行、发现代码更改导致的行为变化、展示设计师理解的差距。
• 模型检查的价值：在有界范围内是完备的，在小范围内能在合理时间内终止且大多自动化，能找到某些特定 bug 及证明正确性。
• 存在的问题：模型检查器使用不当则难以发挥作用，SMT 求解器性能不可预测，对复杂工业协议处理有局限。
  重要细节：
• 测试单输入只能检查一个数据点，财产测试工具和模糊测试可尝试多个输入，但需理解其工作原理。
• 不同模型检查工具在不同类型不变量的发现上各有优势，如 Quint 的随机模拟器和 Apalache。
• 模型检查的有界范围包括固定或有界的协议参数、执行长度、集合边界等。
• [Apalache]引入有界范围，[Alloy]从一开始就有范围，[bounded model checking]围绕限制搜索到短执行。