FORMAL VERIFICATION

DOWNLOAD & VERIFY
THE PROOFS

Don't trust. Verify. Download our complete formal verification proofs and run them yourself using the Rocq/Coq proof assistant. 34+ cryptographic functions mathematically proven correct—no bugs, guaranteed by mathematics.

MINIMUM VERSION REQUIRED

Coq 8.16.0+ or Rocq 2023.01+. The proofs use modern syntax (From Stdlib Require) introduced in Coq 8.16. Ubuntu 22.04's default package (8.15) is incompatible—use Opam or Rocq Platform instead.

DOWNLOAD PROOFS (115 KB)VIEW ON GITHUB

✓

10 Modules

Verified

332 KB

Total Proofs

181+ Lemmas

Proven

✓

65+ Theorems

Certified

▸QUICK START

Verify the proofs in 4 simple steps. No prior Coq experience required.

STEP 1

Install Rocq/Coq 8.16+

Method 1: Opam (Recommended)

$ sudo apt-get install opam

$ opam init -y && eval $(opam env)

$ opam install coq.8.18.0 -y

Method 2: Rocq Platform:

$ curl -fsSL https://get.rocq-prover.org | sh

macOS:

$ brew install coq

Windows:

Download from rocq-prover.org/install

STEP 2

Extract Archive

$ tar -xzf anubis-notary-formal-proofs.tar.gz
$ cd proofs/

The archive contains all proof files, specifications, and a comprehensive README with detailed instructions.

STEP 3

Verify All Proofs

$ make prove

Expected output:

Compiling theories/aead_spec.v...
✓ theories/aead_spec.vo
Compiling theories/argon2_spec.v...
✓ theories/argon2_spec.vo
...
✓ All proofs compiled

STEP 4

Check Status

$ make status

Shows verification status for each proof:

Proof Status:
✓ aead_spec
✓ argon2_spec
✓ cbor_spec
✓ merkle_spec
✓ mldsa_spec
...

▸TESTED CONFIGURATIONS

Know before you start: Verified OS and Coq version combinations.

Operating System	Installation Method	Coq Version	Status
Ubuntu 24.04 LTS	apt-get	8.18+	✓ WORKS
Ubuntu 22.04 LTS	apt-get	8.15	✗ INCOMPATIBLE
Ubuntu 22.04 LTS	Opam	8.18.0	✓ RECOMMENDED
Ubuntu 20.04 LTS	Opam	8.18.0	✓ WORKS
macOS 14+ (Sonoma)	Homebrew	8.18+	✓ WORKS
macOS 13 (Ventura)	Homebrew	8.15	✗ INCOMPATIBLE
macOS (any)	Opam	8.18.0	✓ WORKS
Windows 11	WSL2 + Opam	8.18.0	✓ WORKS

KEY TAKEAWAY

Always use Opam to install Coq 8.18.0 for guaranteed compatibility. System package managers (apt-get, brew) may install outdated versions. Opam works on all platforms and ensures you get the correct version.

▸WHAT GETS VERIFIED

Every cryptographic primitive in Anubis Notary is formally verified for correctness, memory safety, and security properties.

AEAD (ChaCha20Poly1305)

Authenticated encryption correctness

aead_spec.v25 KB

Argon2id

Memory-hard key derivation

argon2_spec.v37 KB

CBOR

Serialization correctness and parsing safety

cbor_spec.v30 KB

Merkle Trees

Tree construction and proof verification

merkle_spec.v101 KB

ML-DSA-87

Post-quantum signature correctness

mldsa_spec.v24 KB

Constant-Time Ops

Timing attack resistance

ct_verified.v12 KB

Nonce Generation

Uniqueness and randomness guarantees

nonce_verified.v11 KB

Memory Safety

Buffer overflow prevention

bytes_verified.v17 KB

▸VERIFICATION GUARANTEES

Formal verification provides mathematical proof—not just testing—that code behaves correctly.

WHAT IT PROVES

✓Correctness: Functions behave exactly as specified
✓Memory Safety: No buffer overflows, use-after-free, or memory leaks
✓Constant-Time: No timing side-channels
✓Security Properties: Cryptographic guarantees (e.g., signature unforgeability)
✓Zero Bugs: Mathematically proven correct (not just tested)

⚠WHAT IT DOESN'T PROVE

×Hardware bugs (e.g., Spectre, Meltdown)
×Compiler bugs (though Coq can extract to verified CompCert C)
×Operating system bugs
×Physical attacks (power analysis, fault injection)

▸REFINEDRRUST INTEGRATION

Anubis Notary uses RefinedRust to bridge Rust code and Coq proofs, ensuring the actual implementation matches the formally verified specifications.

// Rust Source Code

pub fn ct_eq(a: &[u8], b: &[u8]) -> bool {
// Constant-time equality
}

→

(* Coq Specification *)

Definition ct_eq_spec :=
timing_invariant ∧
correctness_proof.

→

✓ Verified Rust Code

Mathematically proven
to match specification

▸ADDITIONAL RESOURCES

Learn more about formal verification and the tools we use.

Rocq/Coq Prover

Official website for the Rocq proof assistant (formerly Coq)

rocq-prover.org →

RefinedRust

Framework for verifying Rust code with Coq proofs

github.com/refinedrust →

Software Foundations

Free textbook series on formal verification with Coq

softwarefoundations.cis.upenn.edu →

▸TROUBLESHOOTING

Common issues and solutions when verifying the proofs.

Error: "Cannot find a physical path bound to logical path Lia with prefix Stdlib"

Cause: You have Coq 8.15 or earlier installed. The proofs require Coq 8.16+ for modern syntax support.

# Check your version

$ coqc --version

# If version is 8.15 or earlier, uninstall and reinstall via Opam:

$ sudo apt-get remove coq