LeanCert

v1 overhaul licensing: Post-baseline Python SDK work is source-available under a provisional evaluation license. Personal evaluation, non-commercial research, education, and bounded commercial, governmental, or other organizational proofs of concept are permitted; production and commercial use require written terms. Python SDK versions through v0.3.2-apache-final, LeanCert Core, and LeanCert Bridge remain separately available under Apache-2.0. See LICENSE.

Formal verification for numerical Python code, powered by Lean4.

Write Python, get mathematical proofs. LeanCert proves properties about your code for all inputs, not just test samples.

Installation

pip install leancert

That's it! The package includes pre-built binaries - no Lean installation required.

Bridge binaries are sourced from the decoupled leancert-bridge release tag pinned in bridge-version.txt.

The v1 overhaul also includes a bridge-independent, exact semantic model under leancert.ast. Its versioned encoding, binder rules, claim closure, and legacy conversion boundary are documented in Semantic AST v1. The typed line-protocol negotiation and checked-response invariants are documented in Python protocol model v2. The semantic claim front door is documented in Unified checked proving. Verified bounds from Bridge Contract 2.1+ can also be exported as independently rebuildable Lean evidence. Bridge Contract 2.3 extends the same workflow to unique nonlinear-system roots certified by exact rational Krawczyk certificates; NumPy and SciPy candidates remain untrusted inputs. Bridge Contract 2.4 adds exact reciprocal-power eventual bounds with supplied or automatically discovered natural-number cutoffs.

Exported projects can be audited without rerunning Python or numerical search:

leancert verify exported_proofs/ --require-trust kernel

After installation, leancert doctor checks the bundled binary, negotiated contract, replay support, adaptive checked route, and release provenance.

Quick Start

import leancert as lc
from leancert import ast

# Define an exact semantic claim
x = ast.var("x")
claim = ast.sin(x) <= 1

# Check it for every x in the closed interval [0, 1]
result = lc.prove(claim, where={x: (0, 1)})
if isinstance(result, lc.Verified):
    print(f"Verified claim {result.claim_id}")
    print(result.provenance)
else:
    print(type(result).__name__, result.reason)

# Two-sided claims use an explicit conjunction.
two_sided = lc.prove(
    ast.all_of(x >= 0, x <= 1),
    where={x: (0, 1)},
)

# Discover and certify a cutoff for every n at or beyond it.
from fractions import Fraction
n = ast.var("n", sort=ast.NATURAL)
eventual = lc.prove(
    ast.eventually(3 / n**2 <= Fraction(1, 1000), variable=n)
)

Neural Network Verification

Verify properties of neural networks across entire input domains:

import leancert as lc
from leancert.nn import TwoLayerReLUNetwork, Layer
import numpy as np

# Create/load a neural network
layer1 = Layer.from_numpy(
    weights=np.array([[2.0, -2.0], [-2.0, 2.0]]),
    bias=np.array([0.0, 0.0]),
    activation='relu'
)
layer2 = Layer.from_numpy(
    weights=np.array([[1.0, 1.0]]),
    bias=np.array([0.0]),
    activation='none'
)
network = TwoLayerReLUNetwork(layer1=layer1, layer2=layer2)

# Prove output bounds for ALL inputs in domain
verified = lc.verify_nn_bounds(
    network,
    {'x0': (-1, 1), 'x1': (-1, 1)},
    output_lower=-5,
    output_upper=5,
)
print(verified)  # True - proven for every possible input!

Key Features

• Checked Bounds: Typed LeanCert checker outcomes with exact provenance
• Neural Networks: Verify ReLU networks, transformers
• Root Finding: Locate and isolate roots with guaranteed correctness
• Integration: Compute integral bounds
• Independent Audit: Rebuild exported fixed certificates with leancert verify
• PyTorch Import: Load weights directly from PyTorch models

Supported Functions

sin, cos, tan, exp, log, sqrt, abs, sinh, cosh, tanh, atan, erf, sinc, and more.

Why LeanCert?

Traditional testing samples inputs: f(0.5), f(1.0), etc. You can never test f(0.7) and the infinitely many values in between.

LeanCert uses interval arithmetic to check properties for all inputs simultaneously. Every Verified result identifies the checker, Golden Theorem, verification route, numerical backend, and exact bridge build that accepted the certificate. Independently rebuildable Lean projects are a separate export milestone rather than an implicit claim of this runtime API.

Verified, Rejected, Unsupported, DomainObstruction, and Inconclusive are distinct outcomes. An enclosure that is too wide produces Inconclusive; failure to find a counterexample is never reported as proof. Bridge Contract 2.2 provides a separate typed adaptive certificate route backed by LeanCert's checked rational optimizer. It can close subdivision leaves that the fixed replayable checker cannot, but is not mislabeled as a replayable bound-check/2 certificate.

Links

• Documentation
• Python SDK Repo
• Lean Core Repo
• Bridge Binaries Repo
• Examples

License

Post-baseline v1 Python SDK material is source-available under the provisional LeanCert Evaluation License 1.0. Personal evaluation, education, non-commercial research, and a bounded 90-day commercial, governmental, or other organizational proof of concept are permitted. Qualifying nonprofit education and non-commercial research are not subject to that 90-day limit. Production deployment, commercial product development, customer services, and SaaS/API deployment require a separate written commercial license. Generated reports, certificates, and proof artifacts lawfully created during permitted use remain free to retain, publish, and use, including commercially; this does not grant continued rights to execute the SDK. See COMMERCIAL.md for the commercial boundary and LICENSE_SCOPE.toml for the authoritative source classification.

Python SDK material through commit 716cb2d, preserved by the tag v0.3.2-apache-final, remains available under Apache-2.0. LeanCert Core, LeanCert Bridge, and third-party components retain their separate licenses. See LICENSE, LICENSES/LeanCert-Evaluation-1.0.txt, and LICENSES/Apache-2.0.txt.