Home

The problem

AI made code cheap. Verification didn't.

Tests pass. CI is green. The agent says done. But what do you actually know?

Traditional metrics tell you how much code you have. Test coverage tells you how much of it you executed. mathema tells you where your knowledge of the code ends.

The gap

Passing tests don't tell you what you know

A passing suite says the code did what the tests asked at the inputs the tests chose, which is worth a great deal and is still a narrow slice of what anyone reviewing the code actually wants to know. It says nothing, on its own, about:

• how the function behaves at the inputs nobody wrote a test for, which mathema samples and, where the mathematics permits, proves over the whole declared domain;
• the properties that follow from the implementation whether or not anyone intended them, such as symmetry, monotonicity or boundedness, which mathema checks with no claims written at all;
• the assumptions a result silently relies on, which a claim has to state as a domain or an assuming premise before it will check;
• where the behaviour becomes undefined, such as a pole, a raise or a non-finite result, which mathema looks for deliberately rather than hoping to stumble on;
• whether the docstring still describes the code, which mathema docsync reports as drift;
• whether a change has invalidated something established earlier, including through a function it depends on, which mathema verify catches by re-checking every record whose code or dependencies moved;
• and what remains unverified, which mathema reports as plainly as what it has proven.

How it works

Give your code an evidence layer

You state what a function is meant to do as a claim, a short mathematical statement such as f(-x) == -f(x). mathema adjudicates that claim against the real function by the strongest route the function's shape allows, and keeps a record of what was established, how, and against exactly which version of the code.

Tests you already have count toward what is known about each line of code, probes run the real function on inputs chosen to find trouble, and proofs settle a claim for every input at once where the function can be read as mathematics. The record that comes out is plain YAML, bound to a hash of the function's structure, so it can be reviewed, diffed and re-checked long after the conversation that produced the code has gone.

Strength of evidence

Evidence isn't binary

A claim that held on a thousand random inputs and a claim that holds on every input are different kinds of knowledge, and mathema never lets one pass for the other. Every verdict carries the route that reached it:

Verdict	What it means
proven	settled mathematically, for every input in the declared domain
holds (n=...)	survived exactly n trials against the real function, with inputs chosen by analysis where possible
falsified	a counterexample, found by running the function and kept permanently
unknown / skipped	not settled, with the reason in the record

Nothing is asserted and nothing is quietly upgraded. Evidence remains evidence, proof remains proof, and an unresolved claim remains unresolved. The evidence ladder sets out every rung, and Guarantees and limits states what each verdict does and does not establish. The same rule holds for this site: every output on it was produced by a real run, and the test suite parses every claim these pages show, so a claim cannot quietly fall out of the grammar.

A worked finding

See what mathema finds

Here is a midpoint function of the kind that gets written, reviewed and merged every day, and the test someone wrote for it:

def midpoint(a: float, b: float) -> float:
    """The point halfway between a and b."""
    return (a + b) // 2

from mid import midpoint

def test_midpoint():
    assert midpoint(2, 8) == 5
    assert midpoint(0, 10) == 5

python -m pytest -q test_mid.py

1 passed in 0.00s

The developer's claim is that the midpoint lies between its two inputs, which is the whole point of a midpoint. mathema checks that claim twice, once over the integers the test happened to use and once over the real numbers the type hints promise:

import mathema
from mid import midpoint

print(mathema.check(midpoint, claims=[
    mathema.claim("for a in [0, 100] subset Z, b in [0, 100] subset Z, "
                  "min(a, b) <= f(a, b) <= max(a, b)", name="between_integers"),
    mathema.claim("for a in [0, 100], b in [0, 100], "
                  "min(a, b) <= f(a, b) <= max(a, b)", name="between_reals"),
]))

