The engine

The engine is generic: it knows no physics directly — every assertion comes from a card. Two complementary checks run against the corpus.

Hypothesis cross-check

The shipping verification surface (MCP tool hypothesis_crosscheck) takes a proposed new principle — a HypothesisCard, by id or inline — and verifies it against the corpus and universal priors:

• dimensional analysis of the proposed relation — comparing the declared dimension vectors, or, when the card supplies a formula (expr) plus per-symbol dimensions (symbols), deriving the dimensions from the formula itself and checking them against lhsDims,
• reference-corpus resolution — does it resolve against known cards,
• declared limit / conservation claims,
• derivedFrom link resolution.

It refuses to fabricate: an unknown id returns a structured error listing the valid ids, not a guess.

Validation envelopes (USCE)

principle cards may declare validationEnvelopes — { key: [min, max] } numerical bounds — plus expectedLimits and conventions. These are the assertions the evaluation engine asserts against a candidate output at runtime. The richer a card’s envelopes and limits, the more deeply the engine can check code that claims to implement it.

Severity

A check does not collapse to one number. There are two scales — one per check, one for the run — and they take different values.

CheckSeverity (per check)	Meaning
pass	The assertion was tested and holds.
warn	The claim could not be tested — recorded, neither proven nor refuted.
fail	The assertion was tested and is violated.

OverallSeverity (per run)	Meaning
NONE	Nothing to report.
LOW	A soft concern.
MEDIUM	A real problem.
HIGH	A hard violation — zeroes the overall score even on a functional pass.

The overall result is the worst check, never an average. That last row is the core thesis: in science, physical correctness gates functional correctness. Passing the tests is not enough if a HIGH-severity physical check fails.

See verdicts for why warn is a distinct value rather than a weak fail.

Cross-method agreement

A third checker sits one relation above USCE. Where a validation envelope bounds what a single run may produce, runAgreementChecks / run_agreement_checks bounds how far two independent methods may disagree with each other, per the crossMethodTolerances a card declares.

Its default is deliberately the opposite of the envelope check’s: an empty result is a failure, not a pass. Fewer than two methods raises outright — a single method cannot corroborate itself — and two methods with no observable in common returns HIGH rather than quietly reporting that nothing disagreed.

It is a library function in both SDKs, deliberately not exposed as an MCP tool.

An absent check is not a passing one

The envelope check’s default is permissive: an output key with no declared envelope is simply not checked, and a run can come back clean having verified nothing at all. Pass requireChecks (TypeScript) or require_checks=True (Python) to runUsceChecks / run_usce_checks to make that state a HIGH finding instead.

This is an engine-level flag, not a tool argument — the MCP usce_check tool always uses the default. Reach for it in CI, where “nothing was checked” and “everything passed” must not look alike.

Series conditions — reaching cards an envelope cannot

An envelope bounds a magnitude. Some quantities have no system-independent magnitude at all, and the corpus says so: five cards deliberately declare no validationEnvelopes because any number would encode one calculation’s setup rather than the physics. A density of states scales with cell volume and band count, and its shape depends on the basis, the k-mesh and the smearing width.

But two of those cards carry something that is universal — a sign:

• density-of-states — g(epsilon) >= 0
• joint-dos — J(omega) >= 0

A density of states cannot be negative in any material, at any k-mesh, under any smearing. The magnitude is unboundable; the sign is not. So runSeriesChecks / run_series_checks gives verification coverage to cards the envelope check structurally cannot reach.

Cards declare these in seriesConditions. A condition may restrict the samples it covers, and that restriction is load-bearing: Im chi_0(omega > 0) <= 0 says nothing about negative frequencies, where Im chi_0 is legitimately positive — testing it there would manufacture a violation the card never asserted.

Convergence order — checking the number, not the claim about it

A numerical-methods card can declare an expected order of accuracy, and USCE will range-check the order you report. Nothing checked that the number was measured correctly, which made the most safety-critical value on such a card self-reported.

runConvergenceCheck / run_convergence_check recomputes it from the refinement study itself — the (h, error) pairs — and compares that against the card’s envelope.

Its most important behaviour is a refusal. A study containing round-off-limited levels fits a shallower slope and can land outside the envelope while the method is perfectly correct. Reporting that as a failure would blame the scheme for a contaminated measurement, so a sequence that is not a clean power law returns warn and prints the per-level orders, naming the refinement level to drop.

Status

The cards corpus and the MCP server are usable today, as are all five checkers: hypothesis_crosscheck for proposed principles, usce_check / run_usce_checks for validation envelopes, the agreement checker for cross-method comparison, and the two above for series conditions and convergence order.

Three of the five are library and CLI only — agreement, series and convergence are not MCP tools yet. All five are reachable from lemma verify and from both SDKs.

The engine ships twice — TypeScript in the MCP server, Python in the SDK — and the two are held to byte-identical verdicts and byte-identical prose by a shared fixture, so either is a valid production choice. The one documented exception is symbolic verification, which is Python-only and opt-in.