Trust and security
Audits and verification
What has been machine-checked, and the repeated AI audits the protocol has had.
Umbra's most critical code is checked by machine and audited repeatedly, not only reviewed by hand.
What has been machine-checked
- The circuits. Lean 4 models of the transaction and escape-hatch circuits prove that no transaction can create value, withdraw more than it funds, or skip its fees. The models are written by hand, and that they match the circuits is assumed; see formal verification.
- The double-spend checks. The nullifier staging buffer, the Merkle tree and the set they use are checked over every input within stated bounds, and modelled in Lean.
- Governance. The shared timelock has a Lean model proving its rules for authorities, delays, expiry and cancellation, and the guardian registry's own governance is modelled too.
- The verifiers. The on-chain checks for enclave attestations and signatures carry Lean models.
- Fuzzing. Fuzz targets exercise governance, the guardian registry, the verifiers and the Merkle tree. Fuzzing finds failures; it proves nothing.
Repeated AI audits
Alongside the machine-checked work, the protocol has been audited repeatedly by frontier AI models, run back to back and across several different model providers. Each run reviews the programs, circuits and services afresh, so one model's blind spots are checked by another's, and their findings feed back into the code. These audits are reviews, not proofs: they find problems rather than rule them out.
Related
Last updated