Verification · 2026-07-10
Trust surface
When Vanyx marks a Lean proof ✓ VERIFIED / GOLD, the kernel audit must only depend on the axioms below. Anything else is UNSOUND or incomplete — including sorry and custom axiom declarations.
Trusted Lean axioms
- propext
- Classical.choice
- Quot.sound
Sourced from lib/trust/axioms.ts — the same set the verifier imports. If this page and the verifier disagree, that is a bug.
Compiler-trust (never GOLD)
- Lean.ofReduceBool
- Lean.ofReduceNat
- Lean.trustCompiler
These appear when a proof uses native_decide-style paths. Flagged honestly — they trust the compiler, not the kernel alone.
What we refuse
- Calling a result verified when no machine check actually ran
- Minting GOLD from tool checks that are not Lean kernel proofs
- Publishing failed attempts / reward traces on the open Ledger
- Promising monetary Campaign payouts while escrow is off