Click on "Deploy Server".
Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state.
In the chat, type @ followed by the MCP server name and your instructions, e.g., "@certo prove the AM-GM inequality in examples/amgm.py"
That's it! The server will respond to your query, and you can continue using it as needed.
Here is a step-by-step guide with screenshots.
Between having a mathematical idea and having a proof of it there is a lot of work that is not proving. certo does that work — find the object, break the claims that are false, measure what survives, reduce it to what it really is, and assemble the rest — and every step comes back with a certificate anyone can re-check without trusting certo.
CLI and MCP. Fifty-four commands. Runs in milliseconds where a formalisation costs hours.
Español: README.es.md · run any command with --lang es.
the didactic introduction: what certo is for, in one page, in both languages | |
all fifty-four, one entry each: the question, the spec, the certificate, and what it does not establish | |
the DSL: every spec type with a minimal working example, shared options, exit codes | |
why they are the centre, the fifty-three kinds, which re-check without a solver | |
real problems end to end: symmetry, sweeps, parametric bounds, packings, toric data | |
status against verdict, the four optimisation claims that look alike, | |
what it does not do, and the FAQ | |
one problem, seven commands, fifteen seconds |
The lab instrument: find a contradiction fast, learn which hypotheses are redundant, exhaustively validate a finite case, bracket a constant with a certificate, synthesise a candidate over a bounded domain.
It is not a proof assistant — that is Lean, Rocq or Isabelle — nor a computer algebra catalogue. What it does not do matters as much as the command list.
The division of labour, in a user's words after a real session: certo finds and certifies the small trades; the human proof explains why they assemble globally without double-counting.
Phase | What you ask | What comes back |
Find | Is there an object like this? What is the best one? | the object itself — and with |
Break | Is this claim actually true? | a counterexample with concrete values, in milliseconds |
Measure | Not whether it fails — how much, and where is it worst? | exact min, max and mean, and the extreme instances by name |
Reduce | Ninety counterexamples. How many objects is that really? | orbits under your symmetry, and one minimal witness per orbit |
Establish | Is it true for every case, every | DRAT proofs, induction with the chain checked, Farkas multipliers, Gröbner cofactors, sums of squares, rigorous enclosures |
Assemble | What does my whole project rest on, and what do I still owe? | the proof with every bridge named, and a report of what is still assumed |
A verdict you cannot re-check is a rumour. Everything here produces an artefact, and most of them check without a solver at all.
Related MCP server: jacobian
Requires Python 3.11+.
pip install "certo-math[mcp,numerics]"The import package and the commands are certo, not certo-math:
from certo import Spec, certo prove spec.py. Only the distribution
carries the longer name, because certo alone is a crowded word.
From a checkout instead:
git clone https://github.com/jtraverso/certo-math
cd certo-math
pip install -e ".[mcp,numerics]"Dependencies: z3-solver and pulp, both of which ship their binaries. The
extras are mcp for the MCP server and numerics for bounds and sos
(python-flint, mpmath, numpy, clarabel and highspy); without them you
get the CLI, minus rigorous numerics and sums of squares, and LPs solved by
starting CBC rather than by HiGHS in-process. polyhedra (pycddlib)
makes semigroup decide with the facets of the cone instead of searching; it
has wheels only for Windows, and elsewhere builds against cddlib and GMP.
Check it works:
certo doctorOptional tools, none installed automatically and none needed to start:
Tool | What for | Without it |
| enumerating graphs | Python engine, comfortable to n=8 |
|
| our own CDCL, correct but slow |
| second opinion on DRAT proofs | the built-in Python checker suffices |
|
|
|
| the Gram search behind | nothing — |
certo doctor says which of these you have and what each gap costs, which
is the part a checklist of red crosses leaves out.
certo core examples/amgm.pyPROVED -- symbolic and universal under the hypotheses [unsat]
hypotheses needed: a_pos, b_pos, c_pos | redundant: noiseEvery file in examples/ carries in its docstring what it does
and what to expect. Lost? certo commands prints the routing table below in
your terminal, in your language.
Every command returns a certificate, or says explicitly why not. Never a bare "yes".
Seven result states: unsat, sat, unknown_solver, timeout,
resource_exhausted, out_of_theory, explored. Only the first two are
conclusive. The next four all mean "no answer", but for different reasons,
and collapsing them is expensive: an LLM that reads "unknown" writes "no
solution exists". explored is a cheap look (--explore), not an answer:
nothing was certified.
Determinism by work budget, not by clock: rlimit in Z3 and
conflict_budget in SAT. This covers our engines, not your predicate: if
your sweep predicate calls scipy or CBC, that part is outside the
guarantee.
Read docs/SPECS.md, or call the dsl_guide MCP tool,
before writing a spec.
Find the command by the question, not the name:
docs/COMMANDS.md, or certo commands.
Run certo lint on every spec before
running it. It is the cheapest thing in the tool and it catches the
contradictory regime, the empty family and the 10⁹ domain.
Read the verdict, not the exit status. unknown_solver is not
"does not exist".
Certificates are written to disk and do not travel in an MCP response.
Call verify with the path you are given.
Running more than a handful of questions? Use the in-process API, not a loop over the CLI: the startup dominates, and a fallback written to avoid it is a fallback in floating point.
Grouped as certo commands groups them. Full entries,
with what each one does not establish, in
docs/COMMANDS.md.
Command | What it does | Engine | Certificate |
| Negate the claim, look for | Z3 | unsat core, or counterexample |
| Satisfiability; | Z3 | model, or core |
| MUS: which hypotheses are needed | Z3 | minimal core |
| Does every hypothesis earn its place, or is the theorem overstated? | Z3 | verdict per hypothesis, each with the assignment that breaks it |
|
| exact LP | Farkas certificate, solver-free |
| Assemble lemmas into one proof, checking the join | Z3 | proof: every lemma, its certificate, and the link |
| Base cases + a step, and the check that the chain joins | Z3 | induction: both halves, and the two numbers that matter |
| CEGIS: ∃obj ∀input ∃aux | CEGIS/Z3 | object + the counterexamples that forced it |
| LP/ILP, or a packing | CBC | dual in exact rationals = the load certificate |
| A discrete skeleton searched, the continuous part certified | CBC + exact LP | mixed design: assignment, exact dual, and a bound |
| The exponent of | exact Laurent | the exponent, solver-free |
| A numeric inequality, rigorously ( | Arb or mpmath | enclosure in exact rationals |
| Polynomial systems: refute them, or certify what follows | Gröbner, ours | cofactors, checked by expanding |
| Remove a variable from two polynomials; keep the condition on the rest | Sylvester + Bareiss | Res = A·f + B·g, solver-free |
| A bound for EVERY value of a parameter, from a dual you already have | weak duality, symbolic | y and the shifted residuals, solver-free |
| The best INTEGER choice for a family of concave quadratics, and the value there | exact, no search | the maximiser and two step inequalities, solver-free |
| "By symmetry": the three hypotheses of the averaging argument, checked | exact, no search | generators, orbits and the quotient, solver-free |
| Exact integer linear algebra: rank, determinant, Hermite and Smith | unimodular transforms | U, V and their inverses, checked by multiplication, solver-free |
|
| exact elimination, Smith | the solution and the system, one product to check; an obstruction when there is none |
| A partition of a program, and the equivalence it induces | exact counting | the class data and both regularities, solver-free |
| Local toric data: primitivity, multiplicity, the height functional, discrepancies | exact det and solve | the numbers two geometric theorems consume, solver-free |
| An LP over every clique of a graph, without listing the cliques: column generation with a pricing search the verifier reruns | exact rational arithmetic | solver-free |
| A parameter domain covered by boxes, each certified by | every piece re-verified, the covering recomputed cell by cell | names the uncovered sliver, solver-free |
| Affine semigroups as a checker: pointedness, minimality, and membership of the cone, the group and the semigroup | exact integer and rational arithmetic | refutes normality with a witness, never asserts it, solver-free |
| How an optimum responds to ONE capacity across an interval: a piecewise-affine function, not a value | exact rational arithmetic | decides |
| The largest of ten thousand linear programs, and why nothing beats it | exact LP | the winner and a dual for the rest, solver-free |
| A fraction inequality for EVERY n | exact polynomials | the cleared numerator and the sign of the denominator, solver-free |
| Is the expected number of bad events below one, so a good object exists? | exact rationals | the moment and the mass it leaves over, solver-free |
| Where a sequence first crosses a line, and by how little | exact rationals | the prefix and the two terms that bracket it, solver-free |
| Does one exist at all, and the refutation when it does not | own CDCL | model, or DRAT proof |
| Is this an exact cover? A clique partition is one case | counting | the universe and the parts, solver-free |
| A polynomial is non-negative, as a sum of squares | numeric + exact rounding | rational squares, solver-free |
| Primality, or a factorisation | Pratt | modular-exponentiation tree |
| SAT with a verified DRAT proof | own CDCL or external binary | DRAT proof |
| Non-isomorphic graphs with filters | nauty or Python | canonical list + hash |
| Predicate and/or value over a family or ANY finite domain | nauty or Python | family + predicate certificates |
| Minimise a counterexample (graph or MUS) | CDCL / reduction | minimality witness |
| A constant's threshold | prove or cases | the pair that brackets it |
| The admissible interval of one variable over the regime, not one point of it | exact LP dual | a Farkas combination at each end, solver-free |
| A parameter that depends on itself: compose the growth classes and close the loop | growth ladder | the chain, its classes and the one comparison, solver-free |
| Tie a certificate to the Lean declaration meant to justify it, and check it does | Z3 entailment | the hypothesis, the statement, and whether one covers the other |
| Check a spec before spending the compute on it | — | — |
| Where a proof stands: proved, owed, hollow, stale | — | — |
| What this install can do, and what each gap costs | — | — |
| Whose bug is it -- certo's, the spec's or the machine's -- and a local folder to file it with. Sends nothing | — | — |
| One entry point: load a spec and run whatever it asks for ( | — | whatever the command produces |
| Which command answers which question | — | — |
| Bundle spec, certificates, versions and hashes for a referee | — | the bundle |
| Run an | re-run certified | the certificate of the certified run |
| Thousands of certificates into one zip with a manifest, each member readable alone | — | the archive; |
| Which certo MCP servers are running old code after a reinstall; | — | — |
| Re-verify a stored certificate | — | — |
| Spec to SMT-LIB2/DIMACS, or a linear Farkas certificate to Lean | — | — |
| Audit log of what was run | — | — |
Common options, after the subcommand: --json, --cert FILE, --lang,
--timeout-ms, --rlimit, --max-memory-mb, --seed.
Exit codes: 0 conclusive, 2 inconclusive, 1 invalid certificate,
3 error. What each status and verdict means is in
What a result means.
The hard limit is asymptotic statements with quantifiers over n. "There
exists N such that for every n ≥ N, every graph…, the loss is ≤ εn²" is
not decided by this tool.
Question |
|
Is R(3,3) ≤ 6? | Yes. |
Is R(3,3) = 6? | Yes. |
Is R(5,5) ≤ 48? | Not in practice. Finite, but the space is 2^903 |
Does R(k,k)^(1/k) converge? | No, in principle. Asymptotic: not expressible |
The full list, and the FAQ, in docs/LIMITS.md.
A CLI costs one Python startup per question. On a Windows laptop that is
1.2 s before certo is imported — python -c pass alone — against ~70 ms
of certo's own. A sweep of 853 linear programs is two minutes of work behind
twenty minutes of starting Python.
from certo import LPSpec, api
spec = LPSpec(sense="max", title="w")
...
res = api.run("opt", spec)
res.meta["objective"] # '32/3' -- an exact string, not a float
res.certificate # the artefact `--cert` would have written
| returns a |
| every command that takes a spec |
| what that command accepts, read off the engine |
run verifies what it produced and raises api.SelfCheckFailed rather
than hand back a certificate that fails its own verifier. That covers
solver-free certificates; one whose check calls a solver again (unsat_core,
model, …) comes back unchecked, with no meta["self_check"] — call
certo.verify on it when it matters. It costs under 1% of an opt. Pass
self_check=False only after measuring.
The engine modules under certo.engines stay private; run, runnable and
options are the promise. Commands that read a directory or the environment
(verify, status, doctor, enum, …) are not here — certo.verify and
certo.load_spec are already exported for the first two.
Every command exposed to the LLM, with no copy-pasting. The project ships a
ready .mcp.json; to register it by hand in Claude Code:
claude mcp add certo --env CERTO_WORKSPACE=. -- certo-mcpCERTO_WORKSPACE (the current directory by default) holds specs/ and
certs/. Every path is confined there.
Three design decisions:
Certificates do not come back in the response. A MUS takes 18× more on disk than the whole response, and the model cannot verify it by reading it. They are written to disk and the path, kind and digest come back.
Errors come back as data, not as exceptions. The SDK turns any
exception into Error executing tool X and swallows the reason; a model
reading that cannot fix its spec. Here it gets what happened and what to
correct.
dsl_guide first. Both a tool and a resource (certo://dsl).
Specs are Python code and they get executed when loaded. That is inherent to the DSL and it is the same level of trust an agent with file access already has. The server confines paths, but it is not a sandbox: do not point it at third-party specs.
certo doctor --register-mcp adds certo to .mcp.json in the current
directory, merging with whatever is already registered rather than
replacing it, refusing to touch a file that is not valid JSON, and checking
that the server actually starts — a different question from whether it is
registered, and the one people mean.
English is the default and the source of truth. Spanish ships as an overlay:
certo core examples/amgm.py --lang es # or CERTO_LANG=esTranslations live in src/certo/locales/ as JSON. A
missing key falls back to English, so a partial translation degrades instead
of breaking. To add a language, copy en.json, translate the values and keep
the {placeholders} — there is a test that enforces both invariants.
Two things deliberately stay English whatever --lang says, because they are
API surface rather than prose: command names and flags, and MCP tool
names and descriptions. Certificates store note keys, not rendered text,
so one issued in Spanish reads correctly for an English reader.
Over five hundred, no test framework required. The count is deliberately not given exactly: the previous README said 253 when there were twice that, and a number nobody recomputes goes stale.
for t in smoke mcp i18n extras adversarial determinism; do python tests/test_$t.py; donepython tests/run_examples.py runs all 65 example specs and verifies every
certificate they produce.
Release notes in CHANGELOG.md; what is planned, blocked and deliberately refused in BACKLOG.md.
MIT. The synthesis engine is a reimplementation of the CEGIS algorithm from marcelwa/CEGIS (MIT), not of its code.
This server cannot be deployed
Tamper-evident proof creation and verification for AI agents via MCP, A2A, and REST.
Physics-based validation of simulation results: receipts with per-check verdicts, via MCP.
MCP-native AI evaluation: rubric audits, eval suites, and proof reports for AI/LLM output.
Read-only Remote MCP for externally grounded AI agent trust receipts.
