本文介绍了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 语句，以及如何使用它们来指定智能合约的属性、合约不变性、方法合约和行为规范，强调了这些规范在开发安全智能合约中的重要性。

本文详细介绍了Medjai，一种用于寻找Cairo程序中的错误的符号执行工具。文章从Cairo语言的背景出发，深入探讨了零知识证明、Cairo工作流程、符号执行技术及其在实际开发中的应用，特别是如何帮助开发者发现Bug并验证修复。文章结构清晰，内容丰富，适合对区块链智能合约开发和安全感兴趣的读者。