Dimensional proof certificates for scientific and machine-learning computation graphs.

UnitSentinel catches a class of production bugs that tensor shapes and dtypes cannot express: a graph can be structurally valid while metres, seconds, temperature kinds, scales, or offsets are physically incompatible. It compiles a bounded canonical graph into tracked exact constraints, fails closed unless every public contract is unique, and can issue an unsigned, content-addressed certificate for a positive result.

Status: the v0.1 verification core, canonical graph codec, 33-unit registry, deterministic CLI, detached certificate codec, independent strict replay, bounded verification-backed annotation repair, canonical training/serving comparison engine, normalization-lineage comparison, and strict comparison-result codec are implemented. The fail-closed comparison CLI and its reproducible compatible/drift/indeterminate evidence are also implemented. Closed-subset ONNX lowering remains future work.

Current implementation. Canonical bytes cross a bounded decoder; tracked constraints pass through Z3, exact extraction, and independent semantic replay before a positive claim can be issued. The accessible SVG source contains the same content.

A 7.6-second loop rendered from the exact committed CLI transcripts: conflict, corrected graph with certificate issuance, then strict replay. Equivalent text paths are available for conflict, verification, and replay.

The demo is not a mock terminal. Its graphs, stdout, exit codes, JSON records, certificate, frames, and output hashes are all committed in the evidence ledger.

Production ML contracts usually preserve tensor dtypes and shapes while the physical meaning of a feature remains in preprocessing code, prose, or loose metadata. Several dangerous changes therefore remain structurally valid:

• serving sends km/h while training consumed m/s;
• an absolute Celsius temperature is treated as a temperature difference;
• a normalization constant comes from a sensor with a different scale;
• two tensors share a shape and dtype but carry incompatible dimensions;
• an exported graph preserves numerical operations but loses the unit contract around its inputs and outputs.

ONNX tensor types describe element types and shapes. TensorFlow Data Validation checks schema properties and statistical skew. UnitSentinel targets another layer: exact physical dimension, quantity kind, scale, and offset across the computation itself.

The committed example is a small physics-informed feature pipeline rather than a toy metres + seconds expression:

1. subtract current and previous wheel speed in km/h;
2. convert the speed delta to m/s;
3. convert the sample period from ms to s;
4. derive acceleration as Δv / Δt;
5. normalize by a reference acceleration;
6. apply a sigmoid only after the value is dimensionless.

Dimensions, exact scales, and quantity kinds come from the live verified contract record. UnitSentinel checks the feature contract; it does not execute the tensors or calculate an anomaly score. Inspect the accessible SVG.

The verified graph is 2,072 canonical bytes and has SHA-256:

139e3e3d99d64c3d9cde89e9e1f116f09452c3532eaaee2e0513c71a0f2ada3c

UnitSentinel supports Python 3.11 and newer.

python3 -m venv .venv
.venv/bin/python -m pip install -e '.[dev]'

mkdir -p .unitsentinel/demo
.venv/bin/python -I examples/build_wheel_anomaly_contract.py \
    --variant verified \
    > .unitsentinel/demo/wheel-anomaly.json

.venv/bin/python -m unitsentinel verify \
    .unitsentinel/demo/wheel-anomaly.json \
    --certificate .unitsentinel/demo/wheel-anomaly.cert.json

Certificate output is deliberately no-overwrite: choose a fresh path for a second run. Successful human output includes ten exact contracts, both graph and result digests, the registry fingerprint, solver checks, and an explicit authentication disclaimer.

Plain text and canonical JSON are the sources behind this screenshot. The PNG is derived from the terminal SVG.

Machine consumers can request the same closed result record:

.venv/bin/python -m unitsentinel verify \
    .unitsentinel/demo/wheel-anomaly.json \
    --json

Verification, replay, repair, and comparison reports use structured stdout. Usage, input/output, expected-digest preflight, interruption, and redacted internal failures use stderr.

The conflicting variant changes exactly one annotation: acceleration-si claims meter-per-second even though Δv / Δt derives meter-per-second-squared. Shapes and dtypes are unchanged.

.venv/bin/python -I examples/build_wheel_anomaly_contract.py \
    --variant conflict \
    > .unitsentinel/demo/wheel-anomaly-conflict.json

.venv/bin/python -m unitsentinel verify \
    .unitsentinel/demo/wheel-anomaly-conflict.json \
    --certificate .unitsentinel/demo/should-not-exist.cert.json

