mathema

Know what your code actually guarantees.

AI has changed the cost of producing code without changing the cost of knowing whether that code is correct, and so more of it now arrives than anyone can review line by line. mathema adds a verification layer between AI-assisted code and trusted systems: you state what a function is supposed to do as an explicit claim, and mathema checks it against the real function, proving it outright where the mathematics permits and gathering reported evidence where it does not. What comes back is a durable record of what has been established, how, and whether it still applies to the code in front of you.

Nothing is asserted and nothing is quietly upgraded. Evidence remains evidence, proof remains proof, and a claim that nothing could settle remains unresolved and says so.

mathema is a System 0 engine: a verification engine with zero models between the code and its verdict. Every result comes from mathematics and from running the real code, never from a model's judgement, so there are no LLM tokens to pay for, no account or API key, and your code never leaves your machine.

The name is Greek: μάθημα, a thing learned.

Why it matters: The bottleneck moved, on how AI moves the bottleneck from writing code to reviewing it, and what mathema does about it.

See it in action

Here is a European call minus a European put on the same strike, both legs priced by Black-Scholes, with a square root, a logarithm, an exponential and the Gaussian CDF expressed through math.erf:

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 collapses to S - K*exp(-r*T), whatever the volatility, which is a surprising thing to say about a function where sigma appears five times. State it as a claim over the region it should hold on:

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

Everything before the last comma is the domain and everything after it is the law, with f standing for the function under test. [0.1,2] is a mathematical interval rather than a two-element Python list, so the claim covers every real value in it, and mathema lifted the body to a symbolic expression in which both Gaussian terms cancel and sigma disappears, establishing the identity for the whole region at once. The second row is that proof's [float] companion, a separate claim that runs the same identity through the real code in floating point at the region's corners and across its interior, because a proof is about the mathematics and whether the implementation keeps up with it in f64 is a different question, answered here by holds. The claim grammar has the full notation.

The domain is doing real work: drop it and the same claim comes back falsified, with a counterexample at a negative maturity where math.sqrt(t) raises, because a claim with no domain covers every real input, including ones the function was never meant to take. A claim without its domain is a different claim, and mathema says so rather than assuming the range you had in mind.

Proof is not the same as testing

A test demonstrates behaviour at the inputs you chose, and a property-based test at many inputs you did not, but neither can say anything about the uncountably many points of [0.1,2] it never visited. mathema keeps its verdicts apart so you always know which kind of answer you have:

Guarantees and limits states what each verdict establishes and what it does not, in one place.

The same distinction reaches claims no amount of test-running could establish. Four defining properties of the logistic function include a limit at infinity and an improper integral over the whole real line, and all four come back proven, with a fifth row for the symmetry identity's [float] companion (the calculus claims spawn none, having no point to execute). The two identities carry a range because this code overflows below about x = -709.78, and stated over the whole line mathema falsifies them there:

import math

def logistic(x: float) -> float:
    return 1.0 / (1.0 + math.exp(-x))

mathema check sigmoid.py \
    --claim "for x in [-700, 700], d(f(x), x) == f(x)*(1 - f(x))" \
    --claim "for x in [-700, 700], f(-x) == 1 - f(x)" \
    --claim "lim(f(x), x -> oo) == 1" \
    --claim "∫(d(f(x), x), x, -oo, oo) == 1"

ok   sigmoid.logistic: source, no side effects; claims 5/5 adjudicated (4 proven, 1 holds, 0 falsified)

When the code is wrong

Proving a good function correct is the easy half, and the question that matters more is whether a bad one gets caught. Here is a discount factor with a pole hiding in it, checked with no claims at all, only mathema's built-in laws:

import mathema

def discount_factor(x: float) -> float:
    """A discount factor that divides by one minus the rate."""
    return 1 / (1 - x)

print(mathema.check(discount_factor))

mathema.Record(discount_factor) · source, no side effects · form ebb4c9b87847
  FALSIFY monotonic_increasing[x]: d(f(x), x) >= 0
           counterexample x = 1
  FALSIFY even: f(-x) = f(x)
           counterexample x = -1
  proven  is_deterministic: f(x) = f(x)
  proven  is_defined: 1 - x != 0
  FALSIFY is_pole_safe[x]: is_pole_safe(x)
           counterexample x = 1 is admitted by the declared domain but sits at or beside a pole: the call raised ZeroDivisionError
  FALSIFY is_representation_safe[x]: is_representation_safe(x)
           counterexample x = 1 (the int spelling) is admitted by the declared domain but the call raised ZeroDivisionError
           [implementation:representation]

