`mathema verify`¶

The test-runner face and the CI gate: sweeps the spec store, re-adjudicates every function whose form hash no longer matches its record (new or changed code), and refreshes the machine records so the next run has a baseline.

mathema verify [<key> | <claims file> ...] [--root .]

Given one or more store keys (canonical dotted module.qualname), the sweep is confined to exactly those records, re-adjudicating and re-stamping each in place. Freshness never skips a key you named: the form-hash short-circuit is an optimisation for a whole-store sweep, so asking about one key always re-checks it (this is the fix the integrity-mismatch warning points at): the single-key form the reconcile workflow points you at (mathema verify mypkg.mod.fn after a merge touched one record). With no key it sweeps the whole store as before. A key that names no record fails as a clear per-key problem line, exit 2.

Arguments¶

Flag	Meaning
`<key> ...`	zero or more store keys to confine the sweep to; omit for the whole store
`<claims file> ...`	a claims file path: every entry in it is adjudicated up front, a library's compendium file included (see Library claims)
`--root`	project root holding `.mathema/verified` and `claimspec.yaml` (default `.`)
`--all`	re-adjudicate everything, ignoring form-hash freshness
`--strict` / `--lenient`	one strictness pair shared with `check`; strict is the default here (CI gates a settled store), `--lenient` reports unverifiable claims and accepted risk instead of failing on them
`--status [TARGET]`	report fresh/stale per `@track_claims`-tagged function, adjudicate nothing, exit 0; an optional TARGET (dotted name or file path) is imported first so its tagged functions register
`--format`	`text` (default) or `json`: the whole sweep as data; per-key entries with `why`, gate `counts`, and claim rows in the same vocabulary `check --format compact` and the MCP tools speak (`stance`/`verdict`/`route`/`source`/`gates`, `counterexample` iff refuted, `supersession` iff the claim was re-authored after it was verified: the new text and the `mathema accept` command that adopts it); `totals.skip_reasons` counts the skipped claims per reason. Exit codes are identical either way
`--output FILE`	write the report to a file instead of stdout
`--verbose`	list every function in the text report; by default it lists only the functions checked again or with a problem, then the summary, which counts the unchanged ones. JSON always carries every function

Store keys are canonical dotted module.qualname names, resolved by importing from --root; the target must be importable there, and a bare-name key fails as a clear per-key problem line.

What fails the run¶

Finding	Default (strict)	`--lenient`
`falsified` claim	fails	fails
`invalidated` claim (held before, fails now)	fails	fails
`unknown` claim, not accepted	fails	fails
`unknown` claim, accepted as risk	fails (`N accepted-risk claim(s)`)	passes, named in the row
`skipped` (unverifiable) claim	fails	passes, informational
unresolved global name	fails	fails
silently-unenforced declared domain	fails	passes, informational
record whose function no longer resolves	fails (names the rename when an unrecorded function has its form hash)	fails
locked function whose body changed	fails, record untouched	fails, record untouched
lock removed outside `mathema unlock`	fails	fails
acceptance the policy rejects	fails	fails

A falsified claim fails in every mode: the record keeps the counterexample permanently (refutation is knowledge), but knowledge of a broken claim is exactly what a gate is for. An unknown claim also fails in every mode; in an agentic loop a claim nobody could adjudicate is indistinguishable from one that would have failed, until a human explicitly owns the gap with mathema accept --as risk. Accepted risk is visible relaxation, not laundering: --lenient proceeds past it (the row still names it), strict mode still refuses it.

Freshness never bypasses the gate: a function whose form hash is unchanged skips re-adjudication, but its stored verdicts are still checked, a record carrying a falsified or open-unknown claim fails the run even when nothing was re-run.

Exit codes: 0 clean; 1 gate failure; 2 usage/target/store error; 130 interrupted.

Worked example¶

Continuing from mathema check's softmax example:

import math
from typing import Annotated
from mathema.types import Shape

def softmax(scores: Annotated[list[float], Shape("n")]) -> Annotated[list, Shape("n")]:
    """Turn a vector of real-valued scores into a probability distribution.

    Claims:
        sums_to_one: sum(f(scores)) == 1
    """
    if not scores:
        raise ValueError("softmax needs at least one score")
    m = max(scores)
    exps = [math.exp(s - m) for s in scores]
    total = sum(exps)
    return [e / total for e in exps]

with its record written by write_spec():

import mathema
from functions import softmax

mathema.write_spec(softmax)