The command exits 1; no positive certificate is written. See the plain transcript, canonical record, or accessible terminal SVG.

UnitSentinel returns the actual four-item deletion-minimal tracked witness rather than a generic “unit mismatch” message:

The witness connects the wrong serving declaration to the divide operation and both explicit conversions. “Deletion-minimal” does not mean minimum-cardinality. Inspect the accessible SVG.

The repair command can mechanically investigate one explicit unit annotation from a fresh minimal conflict core. It removes that annotation in memory, requires the relaxed graph to verify, finds exact canonical registry matches, and freshly verifies each bounded candidate. It never edits the input graph or claims to infer scientific intent.

.venv/bin/python -m unitsentinel repair \
    docs/evidence/contracts/wheel-anomaly-conflict.json \
    --max-sites 1 \
    --max-candidates 1 \
    --max-verifier-calls 3 \
    --max-work-items 64 \
    --total-timeout-ms 30000

The production CLI found exactly one verified candidate under the pinned registry and completed bounds: acceleration-si changes from meter-per-second to no declaration, then to meter-per-second-squared. The source remains unchanged and the output states application: not-performed. Inspect the exact transcript, canonical JSON, cross-bound provenance, or accessible SVG.

The repaired candidate retains the source graph identifier wheel-anomaly-conflict; it is not byte-identical to the separately committed verified fixture. proposed establishes a unique mechanical replacement under the recorded registry and limits—not scientific correctness or permission to apply it. The complete fail-closed contract is documented in Verified unit-annotation repair v1.

Two graphs can each be dimensionally verified and still disagree about their public interface or the normalization computation behind an output. unitsentinel compare uses an explicit canonical plan instead of matching names, positions, embeddings, or samples. The caller must pin the exact plan SHA-256.

The implemented order is part of the trust boundary: validate limits; hash and pin raw plan bytes before decoding; check the registry before opening graphs; hash each graph before decoding; freshly verify both sides; rederive normalization lineage; strictly encode the detached result; publish a new private result file if --result was requested; only then write stdout. Inspect the accessible SVG.

Run the recorded lineage-drift case with a fresh result path:

mkdir -p .unitsentinel/demo

.venv/bin/python -m unitsentinel compare \
    docs/evidence/plans/ratio-drift.plan.json \
    --training-graph docs/evidence/contracts/ratio-training.json \
    --serving-graph docs/evidence/contracts/ratio-serving-reversed.json \
    --expect-plan-sha256 \
    9e0163fba563e9bf73114fd756c5edfe0c3fd2bf2e9a0dc6d555e38b75765009 \
    --result .unitsentinel/demo/ratio-drift.result.json

The command exits 5 with a valid drift report. Both graphs freshly verify, all three public bindings agree dimensionally, and the only mismatch is normalization-lineage-drift for the mapped output. Reversing the ordered divide operands changes the output-normalization semantic digest even though shape, dtype, explicit units, dimension, kind, scale, and offset still match.

The content digests preserve graph-local diagnostics, while whole-lineage semantic digests provide rename-insensitive reviewer evidence. Compatibility is decided from mapped interface metadata and per-output normalization digests—not from the whole-lineage semantic digest. The compatible rename has equal mapped output digests; the reversed divide has unequal mapped output digests and exactly one reported mismatch. Every digest comes from the committed strict claims. Inspect the accessible SVG.

The same fixed fixture family records all three closed outcomes:

These are exact committed artifact byte lengths, not latency, throughput, accuracy, or scalability measurements. The source table is comparison-artifacts.json; the accessible plot source is comparison-artifact-sizes.svg.

The loop is rendered from the same committed full terminal SVGs and declared frame delays. It is presentation, while the comparison provenance, strict raw claims, and exact text/JSON captures are the primary records.

The result file is canonical, strict-decoder round-trippable, unsigned, and written with mode 0600 through atomic no-overwrite publication before stdout. compatible means only “compatible under these exact plan, graph, registry, and solver-limit bindings.” It does not authenticate plan approval, prove deployment or simultaneous file state, execute a model, validate broadcasting/matmul, measure statistical drift, or establish scientific correctness. The complete byte and execution contract is documented in training-serving comparison v1.

A positive certificate binds:

