For Auditors ARCHIVE
For Auditors: 5-Minute Verification Checklist
This page provides a quick verification path for external auditors evaluating MathLedger's governance claims.
5-Minute Verification Checklist
Complete these steps to verify the system's core claims:
Step 1: Open the Hosted Demo (30 seconds)
- Navigate to /demo/
- Confirm the demo loads without errors
- Verify the version banner shows
v0.2.4-verifier-syntax-fix
Step 2: Run the Boundary Demo (90 seconds)
- In the demo, click "Boundary Demo: Same Claim, Different Authority"
- Observe the 4-step sequence:
- Key insight: Same mathematical truth, different outcomes based on trust class declaration
Step 3: Download Evidence Pack (30 seconds)
- After running the boundary demo, click "Download Evidence Pack"
- Save the JSON file locally
- Note: This file contains cryptographic commitments to all demo operations
Step 4: Verify with Auditor Tool (60 seconds)
- Open the Evidence Pack Verifier
- Upload the evidence pack JSON you downloaded
- Click "Verify"
- Confirm status shows PASS
- Observe the hash verification: U_t, R_t, and H_t all match
Step 5: Tamper Test (60 seconds)
- Open the downloaded evidence pack in a text editor
- Change any character in the
reasoning_artifactssection - Re-upload to the verifier
- Click "Verify"
- Confirm status shows FAIL with hash mismatch
Ready-to-Verify Examples (No Demo Required)
If the demo is unavailable or you want to verify without running it, use these pre-generated examples:
Download Examples
The file /v0.2.4/evidence-pack/examples.json contains:
| Example | Expected Result | Purpose |
|---|---|---|
valid_boundary_demo | PASS | Shows a correctly-formed evidence pack from a boundary demo |
tampered_ht_mismatch | FAIL (h_t mismatch) | Demonstrates detection of tampered H_t field |
tampered_rt_mismatch | FAIL (r_t mismatch) | Demonstrates detection of tampered reasoning artifacts |
Verification Steps
- Download
examples.json - Copy the content of
examples.valid_boundary_demo.packto a new file - Open the Evidence Pack Verifier
- Upload the pack JSON
- Click Verify and observe PASS
- Repeat with
tampered_ht_mismatch.packand observe FAIL
Why This Matters
These examples prove:
- The verification algorithm is deterministic (same input always produces same hash)
- Tamper detection works (any modification is detected)
- No demo required (auditors can verify offline using the same code)
What This Version Claims
This version (v0.2.4) demonstrates:
- Deterministic canonicalization of reasoning artifacts (RFC 8785-style)
- Cryptographic binding via H_t = SHA256(R_t || U_t)
- Trust class separation where ADV claims are excluded from R_t
- Replay verification using the same code paths as live execution
- Self-auditing capability via the evidence pack verifier
What This Version Does NOT Claim
Explicit non-claims:- No formal verification — FV (Formally Verified) claims always return ABSTAINED. There is no Lean/Z3/Coq integration.
- No multi-model consensus — Only one partitioner template is active. The "multi-model arena" is not operational.
- No learning loop — RFL (Reinforcement from Ledger) is not active. The system does not learn from past decisions.
- No production hardening — This is a demonstration, not a production system. Do not use for real financial or legal decisions.
- No guaranteed uptime — The hosted demo may be unavailable. Local execution is always possible.
Key Documentation Links
| Document | Description |
|---|---|
| Scope Lock | What this version does and does not demonstrate |
| Invariants | Tier A/B/C enforcement status with explicit counts |
| Field Manual | Obligation ledger driving version promotions |
| Hostile Demo Rehearsal | Pre-prepared answers to skeptical questions |
| How the Demo Explains Itself | UI self-explanation integration points |
Field Manual (Why It Exists)
The Field Manual (fm.tex/pdf) is an internal constraint artifact, not marketing documentation.
It is not rewritten yet; it is used to surface obligations and gaps.How auditors should use it:
- Cross-reference claims — If a feature is claimed, check FM for caveats
- Look for "TODO" and "OBLIGATION" — Explicit acknowledgments of gaps
- Compare versions — FM changes show what was addressed between releases
- Trust gaps over features — The gaps we document are more honest than features we claim
Local Verification (Alternative Path)
If the hosted demo is unavailable, verify locally:
git clone https://github.com/helpfuldolphin/mathledger
cd mathledger
git checkout v0.2.4-verifier-syntax-fix
uv run python demo/app.py
Open http://localhost:8000
The local demo produces identical evidence packs that can be verified with the same auditor tool.
External Audits
Independent audits of this project are listed below.
| Date | Auditor Role | Version Audited | Report | Response |
|---|---|---|---|---|
| 2026-01-03 | External safety lead | v0.2.1 archive, v0.2.0 demo | Cold-Start Audit | Response |
| 2026-01-03 | Link integrity auditor | v0.2.1 site | Link Integrity Audit | Response |
| 2026-01-03 | Acquisition auditor | v0.2.2 site | Hostile Audit v0.2.2 | Response |
| 2026-01-03 | Epistemic integrity auditor | v0.2.2 archive, v0.2.3 demo | Epistemic Integrity Audit | Response |
Legacy Status Labels (Pre-v0.2.2 Archives)
Archives published before v0.2.2 may display a Status: CURRENT label in their HTML, even though they are now superseded. This is expected behavior due to archive immutability.
- Pre-v0.2.2 archives embedded status at build time
- Archived HTML files cannot be modified after publication (immutability requirement)
- The fix introduced in v0.2.2 shows
Status: LOCKEDand defers to/versions/
- A client-side banner is injected into legacy archive pages via Cloudflare Pages Functions
- The banner links to
/versions/for canonical status - No archived files are modified; injection happens at runtime
See Legacy Status Banner for technical details.
Questions?
For technical questions about this verification process, see the Hostile Demo Rehearsal document which addresses common skeptical questions with prepared answers.