Stelling

An assertion-based verifier for JAX array programs — inspired by Kani for Rust. Prove stated properties of traced computations over declared input regions, with a stamp on every verdict naming its own assumptions.

stelling is not affiliated with or endorsed by the JAX project.

JAX silently narrows integer constants during tracing

x = jnp.int8(100)
y = x + 256          # you wrote 256

The jaxpr — the trace JAX actually executes — contains:

add a 0:i8[]         # JAX silently made it 0

No error. No warning. Verify it yourself: jax.make_jaxpr(lambda x: x + 256)(jnp.zeros(1, jnp.int8)) prints add a 0:i8[] — the 256 is gone. (full reproducer)

Six mechanisms were measured against it (numpy_dtype_promotion("strict"), enable_checks, debug_nans, debug_infs, np.errstate(over='raise'), warnings.simplefilter('error')) and all six leave it silent. checkify.all_checks returns None on it while its out-of-bounds and divide-by-zero controls throw.

Check your existing test suite with a single flag

pip install stelling
pytest -p stelling.overflow

The tripwire hooks the exact site where the value dies and reports each narrowing with your source line, the arithmetic, an independent recomputation, and a one-line reproducer. It costs nothing until you switch it on — measured overhead is within noise over 60 cold traces.

Why this matters

A silently wrapped constant does not crash. The program runs, the loss decreases, the simulation looks healthy. The integer you wrote and the integer in the trace are different numbers, and nothing told you. This is relevant anywhere JAX traces integer arithmetic:

• Quantized inference — a scaling factor or zero-point that wraps produces outputs in the wrong numerical range, silently
• Finite-volume solvers — a grid constant or stencil coefficient that wraps causes the discretisation to converge on a physically impossible state
• Sensor pipelines — an ADC offset or calibration constant that wraps inverts the measurement, and downstream checks pass because they verify the traced program, not the written one
• Control systems — an actuator limit or safety threshold that wraps can suppress a protective action

If you then verify a property of that trace — "output stays within bounds" — the verifier is correct about a program you did not write. A VERIFIED over a corrupted trace is worse than no verification at all: it actively suppresses the signal that something is wrong.

The tripwire detects this at trace time, and the static verifier refuses to certify a trace it flagged — the verdict is UNKNOWN with a note naming what was narrowed. A VERIFIED with the tripwire armed is a statement that the trace is faithful to what was written AND that the property holds.

Where Stelling fits

These tools are complementary. checkify catches runtime faults stelling cannot see; jaxtyping catches shape mismatches at definition time; stelling catches the trace-time value corruption both are blind to and proves properties neither attempts.

Quickstart — prove a property

import jax
jax.config.update("jax_enable_x64", True)
import jax.numpy as jnp

from stelling.harness import any_array, assert_
from stelling.preconditions import check


def harness():
    # ANY float64 array of 8 elements, every element in [0.1, 10.0]
    a = any_array((8,), jnp.float64, (0.1, 10.0))
    a_face = 0.5 * (a + jnp.roll(a, -1))          # your own construction
    return assert_(a_face > 0.0)                  # the obligation


v = check(harness, vacuity_mode="inputs-only")
print(v.status)
print("semantics :", v.stamp.semantics.split(":")[0])
print("solver    :", v.stamp.solver.reason)
print("nonvacuity:", v.stamp.nonvacuity)
print("coverage  :", v.stamp.coverage)

prints:

VERIFIED
semantics : real (ℝ)
solver    : no solver invoked: escalation was NOT ATTEMPTED (solver_timeout_ms not set); every obligation was judged by outward-rounded interval arithmetic alone
nonvacuity: UNCHECKED — no membership conditions declared
coverage  : 9 eqns: 8 known (89%); 1 transparent

VERIFIED here is about every array the declaration admits, not a sample — and the stamp says in what arithmetic, with what help, over how much of the query, and whether anyone has tied the declared box to data you actually run on. v.render() prints the whole stamp.

Full walkthrough: docs/quickstart.md

Installation

pip install stelling              # zero dependencies; never touches JAX
pip install stelling[solvers]     # adds both SMT backends (cvc5 + z3)

Stelling has zero required dependencies. JAX and the SMT solvers are opt-in extras, imported lazily on first use, so a bare install never touches the JAX (or CUDA stack) already managing your environment:

Installing one backend rather than both does not weaken what a verdict claims — it removes the cross-check behind every discharge, and the verdict discloses that itself. Measured, in both directions: docs/choosing-a-solver-backend.md.

At runtime Stelling always uses whichever JAX is importable in your environment — the [jax] extra is bootstrap convenience plus a documented tested-version floor, not a binding. [all] deliberately excludes jax: the extra people type reflexively must never let the resolver touch a working jax install (a bump can desync CUDA plugin wheels). Nothing is vendored; both solver backends install from their official PyPI wheels on Linux, macOS, and Windows.

python -m stelling prints which optional dependencies are installed and runs a one-formula smoke test against each available solver.

cvc5: wheel vs external binary

The cvc5 extra installs the official PyPI wheel — the non-GPL "BSD version" build. Verified against cvc5 1.3.4: the wheel bundles libpoly, so the cylindrical-algebraic-coverings solver (nl-cov) that nonlinear real arithmetic leans on is fully functional. What the wheel lacks is the cvc5 CLI and the GPL-gated performance components — CLN (exact-arithmetic speed), glpk-cut-log (LP acceleration), and CoCoALib (Gröbner-basis speedups inside coverings, finite-field theory). The official GitHub release binaries are built the same way (libpoly yes, GPL components no), so a source build with ./configure.sh --gpl --auto-download is the only route to those.

To point stelling at a different cvc5 — a nightly, a distro or custom build, or (if you genuinely need the GPL components) your own source build:

export STELLING_CVC5=/path/to/cvc5   # or just put `cvc5` on PATH

Plainly: the near-term value of the external-binary route is nightlies and alternative builds, and the SMT-LIB 2 subprocess transport it rides on is the same one a later dReal-style backend will use. The GPL source build is a documented possibility, not an expectation — nobody does it casually. Either way, an external solver stays a separate program you chose to install: nothing links into stelling, and its Apache-2.0 licensing is unaffected. python -m stelling reports both transports, including which optional components a discovered binary was built with.

What it does — and what it doesn't, measured

Does:

• Checks stated box invariants on continuous flows (edge-flux inductiveness): the harness declares bounded inputs (any_array), obligations (assert_), and membership of known data in the declared set (nonvacuity) — all as traced primitives, so the query's content hash covers the declarations, not just the program.
• Forward interval propagation over the jax-free IR (stelling.ir), outward-rounded (one deliberate ulp per operation), with three-valued verdicts: VERIFIED, REFUTED (set-level: the stated box is not invariant — not a witness), UNKNOWN (our imprecision, never guessed away).
• Checks the preconditions your solver assumes — positivity of a coefficient field over its envelope, a nonzero mass/shift scalar over its admissible config range — as reusable obligation templates (stelling.preconditions) with a one-call front door (check()), each verdict stamped. Guide: docs/preconditions.md.
• Escalates undecided obligations to SMT solvers (optional extras, never required): scalar linear/polynomial obligations emit as SMT-LIB2 text — exact dyadic rationals, the closed declared box, the negated predicate — routed by fragment through a portfolio (cvc5 with coverings for nonlinear, Z3 as cross-check). Agreement decides; disagreement is a loud error, never a silent pick. sat becomes REFUTED with a concrete witness, checked for box membership and predicate violation by exact-rational replay before it is believed; timeout or unknown stays UNKNOWN — a timeout is never a VERIFIED; unsupported fragments stay UNKNOWN with the reason quoted.
• Every verdict carries a full stamp: stelling and jax versions, query content hash, arithmetic representation and semantics, precision configuration, solver — recorded absence when intervals decided alone, or every invocation (name, version, transport, exact option set) when escalation ran — nonvacuity, the tier and provenance of every transfer used, its assumptions, and ⊤-coverage — including constraints that were dropped, which are counted and named, never hidden.

Doesn't (yet, and the stamp or the docs say so in each case):