$ mathema verify --root .
ok   math.exp: library claims from mathema/compendium/math.claims.yaml; no baseline record; 1 proven, 3 holds, 0 falsified
1 unchanged since the last run (not run again), 1 checked, 0 problem(s)
grammars detected: mathema; verified by this run: mathema
1 intent to accept (1 function): mathema accept --intent

softmax calls math.exp, and the bundled compendium states claims about it, so the sweep adjudicates those against the installed library too (once, and fresh from then on), which is what a premise resting on them reads. It adjudicates no other math function: see Library claims.

The last line counts the stated intents that no one has accepted yet, here softmax's summary line, which sits at the declared rung until a person accepts it. It is information only and never changes the exit code; mathema accept --intent walks each one (see Intent at every level).

Drop the normalization on purpose (return exps instead of dividing by the total):

import math
from typing import Annotated
from mathema.types import Shape

def softmax(scores: Annotated[list[float], Shape("n")]) -> Annotated[list, Shape("n")]:
    """Turn a vector of real-valued scores into a probability distribution.

    Claims:
        sums_to_one: sum(f(scores)) == 1
    """
    if not scores:
        raise ValueError("softmax needs at least one score")
    m = max(scores)
    exps = [math.exp(s - m) for s in scores]
    total = sum(exps)
    return exps

and re-run:

$ mathema verify --root .
FAIL functions.softmax: form changed; 1 proven, 3 holds, 0 falsified, 1 invalidated  <- 1 invalidated claim(s)
1 unchanged since the last run (not run again), 1 checked, 1 problem(s)
grammars detected: mathema; verified by this run: mathema
1 intent to accept (1 function): mathema accept --intent

sums_to_one now fails, and because it held before it is reported as invalidated rather than falsified; the counterexample is kept in the record, and the exit code is 1. Restore the fix (the first version of functions.py above) and re-verify:

import math
from typing import Annotated
from mathema.types import Shape

def softmax(scores: Annotated[list[float], Shape("n")]) -> Annotated[list, Shape("n")]:
    """Turn a vector of real-valued scores into a probability distribution.

    Claims:
        sums_to_one: sum(f(scores)) == 1
    """
    if not scores:
        raise ValueError("softmax needs at least one score")
    m = max(scores)
    exps = [math.exp(s - m) for s in scores]
    total = sum(exps)
    return [e / total for e in exps]

$ mathema verify --root .
ok   functions.softmax: form changed; 1 proven, 4 holds, 0 falsified
1 unchanged since the last run (not run again), 1 checked, 0 problem(s)
grammars detected: mathema; verified by this run: mathema
1 intent to accept (1 function): mathema accept --intent

Back to clean, and the baseline is refreshed; the next verify will be fresh again until the code or the claim set actually changes.

Library claims: lazy by default, a file up front¶

The default sweep is lazy about the claims mathema bundles for libraries: only the library functions your project uses are adjudicated, the ones a swept function calls (through its import aliases, so np.sqrt is numpy.sqrt) or a claim rests a premise on, plus any already in the store. A project that never calls numpy verifies none of numpy's rows, and a new call brings its callee's rows in on the next sweep. A compendium file in your own project is a claims file in the tree like any other, and the sweep adjudicates all of it.

To adjudicate a whole claims file up front, name it. Every entry in the file is adjudicated and recorded like any sweep, whether or not your code calls it:

mathema verify claims/numpy.claims.yaml

A bundled file is named by the path records give it, mathema/compendium/...:

$ mathema verify mathema/compendium/math.claims.yaml --root .
ok   math.exp: library claims from mathema/compendium/math.claims.yaml; no baseline record; 1 proven, 3 holds, 0 falsified
FAIL math.log: library claims from mathema/compendium/math.claims.yaml; no baseline record; 1 proven, 0 holds, 0 falsified, 1 unknown  <- log_monotone unknown: derive could not decide it
       compendium:math declares 'log_monotone' for math.log; mathema verify recorded it unknown against the installed library:
       (i) to take it on its word, run: mathema accept math.log log_monotone --as trusted
       (ii) to decide it, restate the row, then run: mathema check math.log --claim "..."
ok   math.sqrt: library claims from mathema/compendium/math.claims.yaml; no baseline record; 1 proven, 3 holds, 0 falsified
0 unchanged since the last run (not run again), 3 checked, 1 problem(s)
grammars detected: mathema; verified by this run: mathema

