主要观点：在成功对 ChonkyBFT 共识进行规范和模型检查后，将 Quint 及其工具应用于 Solidity 中的治理合约领域，通过 Quint 对 ZKsync 治理协议进行规范和建模，包括各种合约（如 Multisig、Security Council、Guardians 等），重现威胁模型提交中的报告，检查法律声明，使用三种 Quint 工具技术进行实验，最终得出快速反馈循环和多种技术结合的结论。
关键信息：

• ZKsync 治理协议的结构和关键特征，包括不同的投票类和关键职能。
• 使用 Quint 建模协议，包括继承、多签机制、签名和哈希、EVM 调用历史等方面。
• 重现威胁模型提交中的报告，通过编写相应不变量来检查漏洞。
• 检查 ZKsync 治理程序中的法律声明，将其转化为状态不变量。
• 实验设置包括硬件和使用的三种 Quint 工具技术（随机模拟、随机符号执行、有界模型检查）及实验过程。
• 实验结果表明不同技术各有优缺点，有界模型检查能发现其他技术错过的不变量违反情况。
  重要细节：
• Quint 虽不是专门为 Solidity 设计，但在项目中发挥作用，规范和建模花费较多时间，反馈循环快。
• 各种合约的具体功能和实现细节，如 Multisig 合同的签名验证机制等。
• 实验中不同技术的运行方式和特点，如随机模拟的交易选择和参数生成方式等。
• 实验结果的具体数据，如不同实验所需时间、不同技术发现的不变量违反情况等。