Tools
Veridise combines professionals manually reviewing the code with our in-house tools.
We continuously develop and improve our in-house security tools. These tools improve the quality of our audits and reveal bugs that are difficult for the human eye to find.
Our tools enable Veridise to provide comprehensive findings and detect hard-to-find bugs and vulnerabilities.
With Veridise, you can rest assured your codebase is in the hands of industry-leading detection methods.
OrCa
Specification-guided fuzzer
Vanguard
Static analysis tool for smart contracts and ZK circuits
Picus
Zero-Knowledge Proof auditing tool finding bugs in arithmetic circuits
Learn more about each tool below
Vanguard
Static analysis tool for smart contracts and ZK circuits
Vanguard is our static analysis tool for finding common vulnerabilities in smart contracts and ZK circuit source code.
By reading just the source code, Vanguard can quickly and accurately identify smart contract security vulnerabilities like reentrancy bugs and flashloan vulnerabilities. It is also capable of identifying subtle and potentially disastrous vulnerabilities in ZK circuits – underconstrained signals, nondeterministic dataflow and much more.
Put simply, Vanguard quickly and efficiently “proofreads” checks your code for errors so when it’s time to deploy, you can do it with peace of mind.
Picus
Zero-Knowledge Proof auditing tool finding bugs in arithmetic circuits
Picus is a tool we developed to check the uniqueness property (under-constrained signals) of zero-knowledge proof circuits.
It is based on the research paper Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs (PLDI 2023).
Picus currently supports Circom, R1CS, and gnark, with an open-source version available for R1CS.
OrCa
Specification-guided fuzzing
OrCa is a specification-guided fuzzer, a type of automated testing tool which discovers bugs by generating and running thousands of pseudo-random inputs against a target application.
OrCa allows users to write concise but expressive temporal specifications that express properties of a blockchain protocol over time.
With OrCa, you can catch more bugs more quickly – and focus on what really matters: your core project.
The [V] Specification Language
Zero-Knowledge Proof auditing tool finding bugs in arithmetic circuits
Our team has created the [V] specification language. With it, developers can easily provide specifications for formal security analysis in a mathematically precise way.
[V] is a powerful language that provides you with multiple tools to express the properties you care about. With it, you can concisely express many types of correctness and security requirements that you care about.
Featured blog posts
Learn more about our in-house tools and how we improve the quality of audits with them.
Unleashing the Power of OrCa...
Veridise
5 min read
Ensuring Trust and Security: The...
Veridise
8 min read
Unlocking SMT for ZK Verification
Veridise
3 min read
Explore Veridise Github
Some of the tools (such as Veridise Picus for finding bugs in zero-knowledge circuits) are open source and available to the public. Explore our repositories using the link below.