形式化验证

Jolt 开发路线图更新

视频 AI 总结： 该视频介绍了 Jolt 项目在过去六个月的进展和未来计划。Jolt 是一种 RISC-V ZKVM，旨在提供快速的零知识证明。视频重点介绍了 Jolt 在支持 Rust 标准库和 RISC-V M 扩展后，主要解决了验证成本高和证明者空间使用大的问题。通过改进多项式承诺方案和批量处理，Jolt 的证明大小已从兆字节级别降至 200KB 以下，并有望进一步降低。未来，Jolt 将致力于通过折叠方案降低证明者空间使用，并探索基于哈希的承诺方案以进一步提高速度。此外，团队还将投入大量精力进行形式化验证，以确保 Jolt 实现的正确性。 关键信息： * Jolt 在过去六个月主要解决了验证成本高和证明者空间使用大的问题。 * 通过改进多项式承诺方案和批量处理，Jolt 的证明大小显著降低。 * 未来计划包括通过折叠方案降低证明者空间使用，探索基于哈希的承诺方案以提高速度，以及进行形式化验证。 * Jolt 旨在成为在资源受限环境中进行证明的理想 ZKVM，同时保持领先的证明速度。 * 将会有两个版本的Jolt，一个使用椭圆曲线，另一个使用哈希。

高级 Web3 安全课程 | 第九部分

视频 AI 总结： 该视频主要讲解了智能合约的形式化验证，强调其作为最高级别的测试手段，能够彻底证明合约在任何情况下的行为符合预期。与单元测试或模糊测试不同，形式化验证通过布尔公式将智能合约代码转换为 SMT 求解器可解释的形式，从而验证特定不变性。视频还介绍了如何使用 Solidity 内置的 SMT 检查器进行形式化验证，并通过实例演示了如何通过添加 require 语句来限制输入范围，从而使断言通过验证。 关键信息： * 形式化验证基于布尔公式，通过 SMT 求解器检查公式的满足性。 * SMT 检查器通过检查布尔公式的否定的不可满足性来验证断言。 * 可以通过 require 语句限制输入范围，使断言通过形式化验证。 * SMT 检查器不仅可以用于断言验证，还可以用于检查溢出、下溢、除零等潜在问题。 * SMT 检查器有其局限性，对于过于复杂的代码可能无法证明。 * 视频还介绍了如何通过提供价值和建立联系来获取审计机会，以及如何通过参加竞赛来展示自己的能力。