这篇研究报告探讨了在智能合约（如 Diem 支付网络）中推广形式化验证时，开发人员对“规范（specifications）”角色的不同理解如何影响形式化验证的整体效果。作者指出，初次接触形式化验证的软件开发者，往往对规范在操作层面上的意义持有微妙但不同的解释，这些解释会直接影响他们编写的规范类型，进而导致保证效果碎片化，削弱验证工作的整体效力。论文基于在一个金融敏感的智能合约环境中部署形式化验证系统的实际经验，总结了工业界资深开发者（但对形式化方法尚属新手）中常见的三种观点：1）规范是与最终用户沟通的实现与功能之间的契约；2）规范是类型系统的扩展；3）规范是高层状态机的定义。作者认为，虽然哪种解释更接近规范的真正目的尚无定论，但一个重要区分被忽略了：某些规范是“抽象规范（abstracting specs）”，用于锁定需求或意图，因此越多越好；另一些规范是“证明辅助（proof assistance）”，旨在促进实现与抽象规范之间的精化证明，因此应仅在需要时编写；还有一些规范是“指称规范（denotational specs）”，从形式化方法角度看并不增加额外的保证。若缺乏这一区分，形式化验证很容易陷入“规范累积但整体保证并未增加”的陷阱。论文作为一种经验报告，核心贡献在于提出应当明确区分不同类型的规范，并强调抽象规范在保证整体验证有效性中的关键作用。适合正在或计划在智能合约、区块链或高安全性系统中引入形式化验证的团队阅读，尤其对安全工程师和验证工程师具有实践指导意义。