mathema.Record(midpoint) · source, no side effects · form py:cc66f89ce3e7
  proven    between_integers: for a in [0, 100] : int, b in [0, 100] : int, min(a, b) <= f(a, b) <= max(a, b)
           for a in [0, 100] : int, b in [0, 100] : int
  between_reals  for a in [0.0, 100.0] : float|missing, b in [0.0, 100.0] : float|missing, min(a, b) <= f(a, b) <= max(a, b)   falsified: min(a, b) <= f(a, b) fails at a = 99.9999, b = 100
    falsified  computation  for a in [0.0, 100.0] : float, b in [0.0, 100.0] : float, min(a, b) <= f(a, b) <= max(a, b)   counterexample link 1: min(a, b) <= f(a, b): a = 99.9999, b = 100: 99.9999 vs 99.0
    holds      policy       f(a=nan)   no missing policy stated; assumed propagates
    holds      policy       f(b=nan)   no missing policy stated; assumed propagates

So the test established that the function works at two integer points. mathema established that over the integers it is correct everywhere in range, as a proof rather than a sample, and that over the reals it is wrong: floor division throws away the fraction, so the "midpoint" of 99.9999 and 100 is 99, below both of them. Nothing about this bug is exotic, and nothing in the test suite could have found it, because the suite only ever asked about integers. The fix is one character, and mathema proves it:

def midpoint(a: float, b: float) -> float:
    """The point halfway between a and b."""
    return (a + b) / 2

mathema check mid.py:midpoint --claim "for a in [0, 100], b in [0, 100], min(a, b) <= f(a, b) <= max(a, b)"

ok   mid.midpoint: source, no side effects; claims 4/4 checked (1 proven, 3 holds, 0 falsified)

One claim, four lines under it in the full record. The mathematics line is the proof over the real numbers. The computation line runs the same claim through the real code in floating point, at the region's corners and at sampled points inside it, and holds. The two policy lines cover a value that is not there: a float may be nan, nothing in the claim says what midpoint should do with one, so mathema assumes the nan passes through to the result (it propagates) and checks that it does.

A whole codebase

The Monday-morning audit

mathema audit answers the question anyone asks on their first morning with a codebase, namely where to start, without running a single test. Every function it can find gets a row: where it lives as a ready-made sed -n range, how branchy it is, whether it carries any claims, whether the derive route could prove things about it, what state outside its parameters it reads or writes, whether any test report covers it, and how well its docstring states its intent. Here is one module of mathema's own source:

mathema audit mathema.intent --root .

                         ||             || derive route                                                        || typing                || globals                                                                  ||           || docs    ||
key           | span     || claims      || derives | cx | reason                         | code                || typed | finite_domain || vars                      | mutates | funcs                              || tested    || quality || docsync
mathema.intent
 ._references | 92:145p  || {5 | 0 | -} || no      | 15 | 9 branches, 3 loops (1 nested) | loop:multiple-loops || yes   | -             || _REF_SECTIONS, _URL, _DOI | -       | re                                 || no-report || 0/4     || 50%
 ._sections   | 67:73p   || {5 | 0 | -} || no      | 2  | 1 loop                         | loop:not-a-fold     || yes   | -             || _SECTION                  | -       | -                                  || no-report || 0/3     || 50%
 ._summary    | 76:80p   || {5 | 0 | -} || no      | 2  | 1 loop                         | loop:not-a-fold     || yes   | -             || _SECTION, _GOOGLE_HEADER  | -       | -                                  || no-report || 0/2     || 44%
 .parse_doc   | 148:162p || {5 | 0 | -} || no      | 4  | 2 branches, 1 loop             | loop:not-a-fold     || yes   | -             || KEYWORDS                  | -       | DocIntent, _sections, _summary, +1 || no-report || 2/3     || 40%