(trimmed from fourteen claims). The pole was not found by luck: uniform random sampling lands exactly on x == 1 with probability zero, so a property-based run can pass a thousand trials here and report nothing, whereas mathema solves the lifted expression for where the denominator vanishes and makes sure that point is tried. Every falsification rests on an executed witness, never on a symbolic argument alone, and the bracketed tag marks an implementation that fell over (the integer 1 raising where the domain admits it). is_defined reads the other way round: it states the region on which f returns, and 1 - x != 0 is exactly that region.

Built for AI-assisted development

An agent can write the code and propose the claims, but mathema reserves the decisions that turn a verdict into an accepted fact for a person, so the agent never gets to mark its own homework:

agent proposes a claim
        ↓
mathema adjudicates it against the real function
        ↓
a person accepts the verdict            (mathema accept)
        ↓
the function is locked                  (mathema lock)

No tool exposed over MCP accepts a verdict from its caller, and claim expressions are validated against a strict AST whitelist before they run, so a claim from an untrusted source can do no more than evaluate mathematics over the function (the function itself runs as it would in its own tests; see Security and execution). mathema accept prints the exact write before making it, and lets a person accept evidence as sufficient, own a residual risk explicitly, or correct a claim the falsification showed was wrong (the correction is itself adjudicated first). An agent may lock a function it has finished; only a person can unlock one, behind a prompt and optionally a PIN, with deliberately no --yes flag.

Verification that survives code changes

Every verdict binds to the exact code that earned it, through two identity hashes: form, over the AST structure with names and formatting normalised away, and sig, over the parameter shape. mathema.write_spec writes the record as standalone YAML under .mathema/verified/, and mathema verify later re-checks every record whose function, or a function it depends on, has changed since, so a verification result cannot quietly outlive the implementation it describes the way a test result does the moment nobody re-runs it. A locked function fails verification the moment its body changes, though docstring edits stay allowed.

mathema is fully offline: nothing in checking, verifying or recording makes a network call, so none of this sends your source or your claims anywhere. The one command that fetches anything is the explicit, opt-in mathema init --agents, which clones the skills repository.

Audit a codebase you didn't write

mathema audit reads a whole package without running anything and gives every function a row: its location as a ready-made sed -n line range, its branching, whether it carries claims, whether the derive route could prove things about it, the state outside its parameters it reads or writes, whether a test report covers it, and how well its docstring states its intent.

mathema audit --index writes the same map to .mathema/index.yaml, with each module's stated intent and every function's file, line and span, which is the fastest way to hand an agent a codebase without letting it grep its way around.

Beyond tests

None of these replaces the others, and mathema complements your test suite rather than replacing it: the lines your tests already reach count toward the implementation score. mathema's probe route is the same idea as Hypothesis, CrossHair's symbolic execution is the nearest thing in Python to its derive route, and contract libraries such as icontract and deal check pre- and postconditions as the code runs, which complements a claim rather than competing with it. What mathema adds is the place where a property check, a real proof attempt and a durable record meet on the same claim, with the claim routed automatically to whichever method the function's shape can support, and skipped reported plainly the moment none can.

Measuring a codebase

A codebase can have every line exercised by tests while having very little of its intent stated or verified, so mathema measures those separately rather than folding them into one coverage number. mathema badges reports three scores, each measured on its own so a strength in one can't hide a gap in another:

• implementation, coverage that counts proofs: 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;
• intent, what the code is meant to do, stated: 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;
• clarity, how much of the behaviour is pinned down: of everything knowable about a function, how much its verified claims have settled, where a proof counts for more than a sample and a failure found is still knowledge.

They are drawn as a triangle whose area is the overall score, so it falls toward zero when any one of them is empty instead of averaging politely over the gap. An illustrative example:

        CLARITY 50
              ◆
             · ·
            ·   ·
           ·     ·
          ·       ·
         ·         ·
        ·           ·
       ·      ●      ·
      ·     ···       ·
     ·    ······       ·
    ·   ········        ·
   ·  ···········        ·
  · ·············         ·
 ·················         ·
