Skip to content

user_guide.md

Latest commit

 

History

History
76 lines (54 loc) · 3.04 KB

user_guide.md

File metadata and controls

76 lines (54 loc) · 3.04 KB
Raw

User guide

What LeanVerifier does

LeanVerifier checks one property for affine binary classifiers defined over exact rationals:

If |score(x)| > ε · ‖w‖₁ with ε ≥ 0, then every input in the closed L∞ ball of radius ε around x receives the same classification as x, where classification is true iff score > 0.

What it does not do

  • It does not verify neural networks, transformers, or vision models.
  • It does not claim floating-point or PyTorch equivalence.
  • It does not expose a web upload interface (legacy path is quarantined under experimental/legacy-formalverifml/webapp/).
  • Insufficient margin is not-certified, not a proof of vulnerability.

Install

From the repository root (https://github.com/fraware/leanverifier):

# Lean library (once per machine / after toolchain changes)
lake update
lake build

# Python CLI (frozen lockfile)
uv sync --frozen --all-extras

Requires Lean v4.32.1 (see lean-toolchain) and Python 3.11+.

Inputs

  1. Model JSON conforming to schemas/model.schema.json (canonical rational strings).
  2. Request JSON conforming to schemas/request.schema.json (reference input, ε, model digest).

See model-format.md. Worked example: examples/affine_binary/.

CLI

uv run leanverifier validate-model examples/affine_binary/model.json
uv run leanverifier validate-request examples/affine_binary/request.json
uv run leanverifier generate --model examples/affine_binary/model.json \
  --request examples/affine_binary/request.json --out-dir /tmp/lv-out
uv run leanverifier verify --model examples/affine_binary/model.json \
  --request examples/affine_binary/request.json \
  --output /tmp/lv-evidence
uv run leanverifier inspect /tmp/lv-evidence

verify requires --output. It builds in an isolated temporary workspace under the pinned toolchain, runs the axiom audit, then writes an immutable evidence bundle (canonical inputs, generated Lean, logs, axiom report, result, checksums) before deleting the temp workspace.

Exit codes

Code Meaning
0 verified
2 not-certified (e.g. insufficient margin)
3 invalid input / schema
4 Lean build failure
5 axiom audit failure
6 digest mismatch
7 internal error
8 timeout

Reading results

The evidence bundle under --output is the authoritative record. verification-result.json includes claim, digests, generator version, Lean toolchain, mathlib revision, build/audit exit codes, axiom audit status, and evidence_bundle_digest. Use leanverifier inspect <dir> to recompute digests and reject tampering (--rerun optionally re-executes verify). Treat verified as certification of the concrete margin instance only — not deployment readiness or floating-point correctness.

Further reading