0/4 claimed, 0/4 derivable, 0/4 derive reads with nothing supplied, 4/4 fully typed, 2/12 docstring quality criteria met, no coverage.json/.coverage report found, 4/4 depend on state outside their own parameters (see the global_vars/unresolved columns), mean docsync 46%.
`derives` is what the derive route can do here, given the domain the signature, docstring and claims declare. The reason/code cells describe what derive reads with nothing supplied, so a branch:needs-domain row reads blocked there and derives all the same, once a claim declares the domain that prunes the branch. Neither is a ceiling: a probe claim can still be written and checked for every function here.

sed -n 149,163p mathema/intent.py prints parse_doc and nothing else, which is what makes the table useful to an agent as much as to a person: it can go from "where is the function that parses a docstring" to the exact lines in one step. mathema audit --index writes the same map for a whole codebase to .mathema/index.yaml, with each module's stated intent, every function's file, line and span, and a pointer to its verified record where one exists.

Agents and people

Let AI write the code. Don't let it define what correct means.

A claim outlives the implementation it describes: when an agent rewrites a function, the claims about it are re-checked against the new code, and if one breaks you know which, where and with what counterexample. Where behaviour cannot be established, mathema says where it stopped rather than guessing.

What an agent may not do is decide what counts as correct. No tool mathema exposes to an agent accepts a verdict from its caller, and the decisions that turn a verdict into an accepted fact about your codebase, accepting evidence as sufficient, owning a residual risk, or declaring that a falsification revealed a wrong claim rather than a bug, go through mathema accept, which is a person at a terminal. Set a PIN the agent does not know, and every such decision needs it and is stamped in the record as made by someone who knew it, which the agent cannot be.

Settled code can be frozen at the level that matters, the individual function. mathema lock pins a function's structure, after which any change to its body fails the sweep, while docstring edits and every other function in the file stay free:

def discounted(price: float, rate: float) -> float:
    """The price after applying a discount rate."""
    return price * (1 - rate)

mathema lock pricing.discounted

locked pricing.discounted at form py:d2ab6eef1b84
the body can no longer change under a CDD loop; docstring edits are unaffected. A human unlocks with: mathema unlock pricing.discounted

and after someone changes 1 - rate to 1 + rate,

def discounted(price: float, rate: float) -> float:
    """The price after applying a discount rate."""
    return price * (1 + rate)

the next sweep stops on it (an excerpt):

$ mathema verify
FAIL pricing.discounted: locked at form py:d2ab6eef1b84 but the code is now py:53f9c55de50b; there is no record to compare. Restore the function, or a human runs: mathema unlock pricing.discounted

With a record in place the line says the record is unchanged instead, and the record stays as it was.

An agent is allowed to lock a function it has finished, which narrows what it can break on its next pass. Only a person can unlock one, behind a prompt with no --yes flag and, when set, the PIN.

System 0

No model in the loop

In the familiar framing, a language model answering at once is System 1, fast and fluent, and a reasoning model working through steps is System 2, slower and more deliberate. Both generate, and both can be wrong in ways that read as right. mathema sits underneath them as a System 0 engine, a verification engine with zero models between the code and its verdict: it generates nothing, guesses nothing and spends no tokens. Everything it concludes comes from reading the function's syntax tree, doing algebra on what it finds, and running the real code on inputs it chooses, the same kind of deterministic machinery as a compiler or a test runner. Its only required dependencies are sympy and pyyaml.

That changes what a verdict is worth next to an agent. The agent cannot talk mathema round, because there is no prompt to talk to; the answer depends on the code and the claim and nothing else. A check costs CPU seconds rather than tokens, so it runs on every commit in CI, offline, on a machine with no account and no API key. And the same code, claims and version give the same verdicts on every run: sampling is seeded, and the one thing that can vary between machines, whether a proof finishes inside its time cap, is written into the record whenever the cap was hit, so a holds that would have been a proven on a quieter machine says so.

