形式化验证

本文详细介绍了形式化验证（formal verification）的过程及其在智能合约中的应用，强调了与单元测试的互补关系，以及如何利用Halmos工具简化形式化验证的实施。文中分析了正式验证的挑战、规范的编写开销及其在ERC721A智能合约中的案例，展示了通过符号测试实现高效验证的重要性。

本文详细介绍了Silo融资协议中的一个关键漏洞及其修复过程。通过Certora的形式验证工具进行深入分析，报告总结了漏洞的产生原因、修复方法及验证过程，并提出了未来加强规则和安全性的计划。

本文介绍了SushiSwap即将推出的Trident平台中的一个池排空漏洞及其修复过程。通过三个步骤，文章详细阐述了如何通过形式化验证技术发现此漏洞，并详细描述了恶意用户如何利用该漏洞进行攻击，最后介绍了SushiSwap所采取的修复措施。

本文介绍了Compound新协议Comet的一个有趣的正确性规则，以及在早期开发过程中如何利用Certora Prover进行形式化验证，以消除代码中的bug。通过形式化规范和验证，团队成功发现并修复了一个导致用户抵押资产状态错误的bug，从而提高了协议的安全性。

本文揭示了PRBMath库中mulDivSigned函数的一个设计缺陷，该缺陷会导致在计算有符号数的乘法和除法时出现精度问题，特别是在DeFi应用中可能被利用导致资金损失。Certora团队通过形式化验证工具发现了这个存在于多个PRBMath版本中的问题，并与作者Paul Razvan Berg合作，最终通过修改函数定义为向零取整来临时解决，并计划在未来提供更全面的舍入模式支持。

本文详细描述了在 Balancer V2 中发现的一个由 Certora 团队通过形式化验证发现的偿付能力漏洞。该漏洞允许用户通过将贷款分割成小额多次来逃避闪电贷费用，从而导致 Vault 的偿付能力受损。Balancer 团队通过要求 token 地址数组按严格升序排列解决了这个问题。

Beosin-VaaS的业务逻辑验证软件，是一款用来检测智能合约上层业务逻辑漏洞的软件。

近日，成都链安推出全球首个Fabric链码自动形式化验证工具--Beosin-VaaS for Fabric，为链码提供“军事级”的安全验证。

本文探讨了区块链与人工智能安全之间的联系，指出两者在如何调控复杂系统以应对不可预测结果方面存在相似性。作者分析了在DAO治理和加密经济学中面临的共同挑战，以及一些正在探索中的解决方案，例如延迟治理和形式化验证。同时，文章提出了未来DAO可能学习到的经验，强调去中心化的重要性。

本文强调了形式化验证（FV）在Web3和DeFi安全中的重要性，指出传统测试方法不足以应对Web3的安全挑战。FV通过数学证明确保代码按预期运行，能预防高危漏洞，并已在多个知名DeFi项目中应用，同时建议将FV尽早集成到开发生命周期中，以提升代码质量和安全性。

随着以智能合约（Smart Contract）及区块链应用（DApp）为核心的区块链2.0时代逐渐成为主流，智能合约及区块链应用的安全性也越发成为业界备受关注的焦点。尤其是，在经历过诸如THE DAO、币安被盗等事件，智能合约及区块链应用的安全性究竟应该如何得到验证和保障，业已成为当前区块链业界亟待解决的痛点。

“程序测试能证明错误的存在, 但不能证明错误不存在” – Edsger Dijkstra。智能合约是一个对安全性要求非常高的领域，一个不经意的小 bug 很可能会导致不可估量的损失。

本文介绍去中心化金融（DeFi）的概念及其安全性的重要性，强调了寻找智能合约中的漏洞及进行形式化验证的实际方法。文章为有数学或计算机科学背景的学生提供了在DeFi领域发展的机会，提到了一些在线比赛和奖励来激励学习和探索。还提供了后续资源和即将到来的比赛信息。

本文详细介绍了Vlad的Casper协议及其在Isabelle/HOL中的形式化验证过程，探讨了异步环境下共识问题的核心挑战，并展示了如何使用形式化方法确保估计的安全性。