> For AI agents: the documentation index is at https://docs.umbraprivacy.com/llms.txt, and every page is available as Markdown at its URL with .md appended.

# Audits and verification (/docs/security/audits)

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](https://docs.umbraprivacy.com/docs/proofs/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

- [Formal verification](https://docs.umbraprivacy.com/docs/proofs/formal-verification): The Lean libraries in detail.
- [Trust assumptions](https://docs.umbraprivacy.com/docs/security/assumptions): What the checks do not cover.
- [Governance and upgrades](https://docs.umbraprivacy.com/docs/security/governance): Who can change what runs.
- [Trusted setup](https://docs.umbraprivacy.com/docs/security/trusted-setup): Where the proof keys came from.


Last updated 12 October 2026