本文是Certora对Blend v2智能合约进行的形式化验证竞赛报告,通过引入代码突变来评估参赛者提交的规范质量。报告列出了被参赛者成功捕获的突变示例,展示了高质量的属性,并提供了竞赛结果和相关资源链接。