AI helps write the code. mathema checks what that code actually guarantees, proving it mathematically where it can and gathering executable evidence where it can't. It's a System 0 engine: no model in the loop, and nothing leaves your machine.
$ pip install mathema
$ mathema audit your_package
# map every function: claimed, provable, tested
$
AI has made code cheap to produce. Knowing it is correct is still expensive, and as generation speeds up, review becomes the bottleneck. mathema adds a verification layer between AI-assisted code and trusted systems.
mathema turns what a function is meant to do into explicit claims and checks them against the real code, by proof where it can and by evidence where it cannot, so shipping faster stops meaning knowing less. Verification is what turns AI-assisted code into value you can rely on.
A test checks the inputs someone chose to write down. It does not establish behaviour beyond them, and generated tests can inherit the biases of the model that wrote the code.
A claim states what should be true. mathema determines whether it is proved, supported by evidence, or falsified, and gives you the counterexample when it fails.
mathema complements your test suite rather than replacing it: existing tests continue to count toward your implementation score.
Put-call parity says a call minus a put on the same
strike equals S - K*exp(-r*T), whatever the volatility. Here
it is checked two ways against the same Black-Scholes pricer.
1 point checked. Every other input is unknown, and hoped for the best.
pytest -q → 1 passed
It confirms parity at S = 100, K = 100, r = 5%, T = 1 year, σ = 20%. Move any one of those and the test has nothing to say.
Every point Every possible input, proved mathematically.
mathema check → 1 proven
A symbolic proof, from the code itself, covers every combination of S and K from 50 to 150, r from 0 to 10%, T from 0.1 to 2 years and σ from 5% to 80%. Leave the range out and it finds the input that breaks the code instead: T = -1.
The function is not a simple one: a logarithm, a square root,
exponentials and the Gaussian CDF through math.erf, with the
volatility threaded through both legs. Parity says all of it collapses to
S - K*exp(-r*T), and a proof has to show exactly that.
[ options.py ]
import math
def put_call_parity_gap(s: float, k: float, r: float, t: float,
sigma: float) -> float:
"""A European call minus a European put, both priced by Black-Scholes."""
root_t = math.sqrt(t)
d1 = (math.log(s / k) + (r + 0.5 * sigma * sigma) * t) / (sigma * root_t)
d2 = d1 - sigma * root_t
phi = lambda z: 0.5 * (1.0 + math.erf(z / math.sqrt(2.0)))
call = s * phi(d1) - k * math.exp(-r * t) * phi(d2)
put = k * math.exp(-r * t) * phi(-d2) - s * phi(-d1)
return call - putThe test passes. One point, one comparison, limited knowledge.
$ pytest -q 1 passed in 0.82s
[ test_options.py ]
import math
from options import put_call_parity_gap
def test_parity_at_the_money():
gap = put_call_parity_gap(100, 100, 0.05, 1.0, 0.2)
assert math.isclose(gap, 100 - 100 * math.exp(-0.05))[ mathema ]
mathema finds where the code breaks. Claims read like
mathematics, and f stands for the function being checked,
here put_call_parity_gap. Stated with no range, the claim
covers every real input, and the counterexample is a negative maturity,
where math.sqrt(t) raises.
$ mathema check options.py --claim "f(s,k,r,t,sigma) == s - k*exp(-r*t)" FAIL options.put_call_parity_gap: source, no side effects; claims 1/2 adjudicated (0 proven, 0 holds, 1 falsified, 1 skipped) <- 1 falsified claim(s)[ the record ]
FALSIFY parity: f(s, k, r, t, sigma) = -k*exp(-r*t) + s counterexample s = 1, k = 1, r = 1, t = -1, sigma = 1
State the range, and mathema proves it everywhere in it. Not by sampling: the error-function terms in the two legs cancel symbolically.
$ mathema check options.py --claim "for s in [50,150], k in [50,150], r in [0.0,0.1], t in [0.1,2], sigma in [0.05,0.8], f(s,k,r,t,sigma) == s - k*exp(-r*t)" ok options.put_call_parity_gap: source, no side effects; claims 1/1 adjudicated (1 proven, 0 holds, 0 falsified)
For verifying claims: no LLMs no hallucinations no token costs
A second model reviewing the first can share its blind spots. mathema is a System 0 engine, so the check stays independent of whatever wrote the code.
Under the hood it is built on symbolic algebra: SymPy for exact proof, an SMT solver (z3) as an optional further decision procedure, and a suite of algorithms that turn code into mathematics and handle the places where an implementation can go wrong, from folding loops and solving for poles to interval evaluation and checks for overflow, numerical stability and how a value is represented.
Not another model. No LLM is involved in verifying a claim. Verdicts come from proof and from running the real function, so the same evidence stands however the code was written.
Agents propose. They can't adjudicate. Verification happens outside the agent, and accepting a result stays a human decision, kept off every agent and MCP surface.
Runs on your machine. No account, no upload, no API key, no telemetry. Your source never leaves the laptop or the CI runner it lives on.
Nothing to pay per verification. With no model in the loop, running mathema on every commit costs compute you already have, and every counterexample names the exact inputs, ready to paste into a REPL.
mathema is a System 0 engine implementing Claim-Driven Development (CDD): state what a function should do, then keep a machine-checkable record of whether the real implementation satisfies it. The method is published as the open Claim-Driven Development spec, so any tool can read the same records.
A claim sits beside the code, like f(-x) == -f(x) or
min(x) <= f(x) <= max(x), in a docstring, a
decorator, a claims file or a type annotation. Your coding assistant
can write them too.
Where the function lifts into algebra, mathema proves the claim over the whole declared domain. Where it doesn't, it runs the real function against the claim and keeps any counterexample it finds.
Every record is bound to a hash of the function's structure, so when
the code changes its evidence goes stale instead of silently staying
trusted, and mathema verify re-checks only what moved.
Works with your tests, types, CI and coding agents. More in the docs:
Tests tell you what ran. mathema measures what has been claimed, verified and pinned down, as three scores reported in your terminal and in CI. Each is measured on its own, so a strength in one can't hide a gap in another.
The overall score is the area the three span, so it falls toward zero when any one of them is empty instead of averaging politely over the gap.
The share of statements reached by a test, a probe or a derive proof, taken together, so code proven symbolically counts even where no test calls it. Coverage reports are stamped by content hash, so lines from a stale report are left out rather than counted.
How much of what each function is meant to do is explicitly specified and up to date, so intent that lives only in someone's head, or in a prompt that was thrown away, shows up as a gap.
Of everything knowable about a function, how much its verified claims have settled: what it computes, what it accepts, its bounds and shape, how safely it runs and where it can go wrong. A proof counts for more than a sample, and a failure found is still knowledge.
A gate, not a dashboard. mathema verify re-checks
only the functions whose structure changed. A falsified claim exits 1 and
a broken invocation exits 2, so a pipeline can tell a real finding from a
broken run. mathema init --ci scaffolds the GitHub Actions
or GitLab step.
Scores you can diff. mathema badges writes the three
scores, the triangle and a per-function snapshot for each commit, so CI
can report how the picture moved. The scoring algorithm is versioned, so
a change in method never reads as a regression.
One function, one claim, and real output from a fresh install. The full walkthrough in the docs starts with a claim that fails, which is rather the point: mathema found the gap by looking, not by being told where to look.
$ pip install mathema $ mathema audit your_package
def discounted(price: float, rate: float) -> float:
"""The price after applying a discount rate.
Claims:
never_raises_price: for price in [0, 1e6], rate in [0, 1], f(price, rate) <= price
"""
return price * (1 - rate)$ mathema check pricing.py ok pricing.discounted: source, no side effects; claims 1/1 adjudicated (1 proven, 0 holds, 0 falsified)
We're looking for a limited number of commercial teams to shape where mathema goes next: verifying AI-assisted code across an organisation, not just a repository. It starts with a paid six-week design partner pilot, with forward-deployed engineers from Tetrion helping you get your first codebase verified with mathema.