AI Auditing Tools for Cryptography & ZK

zkSecurity is a cryptography security firm with more than a hundred audits across zero-knowledge, MPC, FHE, post-quantum and consensus systems. It builds zkao, the continuous AI scanner for cryptography code, publishes zk-skills and the zkbugs benchmark as open source, and offers enterprise packages that combine zkao with its security engineers and manual audits. Its 2026 case studies (Cloudflare CIRCL, OpenVM, Bron Labs) are the most detailed public accounts of AI findings in cryptographic code, including what the AI got wrong.

Listed first because it is the only firm on this index whose AI tooling was built for cryptographic and ZK code, with upstream-confirmed critical results (seven CIRCL bugs, OpenVM CVE-2026-46669, four bron-crypto zero-days), an open benchmark and open skills, and explicit human-in-the-loop validation by cryptographers.

Trail of Bits built Buttercup, the AIxCC runner-up, and has reorganised its audit practice around AI: it reports 15 to 200 AI-surfaced candidate bugs per week on suitable engagements, about 20 percent of reported findings first surfaced by AI, every one validated by an auditor, and publishes 201 skills and 94 plugins as open source. It has a cryptography and ZK practice.

Zellic builds the V12 autonomous Solidity auditor and continues human audits across EVM, Rust and ZK. It owns Code4rena, which announced it is closing.

Nethermind Security runs AuditAgent after every manual audit as a second layer and publishes its recall against its own human findings (30 percent average, 42 percent of criticals). It also has a formal verification team working in Lean and EasyCrypt.

Sherlock combines its Sherlock AI product with contest-based and private human audits, and has published a controlled precision study of the AI.

Cantina, from Spearbit, markets an AI-native application security platform with an enterprise AI code analyzer, combined with human expert review from a network of more than nine thousand researchers. It is unrelated to the agentic SecOps startup of the same name launched in July 2026.

Consensys Diligence describes an agentic vulnerability-mining workflow in which swarms of parallel agents act as lead generators and a confirmation layer, guided by veteran auditors, alongside its symbolic-execution tooling.

Cyfrin maintains the Aderyn static analyzer (not AI), opened its Solodit database of more than fifty thousand audit findings to AI agents via an API, runs CodeHawks contests, and lists an AI formal verification engagement for Lido's Circuit Breaker (April 2026) in its public reports.

OpenZeppelin markets an AI Auditor within its Program Security offering and published the March 2026 audit of EVMbench that identified invalid high-severity items and contamination risk. Product details are not public.

QuillAudits pairs its QuillShield AI auditor and open-source Claude skills with human audits, reporting more than 1,400 projects audited.

Certora's core is the open-sourced Certora Prover; its AI work (AI Composer, Concordance) uses the prover to check model output rather than to scan code. Human audits continue.

Veridise is a strong ZK audit firm (RISC Zero, Linea, Succinct, Semaphore) whose tooling is formal and static (Picus, Vanguard, ZK Vanguard, OrCa, LLZK) rather than LLM-based. It is listed for teams weighing AI scanners against solver-based alternatives for circuits.