Certora获资推进达姆合约行为可验证性研究

2026年5月21日，端到端安全验证平台Certora正式获得Canton发展基金201万枚Canton代币（约合30万美元）支持，用于构建专为Daml项目设计的开源静态分析系统。该研发计划聚焦于提升智能合约在运行过程中的行为透明度，推动其向机器可验证方向演进，并覆盖基于Canton网络构建的企业级应用。

实现跨包调用链路的可视化追踪

新工具将具备解析编译后.dar格式文件的能力，深入挖掘并呈现多模块间智能合约的交互路径——这一环节历来是系统复杂性与安全风险的核心所在。通过精准定位所有跨包调用权限实例，工具可回溯至具体源码位置及行号，提供完整的行为溯源信息。在强调隐私保护的Canton架构下，这种对合约供应链的全貌掌控，对于评估潜在数据泄露风险具有决定性作用，从而实现部署前关键环节的自动化分析。

优化多方协作系统的安全审计流程

在涉及多个参与方的智能合约体系中，跨包权限委托往往构成人工审查的最大难点。借助该工具的自动化能力，开发、安全与合规团队的工作负荷将大幅降低，同时显著增强组织对Canton上运行应用的信任水平，为跨机构协作提供坚实的技术保障。

该分析工具将以Apache 2.0协议开源发布，并直接嵌入Canton的dpm命令行工具链，便于开发者无缝集成至Daml应用开发流程。

支撑金融机构的分布式账本选型决策

对于正考虑引入分布式账本技术的银行、金融基础设施服务商而言，全面掌握智能合约的执行逻辑是实施部署的前提条件。Certora此次推出的分析能力，首次将高精度行为验证机制引入Canton生态，使技术选型更具可衡量性与可控性。

Certora联合创始人Mooly Sagiv指出：“随着核心金融系统逐步迁移至分布式账本，对智能合约的验证标准必须同步升级。我们与Canton基金会的合作，正是为了建立与DeFi领域同等严谨的自动化验证体系，确保最敏感场景下的系统可靠性。”

打造可追溯、可验证的系统信任基础

在去中心化环境中，信任的建立依赖于行为的可观测性与可验证性。尽管Canton采用隐私优先的设计理念，为可信节点间的协作提供了安全保障，但即便如此，验证方仍需具备对合约逻辑的深度理解能力。

该工具将为开发者与运营者提供清晰、可操作的跨包交互视图，使其能够在部署前完成对潜在安全威胁的全面识别与评估，真正实现从‘黑盒’到‘可审’的转变。