# Tetrion Labs

> Tetrion Labs builds mathema, mathematical verification for AI-assisted code. mathema checks what code actually guarantees: you state claims about a function (for example `f(-x) == -f(x)` or `min(x) <= f(x) <= max(x)`), and mathema proves them mathematically where the function lifts into algebra, or runs the real function against them where it cannot, keeping any counterexample. No LLM is involved in verification, it runs entirely on your machine, and it needs no account or API key.

Built for: technology teams whose productivity gains in writing code aren't translating into better software, developers who don't trust vibe coding, and industries where accountability for decisions is paramount.

Key facts:

- Product: mathema, a Python package (`pip install mathema`), pre-1.0.
- Method: Claim-Driven Development (CDD). The CDD specification is published under CC BY-SA 4.0: https://github.com/aaronbyrnephd/claim-driven-development
- System 0 engine: a verification engine with zero models between the code and its verdict. mathema is a System 0 engine, built on symbolic algebra (SymPy, with z3 as an optional SMT decision procedure) and algorithms that turn code into mathematics and check where implementations go wrong (loop folding, pole solving, interval evaluation, overflow and numerical-stability checks). No language model is involved anywhere between the code and its verdict: for verifying claims, no LLMs, no hallucinations, no token costs.
- Verdicts: `proven` (mathematical proof over the declared domain), `holds` (sampled evidence, never reported as proof), `falsified` (a counterexample, kept in the record).
- Scores: implementation (statements reached by a test, probe or derive proof), intent (how much of what the code is meant to do is explicitly specified and up to date), clarity (how much of a function's knowable behaviour its verified claims have pinned down; technically, a score from the behavioural entropy the claims remove over their declared domain, relative to what remains). The overall score is the area the three span.
- Licensing: mathema is source available under the Business Source License 1.1. Production use is free for organisations under USD 10 million in revenue, for up to three repositories, for non-commercial use, and for a 90-day evaluation; commercial use beyond those needs a licence.
- Company: Tetrion Labs is a trading style of Tetrion Ltd, registered in England and Wales, company number 17398534.

## Docs

- [mathema documentation](https://mathema.tetrionlabs.com/): home
- [Install](https://mathema.tetrionlabs.com/install/): install and optional extras
- [Quick start](https://mathema.tetrionlabs.com/quickstart/): one function from a falsified claim to a proven one in five minutes
- [See what mathema finds](https://mathema.tetrionlabs.com/findings/): four short functions that pass review, and what mathema reports
- [Claim-driven development](https://mathema.tetrionlabs.com/cdd/): the method and verdict vocabulary
- [The evidence ladder](https://mathema.tetrionlabs.com/evidence-ladder/): how proof and sampled evidence are kept apart
- [Intent, implementation and behaviour](https://mathema.tetrionlabs.com/three-layers/): the three scores
- [The claim grammar](https://mathema.tetrionlabs.com/grammar/): everything a claim can say
- [The MCP interface](https://mathema.tetrionlabs.com/modes/mcp/): using mathema from a coding agent
- [Licensing policy](https://mathema.tetrionlabs.com/licensing-policy/): free-use thresholds and commercial licences

## Background

- [The bottleneck moved](https://tetrionlabs.com/why/): why rolling out AI coding tools moves the bottleneck from writing code to reviewing it, and what mathema does about it

## Commercial

- [Design partner pilot](https://tetrionlabs.com/pilot/): a paid six-week design partner pilot for commercial teams, and how to buy a commercial licence
- Contact: contact@tetrionlabs.com