• Derive invariants. Check mode only: you state the box, stelling judges it. Derive mode is designed and deliberately unbuilt.
• Handle cond / scan / while. Control flow falls to ⊤ and is counted as such in coverage.
• Say anything about discrete steps. Every verdict so far is about the continuous flow; a solver's stepped trajectory is a different object, and no artifact here blurs them.
• Judge in float semantics by default. The default stamp says real: obligations are judged in exact real arithmetic, and a predicate can hold in ℝ while failing in floats — that gap held a 258-day bug upstream, which is why the stamp names its semantics per verdict. An opt-in ieee mode now judges the censused binary64 behaviours (rounding collapse, overflow-as-value, NaN) and stamps itself; it treats subnormal-band outcomes as indeterminate (measured: this CPU target flushes subnormals; others may not), declines non-binary64 floats with the gap quoted, and refuses solver escalation (the SMT backends speak ℝ). Every counted or recorded verdict to date is a real-mode verdict.
• Discharge the recorded incidents. Against the 20 long-horizon failures this project mined from public trackers, hand proofs discharged 0 of 3 attempted; the box invariants it checks are preconditions of arguments, not incident closures (design/supply-probe.md, design/layer-probe.md).

The roadmap (design/founding.md) aims it further: index safety, and bounds over horizons no test can reach.

Disclaimer and recommended practice

Stelling is open-source software provided as-is under the Apache-2.0 license, with no warranty of any kind. A VERIFIED verdict is a statement about a mathematical model under stated assumptions — it is not a guarantee about your deployed system, and the stamp exists precisely to name the gap between the two.

Do not rely on any single tool for safety-critical decisions. Stelling is one layer in a verification stack, not a replacement for the others:

• Testing (pytest, unittest) — exercises concrete inputs and catches regressions no static tool looks for
• Property-based testing (hypothesis) — generates adversarial inputs and finds edge cases no author anticipated
• Runtime checking (jax.experimental.checkify) — catches OOB, NaN, and division by zero at execution time, which stelling does not attempt
• Type checking (jaxtyping, mypy, pyright) — catches shape and type mismatches at definition time
• Code review and domain expertise — the only instrument that can judge whether the declared envelope matches the physical system

We are actively working to make stelling as correct and useful as possible, and we disclose its limitations in every verdict it produces. If you find a defect, please report it.

Documentation

Development

pip install -e ".[solvers,jax]" --group dev   # pip ≥ 25.1; uv works too
pre-commit install                            # SPDX headers, REUSE, import hygiene
pytest

[jax] here assumes a fresh venv. It is in this line because a contributor's clean environment needs jax to run the suite. If you are installing into an environment that already has jax, drop it — use ".[solvers]" --group dev instead. The extra exists only to bootstrap an environment with no jax at all, and letting it into a resolver that is already managing your jax can desync CUDA plugin wheels.

Every source file carries an SPDX header (template in .license-header.txt); the pre-commit hook inserts it into new files automatically. Commits must be signed off (git commit -s) — see CONTRIBUTING.md and DCO. Two import rules, both enforced by hooks and tests: (1) only stelling/_jax_compat.py may spell import jax / from jax — the churn boundary; (2) jax._src is banned everywhere except one pinned file (_tripwire/_adapter_jax.py, which reaches the private constant-fold registry via importlib.import_module). Everything else consumes the jax-free stelling.ir.

License

Apache-2.0 for the code; marks reserved. All source is Apache-2.0 — deliberately no NOTICE file: nothing is vendored, so there is no attribution to propagate (one gets added the day third-party code actually lands in-tree). The stelling name and logo (assets/) are not under the code license: they are marks of the maintainer, reserved so a fork cannot be mistaken for the project (LICENSES/LicenseRef-stelling-marks.txt). Nominative use — referring to stelling by name or logo — is fine and expected. This is the same source-open/marks-reserved split Ferrocene ships, not an open-core arrangement, and it is consistent with Apache-2.0, whose §6 grants no trademark rights anyway.

No solver is a required dependency, and none is linked or vendored. The SMT backends are optional extras — separate wheels you opt into — and an external cvc5 binary is driven as a separate process over SMT-LIB2 text. Nothing solver-shaped is compiled into, vendored into, or derived into stelling. This is true by measurement, not just policy: the full test surface passes in an environment with no solver installed at all; verdicts that used no solver stamp that absence explicitly, and verdicts that escalated stamp every invocation — solver, version, transport, and the exact emitted option set.

Provenance is machine-verifiable: the repo is REUSE-compliant (reuse.software; LICENSES/, REUSE.toml, reuse lint in CI), contributions are DCO-signed, and releases are published via PyPI Trusted Publishing with PEP 740 attestations (SECURITY.md shows how to verify). The verdict trust policy lives in SOUNDNESS.md.