Metadata-Version: 2.4
Name: leancert
Version: 2.1.0
Summary: Formal verification for numerical Python code - powered by Lean4
Author: Alejandro Radisic
License-Expression: LicenseRef-LeanCert-Evaluation-1.0 AND Apache-2.0
Project-URL: Homepage, https://github.com/alerad/leancert-python
Project-URL: Documentation, https://docs.leancert.io/python/
Project-URL: Repository, https://github.com/alerad/leancert-python
Project-URL: Issues, https://github.com/alerad/leancert-python/issues
Keywords: formal-verification,theorem-prover,interval-arithmetic,neural-network-verification,lean4,mathematical-proofs
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: Operating System :: MacOS
Classifier: Operating System :: POSIX :: Linux
Classifier: Operating System :: Microsoft :: Windows
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Topic :: Software Development :: Quality Assurance
Classifier: Typing :: Typed
Requires-Python: >=3.10
Description-Content-Type: text/markdown
License-File: LICENSE
License-File: LICENSES/Apache-2.0.txt
License-File: LICENSES/LeanCert-Evaluation-1.0.txt
License-File: LICENSE_SCOPE.toml
License-File: COMMERCIAL.md
License-File: THIRD_PARTY_NOTICES.md
Requires-Dist: lean-runtime<3.0.0,>=2.0.7
Requires-Dist: numpy>=1.20.0
Provides-Extra: dev
Requires-Dist: pytest>=7.0; extra == "dev"
Requires-Dist: pytest-cov>=4.0; extra == "dev"
Requires-Dist: mypy>=1.0; extra == "dev"
Requires-Dist: ruff>=0.1.0; extra == "dev"
Provides-Extra: pytorch
Requires-Dist: torch>=2.0; extra == "pytorch"
Dynamic: license-file

# 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](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

```bash
pip install leancert
```

The wheel is pure Python. On the first checked operation, `lean-runtime`
downloads the compatible Bridge ready-to-run program from the
`ghcr.io/alerad/leancert-bridge-programs` program library. The program contains
the precompiled Bridge and its runtime libraries, not a Mathlib source/build
tree. Later calls reuse it; no Bridge path or system-wide Lean installation is
needed.

Full LeanCert and Mathlib environments are hydrated lazily only for independent
kernel replay, source rebuild audits, or custom registered-enclosure profiles.
Those environments remain distinct from ready programs in result provenance: a
program establishes `compiled_checker`, while successful exported proof replay
establishes `kernel_replay`.

Set `LEAN_RUNTIME_AVAILABILITY=required` when CI must use a downloadable
environment, or `LEAN_RUNTIME_AVAILABILITY=local` to audit the source-build
path. An explicit `LEAN_RUNTIME_LIBRARIES` value replaces the SDK defaults,
including an empty value to disable environment-library lookup.

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](docs/semantic-ast.md).
The typed line-protocol negotiation and checked-response invariants are
documented in [Python protocol model v2](docs/protocol-v2.md).
The semantic claim front door is documented in
[Unified checked proving](docs/prove.md).
Verified bounds from Bridge Contract 2.1+ can also be exported as
[independently rebuildable Lean evidence](docs/export.md).
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.
Bridge Contract 2.5 adds fixed, replayable scalar-root checks for existence,
uniqueness, and exclusion on exact rational intervals.
Bridge Contract 2.6 adds exact polynomial integral equalities and replayable
one-sided integral bounds with fixed checked partitions.
Bridge Contract 2.7 adds replayable strict global bounds backed by an exact
interior margin and the existing checked non-strict Golden Theorems.
Bridge Contract 2.8 adds [profile-bound downstream enclosure rules](docs/registered-enclosures.md)
with immutable registry negotiation and candidate-free fixed replay.

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

```bash
leancert verify exported_proofs/ --require-trust kernel
```

After installation, `leancert doctor` checks the managed environment,
negotiated contract, replay support, adaptive checked route, and runtime-owned
execution provenance.

## Quick Start

```python
import leancert as lc
from leancert import ast

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

# A Solver keeps one managed Lean process alive for the whole batch. The first
# proof prepares it; subsequent proofs normally reuse it in milliseconds.
with lc.Solver() as solver:
    result = solver.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 = solver.prove(
        ast.all_of(x >= 0, x <= 1),
        where={x: (0, 1)},
    )

    # Compare two expressions directly; export retains this original theorem.
    comparison = solver.prove(x <= x + 1, where={x: (0, 1)})

    # Strict targets retain an exact interior checked bound for replay.
    strict = solver.prove(x < 2, where={x: (0, 1)})

    # Independent conjunction children are routed and retained separately.
    combined = solver.prove(
        ast.all_of(x**2 <= 1, ast.sin(x) <= 1),
        where={x: (-1, 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 = solver.prove(
        ast.eventually(3 / n**2 <= Fraction(1, 1000), variable=n)
    )

    # Prove that one—and only one—root lies in the supplied interval.
    unique = solver.prove(ast.unique_root(x, variable=x, within=(-1, 1)))
    if isinstance(unique, lc.VerifiedUniqueRoot):
        # Preparing files is cheap. Pass verify=True, or run `leancert verify`
        # later, to hydrate dependencies and independently rebuild the proof.
        unique.export_lean_project("verified-unique-root", verify=False)

    # Exact polynomial integration and checked one-sided bounds.
    area = ast.integral(x**2, x, 0, 1)
    exact_area = solver.prove(ast.eq(area, Fraction(1, 3)))
    bounded_area = solver.prove(area <= Fraction(1, 2))
```

## Neural Network Verification

Verify properties of neural networks across entire input domains:

```python
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

The checked `ast` + `prove` route currently supports arithmetic plus `sin`,
`cos`, and `exp`. Other constructors exposed by the legacy expression API are
capability-gated and may return `Unsupported`; their presence in Python does
not imply that the negotiated Bridge can certify them. See the
[current capability notes](https://docs.leancert.io/python/proving/)
for the exact distinction.

## 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](https://docs.leancert.io/python/)
- [Python SDK Repo](https://github.com/alerad/leancert-python)
- [Lean Core Repo](https://github.com/alerad/leancert)
- [Bridge Binaries Repo](https://github.com/alerad/leancert-bridge)
- [Examples](https://github.com/alerad/leancert-python/tree/main/examples)

## Development tests

`pytest` runs the Bridge-independent suite by default. Tests that launch a real
managed Lean process are explicit because a cold run may download and build
large dependencies:

```bash
pytest                         # fast/default suite
pytest -m integration          # managed-Bridge integration suite
```

## License

Post-baseline v1 Python SDK material is source-available under the provisional
[LeanCert Evaluation License 1.0](LICENSES/LeanCert-Evaluation-1.0.txt).
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](COMMERCIAL.md) for the
commercial boundary and [LICENSE_SCOPE.toml](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](LICENSE),
[LICENSES/LeanCert-Evaluation-1.0.txt](LICENSES/LeanCert-Evaluation-1.0.txt),
and [LICENSES/Apache-2.0.txt](LICENSES/Apache-2.0.txt).