The run gates like any other: math.log's derivative row cannot be settled against a function with no Python source, so it fails, naming the two ways forward. A file whose library is not importable, or is installed at a version outside the file's versions range, adjudicates nothing and says so on one line (note claims/numpy.claims.yaml: numpy 1.20.0 is outside the file's range >=1.24,<3; nothing in it was adjudicated). An ordinary claims file named the same way confines the sweep to its entries.

Unknown claims and accepted risk¶

A claim neither route could decide stays unknown and fails the run. Add a running balance in balances.py, with three claims in claims/running_total.claims.yaml:

def running_total(xs: list, y0: float) -> float:
    """Add every value in xs to a starting balance y0."""
    total = y0
    for v in xs:
        total = v + total
    return total

balances.running_total:
  claims:
    - name: shifts_with_start
      statement: "f(xs, y0) == f(xs, 0) + y0"
    - name: nonneg_for_nonneg_steps
      statement: "for xs in [0, 1]^n, f(xs, 0) >= 0"
    - name: never_overshoots_much
      statement: "assuming nonneg_for_nonneg_steps is proven, for xs in [0, 1]^n, f(xs, 0) <= len(xs)"

never_overshoots_much rests on nonneg_for_nonneg_steps being proven, and that one only holds (the probe agrees; derive cannot settle the sign of the lifted sum), so the dependent claim is unknown. shifts_with_start proves on the derive route, and every proof spawns a shifts_with_start[float] companion, the same law checked in floating point (see the evidence ladder). The companion is falsified: at xs = [1e300, -1e300, ...] the float sum cancels and drops y0, a result no float64 computation can deliver at inputs of that magnitude. The note says so, with the condition number at the witness, and gives the ways out. Since xs and y0 run along unbounded directions, the first is let |inf| be 1e+21, which bounds only the computation and never the proof, so the proof still covers every real input; mathema ran the claim with that binding before offering it, and its computation line holds. A computation line failing along an unbounded direction is offered such a binding whenever a run under it holds, whatever the conditioning says, B being the largest power of ten that holds where the conditioning gives none. The second accepts the computation line alone as a discovery, which mathema allows because the loss is inherent in the inputs rather than the code's. The second proven claim in the count is dependencies_current, which verify adds to every record:

$ mathema verify --root .
note balances.running_total: shifts_with_start[float] initially falsified: ill-conditioned here (κ ≈ 5e287): no float64 computation can deliver this result at inputs of magnitude 1e300:
  (i) if inputs this large are out of scope, bound the computation alone (the claim keeps its domain): let |inf| be 1e+21
  (ii) if the loss is accepted, run: mathema accept balances.running_total "shifts_with_start[float]" --as discovery
FAIL balances.running_total: no baseline record; 2 proven (1 claim, 1 built-in), 5 holds, 2 falsified, 1 unknown  <- 1 policy row to settle: missing[xs, null], f raises TypeError at a null slot of xs where mathema's default says propagates
       (i) change f
       (ii) write: missing(f, xs, null) raises(TypeError)
       to list them, run: mathema claims balances.running_total
       1 falsified claim(s)
       never_overshoots_much unknown: prerequisite nonneg_for_nonneg_steps is holds, not proven, nothing to rest this claim on
2 unchanged since the last run (not run again), 1 checked, 3 problem(s)
grammars detected: mathema; verified by this run: mathema
2 intents to accept (2 functions): mathema accept --intent

The line also names a policy row the code contradicts: running_total raises TypeError when a slot of xs is None, where mathema's default row says propagates; the clause names the row and the word to write (missing values).

The ways out are real evidence (rewrite the claim or the code so a route can decide it) or an explicit human decision to own the gap (--yes here answers the confirmation prompt). Naming the key re-checks it, so the row counts the accepted claim:

$ mathema accept balances.running_total never_overshoots_much --as risk --note "the premise only holds empirically; monitored" --by "Charles Babbage" --yes
accept balances.running_total :: never_overshoots_much as a risk, by Charles Babbage
  verdict unknown
  its verdict becomes skipped:unknown_but_accepted; strict mode still refuses it, lenient mode proceeds
written.
$ mathema verify balances.running_total --root . --lenient
FAIL balances.running_total: targeted re-verify; 2 proven (1 claim, 1 built-in), 5 holds, 2 falsified, 1 accepted risk  <- 1 policy row to settle: missing[xs, null], f raises TypeError at a null slot of xs where mathema's default says propagates
       (i) change f
       (ii) write: missing(f, xs, null) raises(TypeError)
       to list them, run: mathema claims balances.running_total
       1 falsified claim(s)
0 unchanged since the last run (not run again), 1 checked, 2 problem(s)
grammars detected: mathema; verified by this run: mathema
2 intents to accept (2 functions): mathema accept --intent

Strict mode (the default) still refuses the accepted risk, so a pipeline can choose whether owned gaps block it:

$ mathema verify balances.running_total --root .
FAIL balances.running_total: targeted re-verify; 2 proven (1 claim, 1 built-in), 5 holds, 2 falsified, 1 accepted risk  <- 1 policy row to settle: missing[xs, null], f raises TypeError at a null slot of xs where mathema's default says propagates
       (i) change f
       (ii) write: missing(f, xs, null) raises(TypeError)
       to list them, run: mathema claims balances.running_total
       1 falsified claim(s)
       1 accepted-risk claim(s)
0 unchanged since the last run (not run again), 1 checked, 3 problem(s)
grammars detected: mathema; verified by this run: mathema
2 intents to accept (2 functions): mathema accept --intent

See mathema accept.

Moved functions¶

A record is keyed by the function's dotted name, so a function moved to another module leaves its record under a key that no longer resolves, and that key fails the run. Move running_total from balances.py to ledger.py, and rename its claims file stanza to match:

mv balances.py ledger.py

ledger.running_total:
  claims:
    - name: shifts_with_start
      statement: "f(xs, y0) == f(xs, 0) + y0"
    - name: nonneg_for_nonneg_steps
      statement: "for xs in [0, 1]^n, f(xs, 0) >= 0"
    - name: never_overshoots_much
      statement: "assuming nonneg_for_nonneg_steps is proven, for xs in [0, 1]^n, f(xs, 0) <= len(xs)"

When the orphan's form hash matches a function that has no record, the failure line says so and names the exact remedy, and the new key is held back rather than given a fresh record that would start its history over:

$ mathema verify --root .
FAIL balances.running_total: cannot resolve to a live function (declared in .mathema/verified/balances.running_total.yaml); its form hash matches ledger.running_total, which has no record. If it moved, a human keeps its history with: mathema accept ledger.running_total --as reconciled --from balances.running_total
FAIL ledger.running_total: no record yet, and its form hash matches the orphan record balances.running_total; nothing was checked or written for this key. If it moved, a human keeps its history with: mathema accept ledger.running_total --as reconciled --from balances.running_total; if it is a different function, remove the orphan record instead
2 unchanged since the last run (not run again), 0 checked, 2 problem(s)
grammars detected: mathema; verified by this run: mathema
1 intent to accept (1 function): mathema accept --intent

The rename carries the whole record (claims, acceptances and their history, lineage, PIN stamp, lock) to the new key and removes the old file; see moved functions. The project's source is parsed, never imported, to find the match, and only when an orphan exists. In --format json the orphan's entry carries moved_to and remedy, and the held-back key has why: "moved-pending" with moved_from and remedy.

A record's history¶

A claim row's meta keeps mathema.previous_verdict when its verdict changes: one step, the verdict immediately before this one. There is no history field, because the verified layer is committed to git and git is the history. mathema review [<ref>] reads it by claim (which verdicts flipped, which claims were added, removed or reconciled), and git log .mathema/verified lists every commit that changed a record.

`--status`: the fresh/stale report¶

mathema verify --status is the report-only face: one fresh/stale line per @mathema.track_claims-tagged function, no adjudication, always exit 0. "Fresh" means the function's current identity hash matches its last verified record; "stale" means it changed since. Pass a target (mathema verify --status pkg.mod or a file path) to import it first, so a script's own tagged functions register under their real dotted keys:

@mathema.track_claims
def my_fn(x: float) -> float:
    ...

Mixed-grammar claims files¶

A declared-claims file/key can legitimately mix grammars, a core mathema claim sitting next to a claim in some other grammar (tagged grammar: mathema-data, say) under the same key. verify correctly distinguishes a foreign-grammar claim from a genuine failure: it's reported on its own, non-fatal line (N not this grammar (mathema-data)), not counted toward strict-mode failure. The sweep's closing lines name every grammar seen across the whole run versus what this particular command actually verifies, verify never adjudicates a foreign-grammar claim itself, whatever module owns that grammar; that needs real data/context a static sweep can't provide.

A claim that already has a real verdict recorded under mathema (proven, holds or falsified) and now declares another grammar, on the claim, its entry or its file, is warned about under the key's line, never counted as a failure:

     warning: claim commutative of funcs.add was verified under mathema; its grammar is now 'other', so mathema no longer adjudicates it

The claim's row in --format json carries grammar_changed: {from: "mathema", to: "other"}.

mathema verify¶