AI 中文总结
研究ZKP安全工具现状，梳理工具情况，评估六种工具在70个漏洞中的表现，分析形式验证工作，调查从业者，发现安全工具与开发审计流程整合需优化，为相关人员提供见解。
AI 中文摘要
零知识证明（ZKPs）已成为隐私和可验证计算的核心技术，用于保障处理数十亿美元的区块链和涉及敏感个人数据的身份应用安全。然而，ZKP系统复杂，细微的实现错误可能破坏其安全性。研究人员和从业者开发了一系列错误检测和形式验证方法，但其实用效果和采用情况尚不明晰。本文旨在揭示ZKP安全工具的现状。首先对这些工具进行系统化梳理，发现多数针对Circom，对新的领域特定语言（DSLs）和零知识虚拟机（zkVMs）支持有限。接着评估六种工具在70个实际漏洞中的表现，发现工具在孤立目标上能检测45.7%的漏洞，但在完整代码库中有效性降至19.6%，重要漏洞类别未得到解决。还对形式验证工作进行首次系统分析，揭示当前工作主要聚焦于约束正确性，存在关键差距和风险。最后对48名从业者进行调查，表明开发和安全仍由人力主导，大语言模型广泛使用，从业者优先选择保证更清晰、集成工作量更低的工具。总体而言，研究结果凸显了安全工具与开发及审计流程更好整合的必要性，并为研究人员和从业者提供了可操作的见解。
英文摘要
Zero-knowledge proofs (ZKPs) have become a core technology for privacy and verifiable computing. They are used to secure blockchains that handle billions of dollars and identity applications dealing with sensitive personal data. However, ZKP systems are complex, and subtle implementation errors can completely break their guarantees, letting attackers forge money or false proofs of identity. Researchers and practitioners have therefore developed a growing set of bug detection and formal verification methods to secure these systems. Yet their real-world effectiveness and adoption remain unclear. In this paper, we aim to shed light on the state of ZKP security tooling. We first systematize the landscape of these tools and observe that most target Circom, leaving newer DSLs and zkVMs with limited support. We then evaluate six tools across 70 real-world vulnerabilities and find that while the tools detect 45.7% of bugs on isolated targets, their effectiveness drops to 19.6% on full codebases, with important vulnerability classes left unaddressed. We also present the first systematic analysis of formal verification efforts, revealing that current work focuses primarily on constraint correctness and identifying key gaps and risks. Finally, we survey 48 practitioners, showing that development and security remain human-led, LLMs are widely used, and practitioners prioritize tools with clearer guarantees and lower integration effort. Overall, our results highlight the need for better integration of security tooling with the development and auditing process, and we provide actionable insights for researchers and practitioners.