●·············+···●·········◆
  IMPL 100           INTENT 26
        overall 32

Every line is exercised and intent is a quarter specified, which the area shows as 32 where the mean of the three would have said 59. The badges reference covers how each score is computed and what to expect of them.

API

import mathema

def ema(x: list, alpha: float) -> float:
    """Exponentially weighted moving average."""
    y = x[0]
    for v in x[1:]:
        y = alpha * v + (1 - alpha) * y
    return y

bounds = {"x": (-1e6, 1e6), "alpha": (-10, 10)}
mathema.check(ema, domain=bounds)                   # built-in laws, inside a stated domain
mathema.check(ema, claims=["f(x, 1.0) == x[-1]"])   # your own claim
mathema.check(ema, domain={"alpha": (0, 1)})        # narrow the domain
mathema.write_spec(ema, claims=[...])               # check, then write the record
mathema.status()                                    # fresh or stale, per tracked function

Without anyone reading the code, the first call proves that the result is deterministic and that scaling or shifting every element of x scales or shifts the result the same way, with the [float] companions of those proofs holding across the stated domain, and it finds that reordering x does not leave the result unchanged, with the counterexample kept. Leave the domain out and every claim ranges over all of the reals, where the companions report the overflow at 1e+308 instead. The API reference has the rest.

CI

A gate, not a dashboard:

mathema verify                  # the gate: re-checks what changed, fails on what broke
mathema review origin/main      # what a pull request changed, as claims and verdicts
mathema check model.py --format junit --output claims.xml   # reports for the CI UI

A failing 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, --format github, junit and json feed each platform's own reports, and fuller pipelines are in examples/ci/.

Intent

mathema exists to make the behaviour of a function something that can be checked rather than assumed, namely a claim about what the function does, stated precisely enough that the code can be held to it, with the result recorded as proof, as evidence, or as an open question, whichever is true, and kept honest as the code changes underneath it.

Install

mathema needs Python 3.10 or newer. Install it inside an active virtual environment (python3 -m venv .venv && source .venv/bin/activate, or your usual equivalent) rather than against a system Python:

pip install mathema           # core: the derive route and the spec store
pip install "mathema[all]"    # numpy, z3, MCP server, coverage

The extras can also be taken one at a time: mcp exposes mathema's tools to an agent, smt adds z3 as a fallback decision procedure, numpy enables array-shaped claims, coverage reads a native .coverage report and symbology adds conventional notation.

Documentation

• The bottleneck moved: why verification, not generation, is now the hard part of shipping AI-assisted code.
• Quick start: five minutes, one function, and a claim that goes from falsified to proven.
• Claim-driven development: the vocabulary every mode assumes, including what separates proven from holds.
• The claim grammar: everything you can say in a claim, with a runnable example of each.
• The derive route: which function shapes can reach proven, and what happens to the ones that cannot.
• Case studies: put-call parity, the Greeks, and the sigmoid worked end to end.

The full documentation, including the command reference, is at mathema.tetrionlabs.com.

mathema is at 0.6.0 and pre-1.0, feature-complete for its current scope and covered by over 3,500 tests; the claim grammar and record format are settled by the spec, but the Python API is likely to change before 1.0.

Related projects

claim-driven-development is the specification mathema implements (v0.2: the claim tuple, the claim families and the YAML record schema), maintained independently under CC BY-SA 4.0, so anything that reads or writes that shape interoperates with mathema's records without importing it. mathema.SPEC_VERSION states the targeted version and every record stamps it. mathema-symbology renders claims in a field's conventional notation, and mathema-agents teaches coding agents to drive the claim loop properly, vendored by an explicit, opt-in mathema init --agents.

See also CHANGELOG.md, CONTRIBUTING.md, SECURITY.md and SUPPORT.md.

Licensing

mathema is source-available under the Business Source License 1.1. Production use is free when any one of these applies: your organisation's revenue is under USD 10 million, mathema is used in no more than three of its repositories, the use is research, teaching, personal or otherwise non-commercial, or it is within a 90-day evaluation. Every released version converts to AGPL-3.0-or-later four years after its release. See LICENSING.md for the plain-language version.