A claim the ordinary proof attempt leaves undecided does not stop there. On the default route, best, it goes on to a ladder of genuinely different strategies, each given a time cap of its own: exact root isolation for polynomial differences, interval refinement over the domain, a gallery of equivalent rewrites, a library of changes of variable, and z3's nonlinear real arithmetic when the smt extra is installed, followed by one more try of the ordinary attempt at 15 seconds. Behind all of that sits a failsafe: whatever happens, the ladder stops at 45 seconds, so a single claim can never hold up a run indefinitely. A proof found this way records its route as derive:extensive, so the extra effort is visible in the record. When a proof matters more than the time it takes, extensive=True asks for more, at real cost: it gives the same ladder to a claim pinned to the derive route, widens the time caps, and makes probing search harder for the critical points worth sampling. It changes where the probe looks, never how many points it runs.

That is the division of labour the rest of this page assumes. Let a model propose the code and the claims, which is what models are good at, and let something that cannot be persuaded decide which of them are true.

Who it's for

One engine, several jobs

• If you check numerical code, your own or the pandas and numpy calls inside it: checking a numerical library function.
• If you maintain a codebase with a test suite: adding claims to an existing codebase.
• If you run CI: gating a pipeline with mathema verify.
• If you work alongside a coding agent: building with a coding agent.

Case study

A harder case

The same machinery reaches much further than a midpoint. Here is a European call minus a European put on the same strike, both priced by Black-Scholes, with a square root, a logarithm, an exponential and the Gaussian CDF:

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 on the same strike."""
    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 - put

Put-call parity says that difference is s - k*exp(-r*t) whatever the volatility, a surprising thing to claim about a function in which sigma appears five times:

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 7/7 checked (1 proven, 6 holds, 0 falsified)

proven, over every point of a five-dimensional region of prices, rates, maturities and volatilities: mathema read the body as mathematics, both Gaussian terms cancelled, and sigma disappeared. Of the six holds, one is the proof's computation line, the same identity run through the real code in floating point, and five are policy lines, one for a nan in each argument. No number of test cases could establish that. The case studies go on to the Greeks, stated as the partial derivatives they are.

Direction

Where this goes

Direction, not current capability

Each thread below starts from what mathema does today, then says where it is heading. The heading part is direction: nothing beyond what the linked pages document is a feature of the current release.

One claim, every implementation

A claim is a statement about mathematics, not about Python, and claims transfer already checks an implementation in another language against its Python original. The direction is for a claim written once to hold wherever the behaviour it describes is implemented.

Implementations generated from proofs

Once a behaviour is proven, the proof is a precise statement of what the code must compute. The direction is to derive a reference implementation in another language from that proven form, and then hold it to the same claims through the same equivalence machinery, so generated code arrives with its evidence attached rather than asking to be trusted.

A ledger for whole systems

Today the record is per function and per repository: every verdict bound to the code that earned it, every acceptance with its author and reason, nothing deleted when a belief turns out wrong. The direction is the same ledger at the scale of a codebase and the systems it runs in, the sign-offs, acceptances and behavioural claims across many repositories and services, over years, so an organisation can answer what it has established about its software, on what evidence, and who agreed, without reconstructing it from commit logs.

Linear algebra as a first-class subject

mathema already reads matrix structure, symmetric, orthogonal, positive definite, and proves identities such as det(A @ B) == det(A) * det(B) over whole families of matrices. The direction is deeper: eigenvalue and decomposition claims, conditioning and numerical stability stated as claims, and matrix calculus, so the code at the heart of optimisation and machine learning can be held to the mathematics it implements.

Complex analysis

Identities over the complex plane already prove: for f(z) = z*z, the claim for z in C, f(-z) == f(z) is settled for every complex z. The direction is the analysis itself, analyticity, branch cuts, poles and residues, and contour integrals, which is where signal processing, control and much of physics actually live.

Each of these widens what can be stated and proven, while the rule stays the same as it is today: evidence remains evidence, proof remains proof, and whatever cannot yet be settled says so.

Start

Stop measuring how much code you have. Measure how much you know about it.

pip install "mathema[all]"

Install Read the quickstart