| name | audit-proof |
| description | Audit proof bundles — verify correctness, assess coverage, find gaps. Use when reviewing proofs for a system's requirements. |
Audit proofs
You are helping a reviewer who has received one or more sealed ProofBundle objects and needs to determine whether the proof collection is sound, complete, and honest about its limitations.
Your job is adversarial. You look for gaps — both within individual proofs and across the collection.
Two levels of audit
Level 1: Individual proof soundness
Is THIS proof correct? Are the axioms true? Are the advisories addressed?
Level 2: Collective coverage
Does the COLLECTION of proofs cover all the properties the system needs? What's missing? What falls in the gap between symbolic proof and real-world behavior?
Level 2 is where most failures live. A system can have five individually correct proofs and still fail because the sixth property — the one nobody proved — is the one that breaks.
Argument
The proof bundle(s), file(s), or system to audit: $ARGUMENTS
Workflow
Step 1: Enumerate what needs to be true
Before looking at any proofs, ask: what properties does this system need?
For a control system:
- Stability (open-loop and closed-loop)
- Controllability
- Observability
- Performance bounds (settling time, overshoot, steady-state error)
- Robustness (gain margin, phase margin, parameter sensitivity)
For a DeFi mechanism:
- Invariant preservation
- Rounding direction correctness
- Overflow safety
- Fee/slippage bounds
- Economic incentive alignment
For an optimization problem:
- Convexity of objective
- Feasibility of constraints
- Uniqueness of solution
- Conditioning (strong convexity parameter)
Write this list first. Then check which items have proofs and which don't.
Step 2: Map proofs to requirements
Property needed | Proof exists? | Bundle hash | Status
-----------------------|---------------|---------------------|--------
Closed-loop stability | YES | a3f2... | VERIFIED
Controllability | YES | 7c51... | VERIFIED
Observability | YES | fc89... | VERIFIED
Pointing error < 0.1° | NO | — | UNPROVEN
Robustness to ±20% J | NO (not symbolic) | — | NEEDS SIM
Discrete-time stability | NO | — | UNPROVEN
Gaps are more important than passes. Flag every UNPROVEN and NEEDS SIM entry.
Visualize the dependency structure across all proofs to reveal hidden coupling:
from symproof.export import proof_dag_mermaid
print("```mermaid")
print(proof_dag_mermaid(*all_bundles, expand_lemmas=False))
print("```")
If two "independent" proofs both import the same sub-proof, they're coupled through shared assumptions — if that sub-proof's axioms are wrong, both fail. The DAG makes this visible.
Step 3: Audit each proof individually
For each sealed bundle, re-verify and render:
from symproof import verify_proof
from symproof.export import latex_bundle
result = verify_proof(bundle.proof, trust_imports=False)
assert result.status.value == "VERIFIED"
print(latex_bundle(bundle))
The LaTeX view shows axioms, hypothesis, lemma chain with dependencies, and advisories in one readable document. Review the math directly — don't rely on metadata summaries.
For each proof, check:
Axioms (posited):
- Is each axiom actually true in the real system?
- Are any axioms too strong (assuming more than needed)?
- Are any missing (the proof holds in a wider space than intended)?
Axioms (inherited — inherited=True):
- Trace each inherited axiom back to its foundation proof via its
citation
- Does the
citation.source reference a real, verifiable result?
- Does the foundation's condition actually hold for THIS system?
- An inherited axiom means "the proof chain forced this condition" — it needs the same scrutiny as posited axioms, but the failure mode is different: the proof author may not have realized this condition exists
- The LaTeX export groups axioms into "Posited" and "Inherited" sections with citation sources — use this for review
Hidden axiom check (HIGHEST PRIORITY):
- Does any axiom have
expr=True? What external theorem does it represent?
- If a foundation proof exists: does
seal(foundations=...) pass? If not, what axioms are missing?
- If no foundation exists: what are the theorem's implicit conditions? List them. Are they valid for this system?
- Check the
[ASSUMPTIONS] advisories in proof_result.advisories — they enumerate every posited, inherited, and external assumption with citations
- Violation of hidden axioms — citing a theorem without checking its conditions — is the most common cause of "correct proof, wrong conclusion" failures in applied mathematics
Load-bearing symbol assumptions:
- Were axioms constructed under
unevaluated()? If not, symbol assumptions may have collapsed axiom expressions to True
- The load-bearing check in
seal() catches symbol assumptions that affect verification but aren't declared as axioms — review any such findings
Hypothesis:
- Does it match the stated requirement?
- Is the SymPy expression correct?
Lemma chain:
- What advisories exist? Each is a review item.
- Are dependencies (
depends_on, import_bundle) logically correct?
False-positive vectors:
- Domain-ignoring simplification (rational expressions with singularities)
- Vacuous truth (implication P→Q is trivially true when P is never satisfied)
- Symbolic vs numeric divergence (symbolic proof doesn't guarantee floating-point behavior)
Step 4: Assess the collection
Generate the expanded proof DAG to see the full structure with lemma-level detail:
from symproof.export import proof_dag_dot, proof_dag_mermaid
print("```mermaid")
print(proof_dag_mermaid(*all_bundles, expand_lemmas=True))
print("```")
This is the critical step. Ask:
Coverage: What percentage of needed properties have proofs? 100% symbolic coverage is rare — flag what needs simulation or testing instead.
Independence: Are the proofs genuinely independent, or do they share hidden assumptions? Two proofs using the same axiom set are coupled through those axioms — if an axiom is wrong, both proofs fall.
Layer completeness: symproof covers symbolic analysis only. For each proven property, ask:
- Does it also need simulation? (robustness, noise, finite precision)
- Does it also need code verification? (implementation correctness)
- Does it also need testing? (integration, hardware-in-the-loop)
Consistency: If multiple proofs share an axiom set, run check_consistency on any bundles that prove related claims. Contradictory proofs under the same axioms indicate a bug in the axiom set.
Step 5: Write the audit report
## Audit report: <system name>
### Coverage summary
- Properties needed: N
- Symbolically proven: M (with hashes)
- Unproven (needs proof): K
- Out of scope for symbolic analysis (needs sim/test): L
### Requirements traceability
| Requirement | Property | Proof hash | Verdict |
|---|---|---|---|
| REQ-STAB | Closed-loop stability | a3f2... | PASS |
| REQ-CTRL | Controllability | 7c51... | PASS WITH 1 ADVISORY |
| REQ-PERF | Pointing error | — | NO PROOF |
| REQ-ROB | Robustness | — | NEEDS SIMULATION |
### Individual proof assessments
(per-proof details: axiom review, advisory review, false-positive risk)
### Collection-level findings
- Axiom consistency: <assessment>
- Coverage gaps: <what's missing>
- Layer gaps: <what needs sim/test beyond symbolic proof>
### Recommendation
- Accept / Accept with caveats / Reject
- Specific actions needed before sign-off
What you do NOT do
- Do NOT assume a proof is correct because it says VERIFIED
- Do NOT assess individual proofs without first enumerating what needs to be true
- Do NOT sign off on "symbolic coverage" as "full coverage" — flag what needs simulation and testing
- Do NOT skip the collection-level assessment — individual correctness doesn't imply system correctness
