Input Output 演示用于 Cardano 智能合约验证的 Blaster

Cardano Community 发布了关于 Blaster 的演示，这是一款自动化验证工具，用于检查 Cardano 智能合约是否遵循指定规则。Input Output 工程师 Romain Soulat 和 Jean-Frédéric Etienne 展示了该工具如何检验这些性质，并在发现违背时给出一个反例。他们还讨论了关于证明重建的持续工作，以及如何让结果更易于查看。

定义 Cardano 合约必须做什么

智能合约为区块链交易设定条件，并决定应用如何处理资产。开发者可以指定例如只有获授权的用户才能解锁由合约持有的资金。形式化验证使用数学方法检查系统是否满足规范中写下的性质。传统测试考察的是若干选定情形，而形式化验证旨在确定在模型所覆盖的情形下某个陈述的性质是否成立。

Soulat，Cardano High Assurance 的技术负责人，解释说 Blaster 旨在自动化大量证明工作。开发者仍需定义他们想要检查的行为并提供相应的规范。当工具发现违反时，它可以生成一个供检查的反例。Soulat 举例说明了一笔交易或一系列交易，能够展示并非授权用户的人如何解锁某个输出。

Blaster 如何检查合约性质

Blaster 与自动求解器配合使用 Lean 4，这是一套用于表达数学陈述并处理证明的系统。它会先简化问题。如果在该阶段未能决定该性质，剩余问题可以交给求解器。为使检查与 Cardano 相关，团队已形式化了合约运行环境的部分内容，包括脚本执行和交易规则。

Etienne，资深形式化方法工程师，概述了三种可能的结果：某个性质可以被报告为有效、被证伪或未定。与被证伪结果相关联的反例有助于开发者识别合约缺陷、缺失的假设或规范中的错误。未定结果意味着求解器尚未确定该性质是否成立。一次检查的范围取决于开发者选择表达的性质。

[NEWSBREAK]

证明重建正在开发中

开发者可以将使用诸如 Plinth、Aiken 或 Plutarch 等语言编写的合约编译为 Untyped Plutus Core，这是一种用于执行 Cardano 脚本的表示形式。然后他们可以将编译后的代码导入 Lean 4，并指定要检查的性质。Input Output 先前发布了两个开源库，为这一流程提供了针对 Cardano 的模型。在更早的演示中，团队将该流水线用于一次安全挑战中的练习合约，生成了一个交易上下文，展示了如何可以利用该合约。

Etienne 解释说，证明重建仍在开发中。其目标是让 Lean 独立检查支持有效结果的证据。目前该工具在求解器返回该结果时尚未生成重建的 Lean 证明。Soulat 还概述了更清晰的反例视图计划，使开发者能够检查导致性质失败的交易细节。