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.

Formal claim under validation (not Supported)

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).

Implementation exists; assurance is incomplete — see CLAIMS.md and STATUS.md. 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.1) 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

uv sync --frozen --all-extras
uv run leanverifier validate-model examples/affine_binary/model.json
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

Repository layout

LeanVerifier/          # Supported Lean library (checkout; mirrored into the wheel)
src/leanverifier/      # Supported Python package + CLI
src/leanverifier/resources/  # Packaged schemas, Lake project, axiom-audit script
schemas/               # Checkout mirror of packaged JSON schemas
examples/affine_binary/
tests/                 # unit, schema, integration, mutation, security
scripts/               # axiom audit, docs verification, wheel smoke, release helpers
uv.lock                # Frozen Python deps (runtime, dev, build)
docs/                  # guides + assurance case
experimental/          # Legacy FormalVerifML — not in supported build

Supported Lake targets must not import experimental/.

Documentation

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.