零知识证明（ZKP）已成为隐私和可验证计算的核心技术，广泛应用于保护处理数十亿美元的数字货币区块链以及处理敏感个人数据的身份应用。然而，ZKP系统复杂，细微的实现错误可能完全破坏其安全保障，使攻击者能够伪造货币或身份证明。为此，研究人员和从业者开发了越来越多的漏洞检测和形式化验证方法来确保这些系统的安全性。但它们的实际有效性和采用情况仍不明确。本文旨在阐明ZKP安全工具的现状。首先，我们系统化了这些工具的格局，发现大多数工具针对Circom，而对较新的DSL和zkVM的支持有限。接着，我们使用六个工具对70个真实世界漏洞进行了评估，发现这些工具在隔离目标上检测到45.7%的漏洞，但在完整代码库上，检测率降至19.6%，且重要的漏洞类别未被覆盖。我们还首次对形式化验证工作进行了系统分析，揭示当前工作主要集中在约束正确性上，并指出了关键差距和风险。最后，我们对48位从业者进行了调查，结果显示开发和安全性仍然以人为主导，LLM被广泛使用，从业者更青睐具有更清晰保证和更低集成难度的工具。总体而言，我们的结果强调了将安全工具更好地集成到开发和审计过程中的必要性，并为研究人员和从业者提供了可操作的见解。本文适合需要了解ZKP安全工具现状、有效性及挑战的安全研究人员、区块链开发者以及审计人员阅读。