• graph schema and SHA-256;
• registry version and SHA-256;
• verifier and solver versions;
• exact solver limits;
• ordered inferred contracts;
• the source-labelled constraint catalog;
• the complete verified result digest.

It is canonical and content-addressed, but not signed. UnitSentinel therefore prints authentication: not-provided instead of implying provenance it cannot establish.

Graph, registry, toolchain, result, certificate, and replay identities are taken from the committed claim. REPRODUCED means semantic reproduction, not issuer authentication. Inspect the accessible SVG.

Replay can pin the expected certificate bytes and require the current toolchain to match the claim:

.venv/bin/python -m unitsentinel replay \
    docs/evidence/claims/wheel-anomaly.cert.json \
    --graph docs/evidence/contracts/wheel-anomaly-verified.json \
    --expect-sha256 \
    e93cc87cd72c6ede9cf8d324bfb41b2eb2bdcea6cb0aa6fea7aed4696009ab1a \
    --strict-toolchain

Strict replay recomputes the certificate digest, checks graph/registry and toolchain bindings, replays pure semantic witnesses, then performs a fresh bounded uniqueness verification. Sources: text, JSON, and SVG.

Local arithmetic is enough when every intermediate unit is already known. Real graphs are only partially annotated. UnitSentinel creates exact expressions for seven SI dimension exponents, quantity kind, scale, and offset, then asks two distinct questions:

1. is the tracked system satisfiable?
2. can any observable contract take a different model value?

Only a satisfiable system with no alternate observable model is verified. Every extracted rational value is checked against domain bounds and replayed by independent Python semantics before publication. A timeout, memory boundary, non-rational model value, unsupported operation, or out-of-domain exponent fails closed.

Tracked assertions retain source identities such as:

declaration/acceleration-si/unit
operation/derive-acceleration/dimension
operation/normalize-sample-period/dimension
operation/normalize-speed-delta/dimension

Solver-generated names and raw diagnostics never enter public output.

The repository includes one measured snapshot over identity chains of 1, 8, 32, 128, and 256 operations. Each point is the median of three recorded runs.

This plot reports wall-clock verification-plus-issuance and strict replay on the recorded Python/Z3/Linux environment. It is not an accuracy benchmark, cross-machine ranking, or performance guarantee. Raw runs and environment: scaling.json; accessible source: scaling.svg.

The implementation includes:

• immutable vectors over the seven SI base dimensions with bounded rational exponents;
• exact unit scales and affine offsets without float coercion;
• distinct linear, absolute-temperature, and temperature-difference kinds;
• an immutable 33-unit registry with canonical serialization and a pinned SHA-256 fingerprint;
• a closed topological graph IR with one producer per non-input value;
• scalar types, bounded concrete/symbolic shapes, and explicit unit annotations;
• a byte-level decoder that rejects duplicate keys, floats, noncanonical JSON, unknown fields, invalid topology, and oversized inputs;
• a bounded canonical, unsigned training/serving plan with explicit, duplicate-free interface mappings and graph/registry digest bindings;
• a fresh-verification comparison engine with caller-trusted plan pinning, exact public-occurrence coverage, semantic replay, and deterministic drift codes;
• bounded, content-addressed normalization lineage with mapped logical roots, exact inferred metadata, output routing, and internal-rename invariance;
• fail-closed cross-graph normalization-lineage comparison over two freshly verified, graph-rederived lineages, including repeated-site multiplicity;
• a strict 32 MiB canonical JSON codec for bounded, unsigned comparison-result claims with exact nested digest and model round-trip checks;
• structural preflight limits on bytes, nesting, tokens, nodes, and items;
• exact constraints for all 14 supported graph operations;
• alternate-model uniqueness checks;
• deterministic tracked-core shrinking within a fixed check budget;
• monotonic per-check and whole-run deadlines plus solver memory bounds;
• independent semantic replay of extracted models;
• canonical verification results, proof certificates, and replay reports;
• bounded, non-mutating, verification-backed unit-annotation proposals;
• a deterministic CLI with caller-pinned comparison plans, bounded regular-file reads, stable domain exits, and atomic private no-overwrite certificate/result writes.

The canonical graph contract, registry snapshot, and architecture boundary specify the core. The certificate and replay contract documents the detached claim byte boundary and replay ordering. The training-serving comparison contract defines the explicit alignment plan, fresh engine, and strict unsigned result byte boundary without claiming that decoding proves freshness or that a plan digest authenticates who approved its mapping.

