上週在 OOPSALA '25，我們的 Act 開發者展示了一個改進的、可擴展的 CheckMate 版本，這是一個自動化的證明器，用於正式驗證區塊鏈協議的博弈論安全性。 簡而言之：該工具檢查協議中的激勵是否使作弊不值得。

協議需要三種安全性： • 密碼學：你的密鑰/密碼是否強大？ • 實施：代碼中是否有錯誤？ • 博弈論：激勵是否對齊，以至於作弊不會有利可圖？ 最後一點至關重要，但常常被忽視。

博弈論安全性是確保即使是理性、自私的行為者也更願意遵循規則——因為偏離規則的成本高於收益。 這是安全性的“經濟學”。

CheckMate 正式且自動地使用 SMT 解算器證明博弈論安全性。該論文介紹了一種組合的「分而治之」算法，能擴展到數百萬個節點，交錯模型生成和分析以提高效率。

為什麼這很重要： 我們現在可以自動、正式且大規模地證明區塊鏈協議的激勵措施使作弊變得不理性——在部署之前。