Auditor Manual

Guide & Trust Policy

Learn how to verify mathematical proofs locally and understand our cryptographic trust model.

1. Local Verification (Auditing)

Independent auditing is the core value of the Nano Proof Auditor. Follow these steps to cryptographically verify any proof on your machine.

Ensure you have the Rust toolchain and Cargo installed on your system.
Install the NPA CLI tool from source or package manager:
```
cargo install npa-cli
```
Navigate to any package index directory (e.g. npa-mathlib) and run the verification commands locally:
```
npa package verify-certs --root ../npa-mathlib --checker reference --json
```

2. Trust & Axiom Policy

NPA classifies mathematical constants and axioms to audit logical soundness.

Trusted Evidence vs. Untrusted Sidecars

Deterministic hash values, verifier logs, and checker signatures (.npcert) represent trusted evidence. Source code text, proof replay steps, and documentation overlays are untrusted sidecar assets that are verified only for presentation.

Axiom Whitelisting

To prevent logical contradictions (such as deriving False), theorems are audited against a strict axiom policy. Lean's standard classical axioms (Quot.sound, Propext, Classical.choice) are whitelisted. Unverified axioms or custom assumptions trigger policy violations.

3. Terminology Glossary

Quick definitions of formal verification concepts used in this registry.

Theorem

A mathematical statement verified by a cryptographic certificate (.npcert) showing that a sound proof term was checked.

Axiom

A statement assumed without proof. Axioms are the logical foundation, but unchecked custom axioms can introduce contradictions.

Inductive Type

A data type defined by its constructors (e.g., Natural numbers defined via zero and successor).

Proof Term

A mathematical expression representing the proof of a theorem under the Curry-Howard isomorphism.

Proof Replay

The step-by-step reconstruction of proof terms to verify their validity inside the kernel.