mipiti-verify

Turnkey CI verification for Mipiti threat model assertions. Security controls that never drift.

Install

pip install mipiti-verify[all]      # OpenAI + Anthropic support
pip install mipiti-verify[openai]   # OpenAI only
pip install mipiti-verify[anthropic] # Anthropic only
pip install mipiti-verify           # Tier 1 only (no AI provider)

Commands

run — Verify assertions against a model

# Verify all models in the workspace (recommended)
mipiti-verify run --all \
  --api-key $MIPITI_API_KEY \
  --tier2-provider openai \
  --tier2-model gpt-4o-mini \
  --project-root .

# Verify a single model
mipiti-verify run <model_id> \
  --api-key $MIPITI_API_KEY \
  --tier2-provider openai \
  --project-root .

API keys are workspace-scoped — --all verifies every model accessible by the key that is bound to the repository the verifier runs in: a model whose provenance names another repository is skipped with a notice, one that names this repository has every coverage gap reported, and one that names none is reported only if it has at least one assertion bound here (otherwise a single line says so).

verify — Check a single assertion locally

mipiti-verify verify function_exists -p file=app/auth.py -p name=verify_token
mipiti-verify verify pattern_matches -p file=nginx.conf -p pattern="Strict-Transport-Security"
mipiti-verify verify dependency_exists -p manifest=requirements.txt -p package=bcrypt
mipiti-verify verify import_present -p file=app/main.py -p module=fastapi

No API key needed — runs Tier 1 locally against your codebase.

check — Verify assertions from a JSON file

mipiti-verify check assertions.json --project-root .

Offline batch verification from a JSON file. No API key needed.

list — Show pending assertions

mipiti-verify list <model_id> --api-key $MIPITI_API_KEY

report — Show verification results

mipiti-verify report <model_id> --api-key $MIPITI_API_KEY

Shows Tier 1/2 pass/fail counts, control verification status, drift detection, and sufficiency status.

audit — Verify signed reports

mipiti-verify audit report.html
mipiti-verify audit audit-package.json
mipiti-verify audit audit-package.json --full

Independently verifies ECDSA document signatures on exported HTML reports and JSON audit packages. Validates OIDC provenance, content integrity, and per-assertion reasoning.

Output modes. The default output is a verdict-first workpaper summary: the verdict line, the trust contract, one line per contributing run, the producer-disclosure cross-check, an itemized Caveats section (each with its remediation hint), per-control pass/fail counts, condensed composition aggregates, and the compact cryptographic evidence blocks. Detail auto-expands only for elements that fail or degrade — a failed assertion prints its full row, a hash mismatch prints expected vs. recomputed hashes, an unverifiable run keeps its explanation — so a clean report is short and a problem report shows exactly the problem. --full restores the exhaustive listing in verification order (per-assertion detail, per-CO composition enumeration, inheritance-binding rows, the provenance-health panel). Exit codes are identical in both modes; scripted consumers should gate on the exit code.

Bundle binding. When an audit package carries a Sigstore bundle, the envelope must also carry content_integrity.bundle_bind_hash — the explicit hash the verifier compares against the bundle's in-toto Subject digest (no canonicalisation, no rehashing). Older envelopes that omit this field are rejected. Re-export the audit package from a current Mipiti build to obtain the bundle-bind coverage.

attest-tests / attest-dependence / attest-reach — Record test evidence in the test job

pytest --junitxml=report.xml
mipiti-verify attest-tests --junit report.xml --coverage coverage.json
mipiti-verify attest-dependence --pair tests/test_auth.py::test_token_required=app/auth.py::require_token
mipiti-verify attest-reach --pair tests/test_auth.py::test_token_required=app/auth.py::require_token

