Deterministic first
Compilation, AST-backed symbol indexing, semantic graphs for calls, state, privilege, asset flow and upgrades. Every finding binds to an exact source range and its hash.
Smart-contract security · Solidity & EVM
Audits that show their working.
Corrovera Security is building an evidence-driven audit engine for Solidity and EVM protocols. Deterministic analysis, independent frontier models reviewing blind, adversarial validation of every candidate finding — and a report that states exactly what ran, what did not, and what the result does and does not support.
The core idea
One reviewer can be wrong. Several, disagreeing, are harder to fool.
Independent paths to the same conclusion are worth more than any single opinion, however capable. Corrovera runs multiple genuinely independent model families over the same protocol, blind to one another, then makes them argue. A finding survives only if the evidence does.
Independent minds
Several frontier model families from distinct root lineages review the protocol without seeing each other's work. Two aliases of the same base model are one opinion, not two, and are counted that way.
Adversarial validation
Every candidate is sent to independent reviewers instructed to refute it, defaulting to refuted when uncertain. Agreement between models is never treated as proof on its own.
How an audit runs
Breadth of a large team. Reproducibility of a pipeline.
A protocol is decomposed into coherent shards that respect contract and graph boundaries, then reviewed in passes — orientation, blind discovery, reduction, cross-shard integration, cross-examination, validation, and evidence-capped judgment.
Every surface accounted for
Coverage is reported with real denominators — contracts, functions, privileged entry points, state writers, asset flows. Critical surfaces require review by multiple independent lineages. Nothing is silently skipped.
Executed, not just argued
Where a claim can be tested, it is: the protocol's own suite run against pinned fork state, differential execution across blocks, fuzzing, symbolic execution and formal methods where applicable. Execution can originate a finding, not merely confirm one.
Source-bound findings
Locations are revalidated against real source after the run. A finding that cannot be anchored to code that exists is rejected, not published with a caveat.
Reproducible
Each run emits an immutable manifest: exact models and providers, prompts and schemas by hash, tool versions, configuration, and every artifact. The audit can be re-derived from its own record.
Evidence discipline
The rules we will not trade away.
Most of the engineering in Corrovera is not about finding more. It is about never asserting more than the evidence carries.
- EVIDENCE Model agreement alone cannot confirm a finding. Confirmation requires reproduction, proof, or strong deterministic analyzer evidence that an independent reviewer has accepted.
- FAIL CLOSED An analysis that did not run is never a pass. A missing scanner, unavailable engine, timeout, or failed compilation makes a run incomplete and says so — it does not quietly become a clean result.
- NO CLEAN BILL A report with no findings is not proof of safety. It is a record of what these methods examined at this depth, with the limits stated plainly alongside it.
- PROVENANCE Scanner and model output are leads, never proof. Heuristic signals are labelled as such and can never be promoted to compiler-grade facts.
- PRIVACY Source egress is explicit and bounded. Zero-retention routing by default, credentials and key material excluded before anything leaves the machine, and no weaker policy without recorded consent.
- CLAIMS Every claim follows the evidence. We will not describe Corrovera as superior to professional audit teams until blind, independently adjudicated comparison supports it.
Build status
Where the engine actually is.
This page describes what Corrovera is being built to do. Some of it runs today and some of it does not. Rather than blur the two, here is the current state.
| Capability | State | Notes |
|---|---|---|
| Deterministic Solidity analysis | Running | Project detection, compilation, AST-backed indexing, semantic graphs, coverage denominators. |
| Static analysis integration | Running | Hardened, isolated execution with per-tool provenance and honest unavailable states. |
| Repository sharding & multi-pass review | Running | Coherent semantic shards and a resumable pass scheduler with durable run state. |
| Honest run status & fail-closed gates | Running | A run with no completed analysis reports incomplete and exits non-zero. |
| Fork-based execution & differential testing | In build | Foundry path implemented; Hardhat pending a hardened container toolchain. |
| Qualified multi-model ensemble | In build | Model qualification benchmark and lineage independence accounting in progress. |
| Measured performance benchmark | Planned | Public time-split corpus, private holdout, and independently adjudicated human comparison. |
| Self-serve audit purchase | Planned | Not offered for sale. Nothing is sold here until the engine passes its release gates. |
We are not selling audits yet. Corrovera has not completed an independently adjudicated comparison against professional audit teams, so it makes no claim of superiority — and it will not until that evidence exists. If you want to follow the work, or talk about an engagement when it is ready, get in touch.
Contact
Talk to us.
For protocol teams, prospective partners, and anyone who wants to scrutinise the method. We would rather be challenged early.