Verification, replay, repair, and comparison require no network and never execute model code. The CLI does not consume stdin; it accepts path-backed regular files and rejects FIFOs, oversized documents, duplicate JSON fields, executable extension hooks, unsafe output targets, and symlinks at the input leaf or final parent component. Earlier intermediate path components are not walked individually. Every open descriptor must be a regular file, and bounded nonblocking reads still cap a file that grows after its initial fstat. Certificate and comparison-result writes use private no-overwrite temporary files, file and directory durability checks, and atomic publication before stdout.

Comparison reads the plan, training graph, and serving graph in that order as sequential descriptor snapshots; it does not claim an atomic simultaneous snapshot of all three paths. Human/JSON reports intentionally repeat user-supplied semantic graph and contract identifiers, so stdout is not a private channel.

The threat model excludes a hostile same-UID process that can rewrite the installed verifier, solver, or repository parent directories during execution. A caller-trusted expected digest can detect certificate-byte substitution; successful replay establishes current semantic agreement. Neither establishes author identity or proves that the claimed issuance happened.

• Claiming dimensional consistency proves scientific correctness.
• Executing tensor payloads or validating broadcasting/matmul shapes.
• Full UCUM compatibility.
• Currency, calendar arithmetic, logarithmic units, or contextual chemistry conversion.
• Guessing scientific intent from variable names.
• Executing user Python, model code, plugins, URLs, or import paths.
• Applying an LLM-generated repair without formal re-verification.

The recorder and renderer are part of the repository:

npm --prefix tools/evidence ci --ignore-scripts
npm --prefix tools/evidence run audit

.venv/bin/python -m tools.evidence.generate --check
npm --prefix tools/evidence run check
.venv/bin/python -m tools.evidence.repair_evidence --check
npm --prefix tools/evidence run check:repair
.venv/bin/python -m tools.evidence.comparison_evidence --check
.venv/bin/python -m tools.evidence.comparison_visuals --check
npm --prefix tools/evidence run check:comparison

To refresh only the deterministic repair records and repair rendering:

.venv/bin/python -m tools.evidence.repair_evidence --record
npm --prefix tools/evidence run render:repair
.venv/bin/python -m tools.evidence.generate --write-manifest

To refresh only the deterministic comparison records and visuals:

.venv/bin/python -m tools.evidence.comparison_evidence --record
.venv/bin/python -m tools.evidence.comparison_visuals --record
npm --prefix tools/evidence run render:comparison
.venv/bin/python -m tools.evidence.comparison_evidence --check
.venv/bin/python -m tools.evidence.comparison_visuals --check
npm --prefix tools/evidence run check:comparison
.venv/bin/python -m tools.evidence.generate --write-manifest

The general recorder and renderer remain available when intentionally refreshing the complete legacy evidence set:

.venv/bin/python -m tools.evidence.generate --record
npm --prefix tools/evidence run render
.venv/bin/python -m tools.evidence.generate --write-manifest

The timing snapshot changes only through the explicit --record-benchmark mode. The evidence ledger, generation guide, and closed manifest document every input and output.

The current suite contains 418 unit, integration, adversarial, and evidence tests with 97% statement coverage, 94% branch coverage, and 96% combined statement/branch coverage.

PYTHONPATH=src .venv/bin/python -m unittest discover -s tests -v
PYTHONPATH=src .venv/bin/coverage run -m unittest discover -s tests
.venv/bin/coverage report

.venv/bin/ruff check .
.venv/bin/ruff format --check .
.venv/bin/mypy src tools/evidence tools/measure_comparison_result_boundary.py
.venv/bin/python -m build
.venv/bin/pip-audit

.venv/bin/python -m tools.evidence.generate --check
npm --prefix tools/evidence run check
.venv/bin/python -m tools.evidence.repair_evidence --check
npm --prefix tools/evidence run check:repair
.venv/bin/python -m tools.evidence.comparison_evidence --check
.venv/bin/python -m tools.evidence.comparison_visuals --check
npm --prefix tools/evidence run check:comparison

The evidence tests independently validate canonical graph/certificate bindings, the closed manifest, SVG accessibility and self-containment, PNG chunk CRCs and decompressed dimensions, GIF frame timing/loop structure, README coverage, and secret/PII exclusions.

The repository intentionally has no license yet. Licensing is a decision for Omar before third-party reuse is invited.