attest-tests reads the report your test step wrote and signs it; it runs nothing. attest-dependence and attest-reach are the two opt-in commands that run tests: each named test once, with its mechanism disabled (does the test fail without it?) or alone under coverage (which lines of the mechanism's file does it execute?). Both go through the project's runner adapter (pytest, jest, vitest, mocha, go, cargo, maven, gradle, dotnet, rspec, phpunit, or a --run-cmd for simulators; --suite-cmd + --suite-junit for a harness that runs everything at once) and belong in the job that already runs your tests. See Test-result attestations and Runners.

attest-construction / attest-allowlist-review — Record what only your build can settle

mipiti-verify attest-construction --boundary-type SafeSql --probe probes/safe_sql_from_variable.rs
mipiti-verify attest-allowlist-review --allowlist allowlist.json

Two facts a sound witness cannot establish by reading the repository, signed with the same identity ladder as every other statement.

attest-construction compiles each probe and records the ones the toolchain REFUSED. A probe builds the boundary type from something that is not a literal; a compiler that rejects it is evidence the type cannot be produced another way, which name-based construction tracking can only assume. A probe that compiles means the type does not constrain what reaches it: the command exits non-zero and writes nothing. A probe the toolchain never answered on — no tool installed, no project file above the source, a command that would not start or ran out of time — is an absent answer, not a refusal: it is reported as such and nothing is signed. Nothing is executed — a probe is compiled, never run. Use --build-cmd '<command> {file}' for a toolchain the built-in checks cannot drive.

attest-allowlist-review records the reviewed exceptions and who stands behind them at this commit. The reasons already travel inside the evidence hash; what the repository cannot carry is a signed reviewer. Every entry must name a file, a site, a callee, a reason and a reviewer.

Neither statement changes a verdict. Each replaces "taken on the author's word" with "recorded in a signed statement" in the facts a reader sees.

Audit Envelope Contract

What an auditor running mipiti-verify audit <report> actually verifies, and what each check does (or doesn't) defend against. The contract is what makes the verifier defensible without trusting the platform: every claim the audit reports is anchored in either a public-anchor cryptographic chain or an auditor-supplied pin.

What's inside the envelope

A signed audit package (PDF or JSON) carries the following per-row evidence:

Run-level provenance (contributing_runs + provenance_health)

Verification state in a report accumulates across (often partial) CI runs — each assertion's current status was earned by its most recent run. Newer envelopes disclose that history through two additive top-level keys:

• contributing_runs — one entry per status-determining run. Each entry carries the run's exact canonical results text (results_canonical — the exact bytes whose hash was signed), its own content_integrity block (results_hash, signature, key material), the assertion ids that run determines, and optionally a per-run Sigstore bundle (the canonical trust anchor for that run when present).
• provenance_health — the producer's own coverage disclosure (assertions run-covered vs. manifest-only, per-run key/serialization limitations, warnings). Rendered as a panel in --full output; the default summary surfaces its warnings in the Caveats section and reports the agreement/disagreement outcome of the auditor-side cross-check. The per-run verification is the independent auditor-side check in both modes.

The verifier checks each run independently: SHA-256 recomputed over the exact results_canonical bytes against results_hash, the signature over the hash with the run's key (embedded PEM or JWKS lookup by fingerprint), and the per-run Sigstore bundle when present. Each run is reported as VERIFIED, UNRESOLVED KEY, UNVERIFIABLE SERIALIZATION, TAMPER-MISMATCH, or UNSIGNED. A run whose content_integrity declares unverifiable_serialization (signed material exists but the signed bytes can no longer be re-derived; the serialization predates canonical freezing) is a coverage limitation — reported distinctly from a hash mismatch and never treated as tampering. A genuine mismatch over present results_canonical fails the audit.

Assertions carried by the report's records but determined by no embedded run are reported as manifest-only provenance, cross-checked against provenance_health.assertions_manifest_only. When contributing runs are embedded, the deprecated top-level results_hash + signature pair is superseded: a divergence there is rendered informationally (NOT SCORED) and tamper conclusions come solely from the per-run checks. Older envelopes without these keys verify exactly as before — the legacy pair stays strict, and the trust contract reports run-level provenance as UNKNOWN (latest-run evidence only), never as a failure.

Each check the verifier runs

What's signed vs. what's only present

• Signed by Fulcio (provable identity): bundle DSSE payload (per-tier verification statement, including assertion specs and verdicts).
• Signed by platform JWKS key: bundle_bind_signature (platform's attestation that this bundle_bind_hash came out of an authorized Mipiti instance).
• Signed by workspace key: content_integrity.signature over results_hash for workspace-keyed rows.
• Recorded in Rekor: every Sigstore bundle (publicly auditable, immutable transparency log).
• Not signed: the package's outer JSON metadata (generated_at, model.title, etc.) — those are unsigned and forgeable. The verifier never reads pin-relevant values from outer metadata.

Auditor pins and what each one buys

Pins are out-of-band knowledge the auditor brings to the verification: they're what closes the gap between "this bundle is internally consistent" and "this bundle came from the customer's actual release process." Without pins, the verifier can confirm cryptographic integrity but not identity.

• --expected-ci-identity '<SAN>' — pin the workflow identity. SAN format: https://github.com/Org/Repo/.github/workflows/<file>.yml@<git-ref>. Source the value from the customer's release docs / security policy, never from the bundle itself.
• --ci-identity-from-env — auto-derive from GITHUB_WORKFLOW_REF when running audit inside CI for the same workflow that generated the report.
• --expected-issuer — pin the OIDC issuer. Required for self-hosted GitHub Enterprise / GitLab; auto-derived from SAN prefix for github.com / gitlab.com.
• --expected-workspace-key '<fp>' — pin the workspace ECDSA key fingerprint (SHA-256 hex of DER SubjectPublicKeyInfo).
• --expected-customer-key '<path-to-pubkey.pem>' — pin the customer's public key (PEM) for the customer-keyed offline DSSE path. The verifier requires the SHA-256 fingerprint of this key's DER SubjectPublicKeyInfo to equal the key that actually signed the bundle. Source the public key from the customer out-of-band, never from the envelope. Required whenever the package carries a customer_dsse envelope — without it, the audit fails closed.
• --expected-model-id, --expected-commit-sha — pin predicate fields signed inside the bundle. For customer_dsse, --expected-customer-key is the analogue of a SAN pin: it makes the predicate pins meaningful (the predicate is signed by the customer's own key), so predicate pins may be used together with it without --expected-ci-identity.

The verifier emits a "Trust contract" summary block in every audit — immediately after the verdict in the default summary, at the end of the --full listing — naming which pins were enforced and which were skipped, so an auditor can see at a glance what their command actually checked.

Failure modes (every check fails closed)

The verifier exits non-zero on any of:

• Cryptographic check fails (bundle signature, Rekor proof, bundle-bind, content-integrity sig).
• Identity pin set but bundle's SAN/issuer doesn't match.
• Workspace key pin set but the recomputed fingerprint doesn't match.
• Predicate pin set but the bundle's predicate field doesn't match.
• Bundle-bind signature present but no platform key resolvable (would be silent skip otherwise).
• Document signature on the PDF/HTML body is missing or invalid.
• Pinning flags supplied to a format that can't honour them (e.g. identity pins on an HTML report — fails-closed instead of silently dropping the pin).

There is no --allow-unsigned, no soft-fail, and no fallback that treats a missing signature as "good." When the auditor needs to enforce attestation on the producer side too (CI runner), use --require-attestation on mipiti-verify run to make missing/failed signing a non-zero exit.

Independent re-verification

Every published audit can be re-checked offline using only:

• The Sigstore TUF root (cacheable; pinnable via --sigstore-trust-config <path>).
• The Mipiti instance's JWKS (/.well-known/jwks; pinnable via --platform-pubkey <pem> for fully offline runs).
• The customer's workspace key fingerprint (auditor's out-of-band knowledge).
• The customer's CI workflow identity (auditor's out-of-band knowledge).
• For the customer-keyed offline DSSE path: the customer's public key, pinned out-of-band by the auditor via --expected-customer-key.

No live Mipiti API access is required at audit time. The verifier produces the same verdict on the same input regardless of network reachability to api.mipiti.io.

Customer-keyed offline signing (air-gapped / non-Sigstore CI)

Sigstore signing needs a Fulcio-trusted OIDC token and reachability to public Sigstore infrastructure at sign time. CI that structurally cannot do this — Jenkins, self-managed or older GitLab, Buildkite/CircleCI without OIDC, regulated/air-gapped networks — can instead sign with a customer-controlled key, fully offline, and have the result remain independently verifiable in the standard DSSE / in-toto format.

Producer side (mipiti-verify run). Generate an ECDSA P-256 keypair, keep the private half local, and register the public half on the Mipiti workspace. Then:

mipiti-verify run tm-abc123 \
  --api-key "$MIPITI_API_KEY" \
  --customer-key ./customer-signing-key.pem \
  --customer-key-passphrase "$KEY_PASSPHRASE"   # omit for an unencrypted key

--customer-key (env: MIPITI_CUSTOMER_SIGNING_KEY; passphrase env: MIPITI_CUSTOMER_SIGNING_KEY_PASSPHRASE) builds a standard in-toto Statement (same shape as the Sigstore path — assertion specs + verdicts in the predicate), computes the DSSE Pre-Authentication Encoding, and signs it with the customer's key. No Fulcio, no Rekor, no network at sign time. When supplied, this path is preferred over Sigstore. Combine with --require-attestation to fail the run if signing did not occur.

Auditor side (mipiti-verify audit). Obtain the customer's public key out-of-band (release docs / security policy) and pin it:

mipiti-verify audit report.json \
  --expected-customer-key ./customer-public-key.pem \
  --expected-model-id tm-abc123        # optional predicate pins, now meaningful

The verifier reconstructs the DSSE PAE from the embedded payload, checks the signature, requires the SHA-256 fingerprint of the pinned key's DER SubjectPublicKeyInfo to equal the key that actually signed the bundle (the vendor-independence gate — a swapped key fails here), and binds the Statement subject digest to the report's content hash. Entirely offline. If the package carries a customer_dsse envelope but --expected-customer-key is not supplied, the audit fails closed and says so — the embedded PEM is never silently trusted.

For this path the vendor-independence property holds without caveat: the auditor verifies the chain from the envelope bytes plus a fingerprint pinned from the customer. Mipiti is pure transport — it holds no customer private key and cannot substitute the key without failing the fingerprint gate. Revocation is out-of-band (the customer tells auditors to stop trusting a fingerprint), the same as any pinned key.

API Key Scopes

Developer keys skip result submission automatically — no --dry-run needed.

Key Flags

GitHub Action

permissions:
  id-token: write    # required: mints the OIDC token used for Sigstore signing
  contents: read

jobs:
  verify:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2

      # Your tests, run by you. Write a JUnit report so the result can be
      # recorded as evidence; verification reads it and runs nothing itself.
      - run: pytest --junitxml=report.xml

      - uses: Mipiti/mipiti-verify@6506a67e94c451055cc0659643b1572fb69f265f # v0.55.5
        with:
          # Required
          api-key: ${{ secrets.MIPITI_API_KEY }}

          # Needed for test_attested assertions. Points at the report the step
          # above wrote; the action records a signed attestation from it before
          # verifying. Space-separate several paths for more than one suite.
          # Signed keylessly through Sigstore using the run's OIDC token — no
          # secret to create or rotate. Only CI without a workload identity
          # needs attestation-signing-key.
          junit-report: report.xml

          # Optional, opt-in, and the only inputs that run tests: dependence
          # and reach for the pairs named, through the project's runner.
          # dependence-pairs: tests/test_auth.py::test_token_required=app/auth.py::require_token
          # reach-pairs: tests/test_auth.py::test_token_required=app/auth.py::require_token
          # runner: go                 # override the detected runner; 'command' with run-cmd for simulators

          # Optional, for assertions that require the run to have used a
          # particular configuration. A suite can pass with the control it
          # exercises switched off, and a file in the repository shows what is
          # declared, not what the run had. Only these names are recorded, and
          # a name that looks like a credential is refused.
          attestation-env: FEATURE_AUTH ENFORCE_TLS

          # Model selection (one of these)
          all: true                    # Verify all models in the workspace
          # model-id: "tm-abc123"     # Or verify a specific model

          # Tier 2 semantic verification (omit for Tier 1 only)
          tier2-provider: openai       # openai, anthropic, or ollama
          tier2-model: gpt-4o-mini     # e.g. gpt-4o, claude-sonnet-4-5-20250514
          tier2-api-key: ${{ secrets.OPENAI_API_KEY }}

          # Optional
          # reverify: true             # Re-verify all assertions, not just pending (default: true)
          # dry-run: false             # Run without submitting results (default: false)
          # concurrency: 1             # Max concurrent Tier 2 LLM calls (default: 1)
          # project-root: "."          # Project root directory (default: ".")
          # base-url: "https://api.mipiti.io"  # API base URL (default: https://api.mipiti.io)
          # sigstore-tuf-url: "..."    # Private Sigstore deployment (default: public sigstore.dev)

All assertions are re-verified by default. Use reverify: false to only check new assertions (reduces Tier 2 API costs on PRs). Omitting tier2-provider runs Tier 1 only — controls won't reach "verified" status without Tier 2.

Requiring an attestation (recommended)

When the job has no OIDC token (no id-token: write) and no workspace-signing-key, the action still submits results, unsigned, and emits a ::warning:: annotation saying so. For a CI gate whose results are meant to be audited, set require-attestation: true so a run that cannot produce an attestation fails instead of submitting one the audit side cannot pin to a signing identity:

permissions:
  id-token: write
  contents: read

steps:
  - uses: Mipiti/mipiti-verify@<pinned-sha> # vX.Y.Z
    with:
      api-key: ${{ secrets.MIPITI_API_KEY }}
      all: true
      require-attestation: true

The default stays false so existing workflows on runners without workload identity keep working; the annotation is the signal to either grant the permission, configure a key, or opt into failing closed.

Attestation (Sigstore)

mipiti-verify signs every submitted result set with Sigstore: the runner's short-lived OIDC token is exchanged at Fulcio for a signing certificate, the verified content hash is signed, and the entry is recorded in Rekor (the public transparency log). Mipiti's backend receives only the resulting bundle — the raw OIDC token never leaves CI.

Offline verification. The bundle is self-contained: it carries the signing certificate, signature, Rekor inclusion proof, and signed Merkle tree checkpoint. An auditor can re-verify the bundle without contacting Rekor or Mipiti — they need only the Sigstore trust root (Fulcio CA chain + Rekor public key + CT log keys). The sigstore client fetches the trust root from TUF on first use and caches it; the TUF timestamp expires in ~1 week, so repeat verifications on the same workstation are network-free until then. For fully air-gapped review, pin a trust root snapshot and pass it to mipiti-verify audit --sigstore-trust-config <path>.

What the attestation carries. The signed in-toto predicate holds model_id, tier, content_hash, pipeline metadata, and a compressed {assertions, results} payload. assertions carries each assertion's verified content (id, type, params, description; the fields bound by content_hash), its binding (control_id / assumption_id / functional_test_id / node_id, repo), and provenance (origin, inherited_from_model_id, created_by, created_at). results carries this run's verdicts. The platform's stored verdict state from earlier runs is not part of the attestation. Verifiers bind on content_hash (the Subject digest) and the predicate pins; the payload arrays are evidence for a reader of the bundle, not an input to any signature check.

Network dependencies at CI-time. Signing requires outbound access to fulcio.sigstore.dev (certificate issuance), rekor.sigstore.dev (transparency log), and tuf-repo-cdn.sigstore.dev (trust root). Each CI job starts from a cold TUF cache, so expect ~1–3s of trust-root fetch on every run. To eliminate the TUF fetch entirely — e.g. for air-gapped CI — download a Sigstore ClientTrustConfig JSON out-of-band and pass it via sigstore-trust-config. Private Sigstore deployments can redirect the whole stack via sigstore-tuf-url.

Private or air-gapped deployments can also redirect signing itself at their own Sigstore instance via sigstore-tuf-url on the run command.

Test-result attestations (test_attested)

A test_attested assertion is checked against a statement your CI signed about a test run your own workflow performed. mipiti-verify attest-tests --junit <report> (or the action's junit-report input) turns a JUnit report into an in-toto Statement with predicateType https://mipiti.io/attestations/test-result/v1, signs it, and writes it to .mipiti/attestations/ in the checkout (or to the directory MIPITI_ATTESTATION_DIR names; the action sets that itself when the checkout is not writable by the container's user). Verification reads it and executes nothing.

Predicate schema. Published at schemas/test-result-v1.schema.json. Any producer that emits a conforming statement, signed under an identity the verifier is pinned to, is accepted; the CLI is one producer, not the interface. The load-bearing fields are commit (must equal the commit under verification), totals and selected.matched_count (a run that selected nothing or in which nothing passed is refused), and tests[] with a per-test status (the named test must itself be passed; a skip is not evidence). environment records only the variables nominated with attestation-env, and an assertion's env param requires their values.

Signing identity and what reaches the platform. The attestation is signed the same way the verification run is: keylessly through Sigstore under the CI workload identity (ci_oidc) where one exists, with a customer-held ECDSA key (customer_key) where none does, and unsigned only where neither could apply. Each test_attested result submitted to the platform carries that class in a provenance field, so the audit envelope and the platform's sufficiency inputs can weigh a workflow-signed pass against a self-declared one as data rather than by reading prose.

Tests and verification in separate jobs. .mipiti/attestations/ lives in the runner's working tree, not in the repository. If your tests run in one job and verification in another, upload that directory as a workflow artifact from the test job and download it before the verify step. This is sound because freshness is not the guard, the commit binding is: an attestation names the commit its run covered, so a file from an older run names an older commit and is refused, and a file that names the current commit could only have been produced by a run against that tree. No file committed into the repository can name its own commit, since the commit hash covers the file. What an attestation cannot say is whether something outside the tree, such as a live service, changed between the run and the read; attested_at and ci.run_url are recorded for exactly that reader.

GitLab. Keyless signing uses the id_tokens job keyword; expose the token as SIGSTORE_ID_TOKEN with audience sigstore. The retired CI_JOB_JWT_V2 is still honoured.

What the attestation now carries. Beyond the run's outcome, each recorded test is bound to its content and, optionally, to what it did:

• Definition. attest-tests locates each test in the checkout (pytest classname → module → file, or the JUnit file attribute for other runners) and records file and definition_sha256, a hash over the definition block from its decorators to the end of its body, whitespace-normalised. A parametrized id (test_x[case-1]) resolves to the function; a method's hash covers the method. Each entry says what the hash covers (definition_scope: symbol, block or file) and what isolated it (parser); see Languages for how each language is cut and what the fallback can and cannot tell apart. A test that cannot be located carries neither field. The test_attested result reports the hash as evidence_hash, so a tier-2 acceptance is bound to the definition it was given, and a changed definition is re-judged rather than carried forward.
• Reach. attest-tests --coverage <report> reads a coverage report (coverage.py JSON, LCOV, Cobertura XML, JaCoCo XML, or a directory of one report per test; see Languages) and records, per test, reached: [{file, lines}] when the report attributes lines to that test, or suite_reached when it only says what the whole run executed. When the assertion names a mechanism, the result reports reached: true|false: whether the test executed a line of that mechanism's definition. An empty reached is a fact (the run had coverage and the test touched nothing); suite_reached and a run without --coverage leave it unknown.
• Dependence. mipiti-verify attest-dependence runs each (test, mechanism) pair once with the mechanism disabled and signs the outcome into a second attestation with predicate.kind = "dependence". The result reports depends: true|false: a test that fails without the mechanism depends on it; one that still passes does not. This command runs tests. It is opt-in and lives in the job that already runs your tests next to attest-tests; run still executes nothing. Pairs come from --pair <test>=<file>::<symbol> (repeatable) or --from-model <id> (every test_attested assertion of the model that names a mechanism, fetched with the same credentials run uses). How the mechanism is disabled depends on the runner (see Runners): a pytest plugin stubs a Python symbol at import time (the module is imported at pytest configuration time, so nominate mechanisms in modules that are safe to import); jest, vitest and mocha load a setup file that mocks the module and replaces the export with a function that throws; every other language has the definition's body replaced in the source by one that aborts, compile-checked first and restored byte-for-byte afterwards. The fact is defined identically everywhere: the test's outcome is anything but passed with the mechanism disabled and the mutated tree compiled. A mutated tree that does not compile, a file with uncommitted changes, a runner that selected no test, or a mechanism that cannot be disabled records status: error with a reason, which the verifier reads as unknown, never as an outcome. Two clocks bound the command: --timeout per pair (default 300s) and --total-timeout for the whole run (default 1800s, also MIPITI_DEPENDENCE_TOTAL_TIMEOUT). A pair that would start after the total budget is spent is recorded as not run (status: error with a reason), so the attestation still names every requested pair.
• Reach, per test, for any runner. mipiti-verify attest-reach runs each nominated test alone under the language's coverage tool through the same runner adapter and signs the lines it executed in the mechanism's file into a third attestation with predicate.kind = "reach", in the same per-test reached: [{file, lines}] shape attest-tests --coverage records. Running one test at a time is what makes it a claim about that test rather than the suite, which is why an aggregate report never yields reached on its own. Only the mechanism's file is recorded. Same pair sources, same two clocks, same signing as attest-dependence; a runner whose coverage tool is missing or produced no report records status: error with the reason. Per-test reach requires running a test alone. For a harness that cannot, attest-reach --suite-cmd "<command>" --coverage-file <report> runs the suite once under coverage and records, per nominated test, what the suite reached in its mechanism's file as suite_reached, with predicate.reach_scope = "suite". That is information, not the fact: per-test reach is undefined for such a harness, so a suite-scope record never yields reached; the verifier reports reached mechanism: unknown (suite-level coverage only). attest-reach without --suite-cmd (per test, through the adapter or --run-cmd with {test}) is what establishes the fact.

The mechanism param. A test_attested assertion may name the mechanism the test is meant to exercise as mechanism: "<file>::<symbol>" (Class.method for a method; <kind>:<name> to name the kind outright, e.g. rtl/alu.sv::module:alu or rtl/fsm.sv::always:seq_logic). It is what reach and dependence are computed against, and what the tier-2 reviewer is shown next to the test.

Languages

The proofs are language-agnostic; only one question is language-specific: which lines make up the definition of (file, kind, name). It is answered by a parser where one exists and by a sound fallback otherwise, and every attestation entry says which (parser) and how exactly (definition_scope).

In an HDL, function means any subprogram (a task or procedure too), since a test is nominated by name rather than by the keyword that declared it; task and procedure are strict. definition_scope is symbol when a parser or the keyword scanner isolated exactly the named definition (a Class.method name resolves inside its class); block when the line heuristic cut a block starting at the first match of the name, which cannot tell two same-named definitions apart, so a method name duplicated across classes in one file resolves to the first; file when nothing could be isolated and the hash covers the whole file. Every scope is sound for the pin: any change to the hashed text, or a move of the name, changes the hash. parser is ast, tree-sitter, keyword or lines (absent for file). The extra downloads each grammar into a local cache on first use; where it is not installed or a grammar is unavailable the fallbacks apply and the attestation records that.

Coverage formats accepted by --coverage: coverage.py JSON (coverage json; with --show-contexts lines are attributed to tests), LCOV (.info / .lcov, including what verilator_coverage --write-info writes), Cobertura XML and JaCoCo XML. The format is detected from the content. Reach is a claim about one test, so only a report that attributes lines to a test yields reached; an aggregate report is recorded as suite_reached (informational) and reach stays unknown. To attest reach in a language whose coverage tool has no per-test contexts, run each nominated test alone and write its report into one directory as <test id>.<ext> with :: spelled __ (for example tests.test_guard__test_a.info, or test_a.info); pass that directory to --coverage and each file is read as that test's own run.

Tier 2 reads the closure. For a test_attested review the reviewer is handed the test's definition from the checkout, the named mechanism's definition, and a facts block (definition hash match, reached, fails without). The criterion is YES only if the test as shown exercises the mechanism and asserts the stated outcome; a fact of reached: no or fails without mechanism: no is a NO whatever the test text says.

Never skipped under --changed-files. An assertion whose evidence is a signed execution witness (test_attested), one that names no file at all (a glob such as test_exists, or a scope such as the sound witnesses), and one whose file is a test file (function_exists / class_exists) are always verified, in both tiers, when --changed-files is set: what a test evidences is the code it exercises, so its own file being unchanged says nothing about the claim, and a claim over a glob or a scope is not scoped by a file list at all. A test file is recognised by layout (tests/, test/, __tests__/, test_*, conftest*, *_test.*, *_spec.*, *.test.*, *.spec.*); repositories whose tests live outside the conventional layouts, e.g. specs/auth.py, add --test-file-pattern '<regex>' (also MIPITI_TEST_FILE_PATTERN), which marks additional repository-relative paths in addition to the heuristic.

      - run: pytest --junitxml=report.xml --cov --cov-context=test && coverage json --show-contexts -o coverage.json
      - uses: Mipiti/mipiti-verify@<pinned-sha> # vX.Y.Z
        with:
          junit-report: report.xml
          coverage-report: coverage.json
          # Opt-in: runs each named test once with its mechanism disabled.
          dependence-pairs: "tests/test_auth.py::test_token_required=app/auth.py::require_token"

Runners

attest-dependence and attest-reach execute tests through a runner adapter, detected from the project's files; --runner <name> (action input runner) overrides it, and --run-cmd selects the command runner. In a polyglot checkout the language of the mechanisms breaks the tie; a checkout with no marker at all is treated as pytest.

Source mutation. For Go, Rust, Java, Kotlin, C, C++, C#, Swift, Verilog, SystemVerilog and VHDL the mechanism is disabled by rewriting its definition in place for the duration of the one run: a function or method body becomes one that aborts (panic, panic!, throw, abort() with #include <stdlib.h> added when missing, fatalError); a class, struct or impl has every method body replaced; a Verilog module becomes a stub with the same header whose outputs are driven to x (a non-ANSI module keeps its body port declarations, re-emitted verbatim; a port the header names without a declaration, or a declaration the header does not name, is error with the reason); a function / task body becomes $fatal; a labelled always / initial block, a property or sequence (with every assertion that instantiates it) or a labelled assert is removed; a VHDL architecture body is emptied, a labelled process removed, a function / procedure body replaced by assert false ... severity failure. Name the kind when a bare name would be ambiguous: rtl/alu.sv::module:alu, rtl/fsm.sv::always:seq_logic, rtl/alu.sv::assert:a_no_overflow, rtl/top.vhd::process:p_clk. Source mutation needs a clean git checkout (git on PATH, the file committed with no uncommitted changes): that is how a run proves it can restore the file whatever happens. Outside a git checkout every mutation pair is error with a reason saying so; --strategy hook is the way through for the go and cargo runners and the command runner, and Python and JavaScript need no checkout at all because pytest and jest / vitest / mocha disable a mechanism at runtime rather than by rewriting a file. Four invariants hold for every mutation: the definition must be isolated exactly by the language layer (a parser, or the HDL keyword scanner, which reads the name at the block's own start; a line-heuristic block span may be a different definition, and a mutation of the wrong block can still compile, which would attribute a test's outcome to the wrong mechanism, so such a pair is error with reason definition not isolated exactly (install mipiti-verify[ast] or nominate a unique symbol)); the file must be committed with no uncommitted changes (otherwise the pair is error, so a run can never leave a change behind the tree did not already have); the mutated tree is compile- or lint-checked before the test runs (go build, cargo check, mvn compile / gradle compileJava / javac, kotlinc, cc -fsyntax-only, dotnet build, swift build / swiftc -typecheck, verilator --lint-only / slang --lint-only / iverilog -t null, ghdl -a / nvc -a, whichever is present), and a failing check is error with the tool's output as the reason, never failed; and the original bytes are written back afterwards and verified by hash, whatever happened in between.

Suite mode: dependence from a whole-suite run. A simulator or a Makefile harness often has no way to run one test, and its pass/fail is a JUnit report rather than an exit status. attest-dependence --suite-cmd "<command>" --suite-junit <report> covers that route with any runner (the runner supplies the disable strategy; the command runs the tests): pairs are grouped by mechanism, and for each distinct mechanism the mechanism is disabled (same compile/lint gate, same byte-exact restore), the suite command runs once, and the report it wrote gives every nominated test naming that mechanism its outcome: passed, failed, or error from the report as they are (an errored test did not pass, so it counts as dependence); a test the report skipped is error with reason skipped under mutation; a test absent from the report is error with reason not in report; a command that wrote no report is error with reason no report for every pair on that mechanism, as is a failed gate. --timeout applies per suite run and --total-timeout across mechanisms; a mechanism that would start after the budget records its pairs as not run. The result is the same kind: "dependence" attestation, so verification reads it unchanged. A stale report is removed before each run so an old one can never be read as this run's.

Strategy B: hook-instrumented build (--strategy hook). The mutation strategy above recompiles once per mechanism. A compiled codebase that would rather build once can place a tripwire inside each mechanism instead, and attest-dependence --strategy hook (also attest-reach --strategy hook) builds once with the tripwires compiled in, then runs each nominated test with its mechanism named. The contract, stated exactly:

• The tripwire goes inside the mechanism's own body, and nowhere else: never in a test helper, a fixture, TestMain, a constructor the tests share, or a module initialiser. It is gated out of production builds by a build flag (Go build tag mipiti_hooks, Rust feature mipiti_hooks, C/C++ MIPITI_HOOKS, Swift MIPITI_HOOKS, Verilog `MIPITI_HOOKS, a VHDL generic); Java and Kotlin have no build-time gate, so their check is compiled always and is inert unless the variable is set.
• It reads MIPITI_DISABLE_MECHANISM (a plusarg or generic for HDL) and, only when the value equals its own mechanism id, aborts with a message that carries mipiti-hook <file>::<symbol> at <file>:<line>, where <file>:<line> is the tripwire's own position. Any other value, including unset, is a no-op.
• The verifier runs the go runner as go test -c -tags mipiti_hooks (one test binary per package, built once), cargo as cargo test --no-run --features mipiti_hooks, and the command runner as --build-cmd once (with -DMIPITI_HOOKS, +define+MIPITI_HOOKS, or whatever the build takes) then --run-cmd per pair with {test} and {mechanism} substituted and the variable set. No source is rewritten and the tree need not be clean. pytest, jest, vitest and mocha refuse --strategy hook with a reason: they disable at runtime already.

Why the placement rule: a tripwire in a helper every test calls fires for every test, and one placed next to the mechanism rather than in it fires for tests that never reached the mechanism. Either would credit dependence the tests do not have. Two checks make a misplaced tripwire visible instead of credited, and both are recorded in the attestation:

1. Location proof. A failing run is credited as dependence only when its output carries the marker for this mechanism and the marker's <file>:<line> falls inside the mechanism's exactly located definition (the same symbol scope the mutation strategy requires). A test that failed without the marker records error with reason test failed without the hook firing (it could be any failure); a marker outside the span or in another file records error with reason hook fired outside the mechanism, one for another mechanism a hook for a different mechanism fired. The location is recorded on the fails_without entry as hook_location.
2. Control run. Before any pair, every nominated test runs once with MIPITI_DISABLE_MECHANISM=mipiti-control-<random>. Every test must pass. Any failure records error with reason hook fires unconditionally (control run failed) for every pair and the run stops. The run is recorded at the predicate level as control_run: {status, mechanism, tests}, and the record carries strategy: "hook".

Helper snippets, one per language (these are the whole helper; there is no library to install):

// hooks_on.go
//go:build mipiti_hooks

package guard

import ("fmt"; "os"; "runtime")

// Tripwire aborts when MIPITI_DISABLE_MECHANISM names this mechanism.
func Tripwire(id string) {
	if os.Getenv("MIPITI_DISABLE_MECHANISM") != id {
		return
	}
	_, file, line, _ := runtime.Caller(1)
	panic(fmt.Sprintf("mipiti-hook %s at %s:%d", id, file, line))
}

// hooks_off.go
//go:build !mipiti_hooks

package guard

func Tripwire(string) {}

// in the mechanism:
func RequireToken(t string) bool {
	Tripwire("internal/auth/guard.go::RequireToken")
	...
}

#[cfg(feature = "mipiti_hooks")]
macro_rules! mipiti_tripwire {
    ($id:expr) => {
        if std::env::var("MIPITI_DISABLE_MECHANISM").as_deref() == Ok($id) {
            panic!("mipiti-hook {} at {}:{}", $id, file!(), line!());
        }
    };
}
#[cfg(not(feature = "mipiti_hooks"))]
macro_rules! mipiti_tripwire { ($id:expr) => {}; }

pub fn require_token(t: &str) -> bool {
    mipiti_tripwire!("src/guard.rs::require_token");
    ...
}

/* mipiti_hooks.h */
#ifdef MIPITI_HOOKS
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#define MIPITI_TRIPWIRE(id) do { const char *v = getenv("MIPITI_DISABLE_MECHANISM"); \
    if (v && strcmp(v, (id)) == 0) { fprintf(stderr, "mipiti-hook %s at %s:%d\n", (id), __FILE__, __LINE__); abort(); } } while (0)
#else
#define MIPITI_TRIPWIRE(id) do {} while (0)
#endif

int require_token(const char *t) {
    MIPITI_TRIPWIRE("src/guard.c::require_token");
    ...
}

// No build-time gate in Java or Kotlin: compiled always, inert unless the variable is set.
final class MipitiHooks {
    static void tripwire(String id) {
        if (!id.equals(System.getenv("MIPITI_DISABLE_MECHANISM"))) return;
        StackTraceElement at = new Throwable().getStackTrace()[1];
        throw new IllegalStateException("mipiti-hook " + id + " at " + at.getFileName() + ":" + at.getLineNumber());
    }
}

@inline(__always) func mipitiTripwire(_ id: String, file: StaticString = #file, line: UInt = #line) {
    #if MIPITI_HOOKS
    if ProcessInfo.processInfo.environment["MIPITI_DISABLE_MECHANISM"] == id {
        fatalError("mipiti-hook \(id) at \(file):\(line)")
    }
    #endif
}

// inside the module, compiled with +define+MIPITI_HOOKS; the run passes +MIPITI_DISABLE_MECHANISM=<id>
`ifdef MIPITI_HOOKS
  string mipiti_target;
  initial if ($value$plusargs("MIPITI_DISABLE_MECHANISM=%s", mipiti_target) && mipiti_target == "rtl/alu.sv::module:alu")
    $fatal(1, "mipiti-hook rtl/alu.sv::module:alu at %s:%0d", `__FILE__, `__LINE__);
`endif

-- a generic on the entity, set by the simulator (-gMIPITI_DISABLE_MECHANISM=<id>); inside the architecture:
assert MIPITI_DISABLE_MECHANISM /= "rtl/alu.vhd::architecture:rtl"
  report "mipiti-hook rtl/alu.vhd::architecture:rtl at rtl/alu.vhd:" & integer'image(42) severity failure;

For a Java file the marker's <file> is the bare source file name; the location proof accepts a marker whose path ends with the mechanism's file. Reach under --strategy hook runs each test alone under coverage against the same build with the variable unset.

Suite mode: reach from a whole-suite run. attest-reach --suite-cmd "<command>" --coverage-file <report> runs the suite ONCE under coverage and reads the report (any accepted format). Every nominated test records the lines the suite executed in its mechanism's file as suite_reached, and the record carries reach_scope: "suite"; each entry's status is the command's exit (passed on 0), a command that could not run or wrote no report is error with the reason for every pair. This is stated exactly for what it is: per-test reach is undefined for a harness that cannot run one test alone, so suite mode records suite reach as information and never credits reach. Only per-test attest-reach establishes the fact.

# Verilator or Icarus harness whose Makefile runs every testbench and writes JUnit:
# one make per mechanism, the RTL mutated and linted first
mipiti-verify attest-dependence --suite-cmd "make sim JUNIT=out.xml" --suite-junit out.xml \
  --pair 'tb_alu_overflow=rtl/alu.sv::module:alu' \
  --pair 'tb_fsm_reset=rtl/fsm.sv::always:seq_logic'

Examples.

# Go: go test -run selects the test; go build checks the mutated tree; reach through -coverprofile
mipiti-verify attest-dependence --pair 'internal/auth::TestRequiresToken=internal/auth/guard.go::RequireToken'
mipiti-verify attest-reach      --pair 'internal/auth::TestRequiresToken=internal/auth/guard.go::RequireToken'

# jest: file::test name; the export is mocked for the run
mipiti-verify attest-dependence --pair 'src/auth.test.ts::rejects a missing token=src/auth.ts::requireToken'
mipiti-verify attest-reach      --pair 'src/auth.test.ts::rejects a missing token=src/auth.ts::Auth.check'

# cocotb driven by a Makefile: the command runner, the RTL mutated and linted with whichever of verilator / slang / iverilog is installed
mipiti-verify attest-dependence --run-cmd 'make -C sim sim TESTCASE={test}' \
  --pair 'test_alu_overflow=rtl/alu.sv::module:alu'

# Verilator harness: coverage written by the run and converted to LCOV, then read for the one test
mipiti-verify attest-reach --run-cmd 'make -C sim run TEST={test}' \
  --coverage-cmd 'make -C sim run TEST={test} COVERAGE=1 && verilator_coverage --write-info sim/coverage.info sim/coverage.dat' \
  --coverage-file sim/coverage.info \
  --pair 'test_alu_overflow=rtl/alu.sv::always:alu_ff'

Action Inputs

Action Output

Two-Tier Verification

Tier 1 (Mechanical) — 30 typed assertion checks, deterministic code analysis, no external API calls. No assertion type executes project code.

Every type declares the CLASS of fact its verdict reports. The class is a property of the check, not of the wording of the claim it is attached to, and it is what decides whether a pass can carry a claim about every case or only about the case it saw:

The RTL and hardware types (module_exists through register_reset) read Verilog, SystemVerilog and VHDL; the two sound witnesses read those languages through the same rules as software sources.

Sound witnesses (sink_default_deny, typed_boundary)

These two are the only types whose pass is a statement about EVERY site in a scope rather than about one place. They take no file: their subject is a scope of repository-relative paths, directories or globs.

sink_default_deny — over every source file in scope, every site of a declared sink receives, at each guarded position, only a form the declared safe_forms vocabulary accepts, or is an allowlisted site with a reviewed reason. A sink is a call, a constructor, a macro invocation, a store to a named target (an HDL blocking or non-blocking assignment, a field store) or a module instantiation. The accepted forms are literal, named_constant (a name bound once at module, class or package scope to a literal, or an HDL parameter, localparam or constant), literal_concat (every operand safe; a template with any expression part is a violation) and parameter_binding (a data structure written at the site — an array, list, tuple, map or dictionary literal — every element of which is itself one of the accepted forms; decided from the value and its elements, never from the position it sits in).

typed_boundary — every guarded sink position receives a value whose static form is a construction of boundary_type through one of the declared constructors, and every construction site of that type in scope receives only literal or named-constant arguments, or is allowlisted.

A verdict of either type reports, beside the pass or fail, how many sites of the declared sinks the run decided and how many of those stand on a reviewed exception rather than on a form it admitted. A claim about every site is worth exactly what the enumeration behind it is worth, so the run states the size of that enumeration as data a reader can act on rather than as a sentence a reader has to trust. Every run of these types states both, a refused one included: a run that decided nothing reports nothing decided, so a later run is never read against an earlier run's numbers. Neither is ever read from the assertion — a count of what a run examined is a fact only that run holds — and a check that enumerates no scope states neither.

What makes the verdict worth something is what the check REFUSES:

• A scope that matches nothing, a file it cannot read, a file whose extension names no language, a file the language's parser rejects, and a file in a language this install has no parser for are all failures. A pass never comes from an empty enumeration, and never from a search that saw a name without seeing what was handed to it. Reading a language other than Python needs the parsers: install mipiti-verify[ast] (the GitHub Action image already carries them). The refusal names the remedy.
• A link anywhere in the region a scope entry searches is a refusal, matched or not: a pattern walk does not descend through a linked directory, and a linked file names content under a path the tree does not own, so an enumeration that met one would be short of what the entry names with nothing to say so. Name the target's own path.
• A scope whose files come to more than 16 MiB together is a refusal, as is one over 5,000 files or holding a file over 2 MiB. Every file in scope is read and parsed at once, so a scope inside the other caps can still be more than a run can hold; that arrives as "narrow it", never as a killed job.
• A chain of functions forwarding into a declared sink deeper than 12 hops is a refusal: the sink set had not closed over the scope when the budget ran out, and an unclosed sink set means sites that were never enumerated. Declare the outermost of them in wrappers.
• Every site it could not classify counts as a violation. Reflection, dynamic evaluation, a macro body naming a sink, a shell invocation built from a variable, and a sink handed on as a value are violations too.
• Aliases (an import alias, a rebinding), and wrappers in scope that forward a parameter into a guarded position, are sinks themselves, found by a fixpoint over the scope. Wrappers the check cannot see are declared in wrappers.
• An allowlist entry must name a file, a site, a callee, a reason and a reviewer, and must match a site the check actually flagged. A stale entry fails the run, and the allowlist content is inside the evidence hash, so editing it reopens review. An exception excepts a site the run examined, so the list cannot be longer than the sites in scope, and a run whose every flagged site is an exception — with nothing anywhere in the scope admitted by form — has decided nothing mechanically and is a refusal, as vacuous as a scope the declared sinks never occur in.

parameter_binding is decided by what the structure was written with, because an element of a structure reaches the callee as surely as a value at the position does: a structure holding an interpolation, a name that is not a constant, a call or another structure is a violation, and so is one no element could be read from. Whether a callee treats such a value as data or as the statement it runs is a property of the callee, which this check does not read — the same boundary every other form stops at — so a sink that takes bound values in a later argument is declared by naming the statement position in positions, which leaves the data positions unguarded.

The residual, stated in the result and reviewed by tier 2, is the sink list itself: a sink reached under a name that appears in neither sinks nor wrappers is not enumerated. Tier 2 is shown the inventory the mechanical tier built — every site with each argument's static form, every undeclared call into the sinks' receivers, every allowlisted site with its reason, and how many files each parser read — and answers whether the declared sinks are the sinks through which the stated property could be violated in that code. It never re-scans.

Two optional signed statements upgrade the two residuals the repository content cannot settle on its own: attest-construction records that your toolchain refuses a probe that builds the boundary type from a non-literal, and attest-allowlist-review records who stands behind the reviewed exceptions at this commit. Neither changes the verdict; both are stated in the facts a reader sees.

Tier 2 (Semantic) — AI evaluates whether matched code actually implements the control's intent. Supports OpenAI, Anthropic, and Ollama (local).

Sufficiency — evaluated server-side: do all assertions collectively cover every aspect of the control?

Formal Verification

The verification pipeline is formally verified using TLA+ specifications with independent model checking (TLC), exhaustive state exploration, and cross-checks against the real code. Key guarantees: all error paths fail-closed (no silent PASS), and LLM semantic checks can never override mechanical verification failures.

See formal/README.md for the full methodology, invariants, and verification chain.

Development

git clone https://github.com/Mipiti/mipiti-verify.git
cd mipiti-verify
pip install -e ".[dev]"
python -m pytest -v

Updating dependencies

After changing dependencies in pyproject.toml, regenerate the lockfiles:

pip install uv
python lock-deps.py

This produces requirements.lock and requirements-all.lock with SHA-256 hashes. Commit them alongside pyproject.toml changes.

License

Proprietary. Copyright (c) 2026 Mipiti, Inc. All rights reserved. See LICENSE for details.