Security Audits
Overview
The snarkVM stack (including AleoVM components) and the broader Aleo stack have undergone third-party security reviews and audits. This page links to official announcements and public audit reports. Blog posts are typically high-level summaries, the audit reports are the canonical source of findings, severity, and remediation status.
Blog posts and announcements
Audit announcements and summaries
- Aleo completes security audits of snarkOS & snarkVM — Aleo Foundation announcement summarizing audits of the Aleo node (
snarkOS) and VM/crypto stack (snarkVM). - Aleo synthesizer audit — zkSecurity blog post summarizing their audit of Aleo’s synthesizer.
Security assurance engineering (formal methods, fuzzing)
- Formal Verification of Constraint Systems — Provable’s work on formally verifying compilation phases and constraint system gadgets.
- Celebrating AleoBFT formal verification milestone — Provable’s formal modeling/proof work for AleoBFT properties in an ACL2 model.
- Fuzzing the Aleo VM: Two Approaches to Bulletproof Security — Provable’s fuzzing strategy for hardening AleoVM/snarkVM.
Public audit reports
- zkSecurity audit reports — Public audit reports from zkSecurity, including Aleo-related components.
Specifications
For formal specifications of the AleoVM and consensus layer that were in scope for these audits, see Specifications (or https://developer.aleo.org/concepts/specifications).