本文是零知识虚拟机（zkVM）安全系列的第一篇文章，主要介绍了zkVM的基本概念、工作原理及其在可验证计算中的作用。文章还简要介绍了zkEVM及其在区块链中的应用，并概述了该系列后续文章的主题，旨在为零知识领域的研究人员和zkVM开发者提供有用的安全指导。

本文是 RISC Zero 的高级协议工程师 Rami Khalil 参加的炉边访谈的总结，讨论了使用 RISC Zero zkVM 构建应用程序的设计空间，包括 zkVM 的原理、开发者体验、安全性保证、去中心化证明网络 Boundless，以及 zkVM 如何赋能新的应用场景，还分享了开发者的建议和 Veridise 的安全审计经验，和RISC Zero的未来发展方向。

Veridise 与 Succinct 合作，使用 Veridise 的工具 Picus 来验证 Succinct 的 RISC-V zkVM，SP1 电路的确定性。通过将 Plonky3 电路转换为 LLZK，成功验证了多个 SP1 电路的确定性。同时，也发现了 Plonky3 到 LLZK 转换管道的局限性，并提出了改进方向，未来计划扩展 Picus 以验证 SP1 中的所有电路。

Aztec 团队的 Michael Klein 和 Veridise 的 Jon Stephens 展开了一场炉边谈话，深入探讨了 Aztec 网络的关键组成部分——Noir 编程语言。讨论涵盖了 Noir 的设计决策、开发者体验、工具生态以及安全相关主题，还讨论了 Noir 与其他 ZK DSL 的比较、隐私考虑、元编程、Noir 和 zkVM 的区别以及形式化验证的作用。

本文介绍了Veridise与RISC Zero在zkVM安全方面的合作，强调通过自动化零知识验证工具Picus实现持续的安全验证，确保RISC Zero开发的zkVM具备正式的安全保证。文中详细描述了三种关键漏洞及其修复方法，展现了如何通过深度合作提高零知识系统的安全标准。

Veridise获得以太坊基金会的资助，开发出名为LLZK的新中间表示（IR），旨在统一和简化零知识电路编译，从而解决该生态系统中存在的碎片化问题。LLZK通过提供模块化、灵活性和形式验证等特点，计划提升ZK语言的可维护性与安全性，并加速安全工具的发展。

探索 ZK 框架：用 5 种不同的 ZK 语言实现的 Mastermind 游戏

本文介绍了Veridise在零知识安全方面的研究，重点分析了四篇相关论文。这些研究探讨了零知识电路的认证、自动检测不完全约束电路、零知识证明电路的实用安全分析以及分割Gröbner基的方法，展示了各自的创新工具和技术如何提高零知识系统的安全性和可靠性。

本文介绍了Veridise团队在智能合约安全领域的学术研究成果，共精选五篇论文，涵盖了智能合约的安全性检查、优化及验证等多个方面。每篇论文的研究均对智能合约的设计与安全审计具有重要的指导意义，并且为Veridise开发内部工具提供了基础和灵感。

这篇文章介绍了 V 规范语言，主要用于形式验证以证明程序逻辑的正确性。文章详细阐述了 V 语言的核心构建块—— V 语句，以及如何使用它们来指定智能合约的属性、合约不变性、方法合约和行为规范，强调了这些规范在开发安全智能合约中的重要性。