LeanVerifier
LeanVerifier is a research technical preview for exact formal checks of affine binary classifiers over the rationals.
v0.1.0 target — not authorized for release. Read STATUS.md, CLAIMS.md, and SECURITY.md before use.
Supported claim (only)
Given a dimensionally valid affine binary classifier over exact rationals ℚ, a reference input (x), and a nonnegative L∞ radius (\varepsilon), if the absolute score margin strictly exceeds (\varepsilon \cdot |w|_1), then the classification sign (strictly positive score) is invariant on the closed L∞ ball of radius (\varepsilon) around (x).
This is not a general ML verification product. Neural nets, transformers, vision models, SMT automation, distributed or enterprise features, and the legacy web upload path are unsupported historical material under experimental/legacy-formalverifml/.
Quick start
Prerequisites
- Lean 4 matching
lean-toolchain(leanprover/lean4:v4.32.0) via elan - Python 3.11+ for the generator and CLI
- Docker (optional) for a Lean-only container build
Lean library
lake update
lake build
python scripts/audit_axioms.py
Python package / CLI
python -m pip install -e ".[dev]"
leanverifier validate-model examples/affine_binary/model.json
leanverifier verify --model examples/affine_binary/model.json --request examples/affine_binary/request.json
| Exit | 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 |
Repository layout
LeanVerifier/ # Supported Lean library
src/leanverifier/ # Supported Python package + CLI
schemas/ # Canonical JSON schemas
examples/affine_binary/
tests/ # unit, schema, integration, mutation, security
scripts/ # axiom audit, docs verification, release helpers
docs/ # guides + assurance case
experimental/ # Legacy FormalVerifML — not in supported build
Supported Lake targets must not import experimental/.
Documentation
| Doc | Purpose |
|---|---|
| STATUS.md | Program status and blockers |
| CLAIMS.md | Supported / experimental / planned / rejected claims |
| SECURITY.md | Supported surface and legacy web quarantine |
| CHANGELOG.md | Release notes |
| docs/user_guide.md | Operator guide |
| docs/developer_guide.md | Build, layout, contribution mechanics |
| docs/model-format.md | Canonical rational JSON |
| docs/assurance-boundary.md | In / out of scope |
| docs/trusted-computing-base.md | TCB inventory |
| docs/threat-model.md | Threats and controls |
| docs/limitations.md | Known limits |
| docs/release-process.md | RC and v0.1.0 authorization |
| docs/history/README.md | Withdrawn FormalVerifML materials |
Contributing
See CONTRIBUTING.md. On formal-kernel, schema, generator, workflow, and release PRs, the implementer must not be the sole designated reviewer.
Citation
See CITATION.cff. Prefer citing the specific commit or tag you evaluated.
License
MIT — see LICENSE.