Verification
Mint uses layered checks.
Each check has a narrow proof boundary.
No single check proves the full containment invariant.
Proof map
Section titled “Proof map”| Check | Proves | Does not prove |
|---|---|---|
| Formatter and compiler checks | Rust syntax and type correctness | Runtime policy or custody behavior |
| Clippy with warnings denied | Lint-clean workspace targets | Production configuration |
| Workspace tests | Declared unit and integration contracts | Live host identity or vendor behavior |
| Zero-leak gate | Hermetic leak and exfil tests keep a fresh sentinel out of output | Production network topology |
| Local probe | Placeholder-to-fake-vendor flow, denial, audit, and local zero-leak behavior | Tailnet identity and production custody |
| Remote probe | Production-shaped allow, deny, and sanitized verifier behavior | Every route and every consumer |
| Doctor | Effective startup declarations and bounded custody self-test | A running broker |
| Health endpoint | Live audit admission and declaration generation | Upstream success or complete route coverage |
| Audit verify | Surviving ledger chain integrity | Absence of leaks outside the ledger |
| Release preflight | Immutable bundle shape, parser compatibility, and content addressing | Service readiness after activation |
| Release activation | Atomic target switch, readiness, runtime evidence, and rollback | Consumer migration completeness |
Repository gate
Section titled “Repository gate”Run the repository gate from the repository root.
cargo fmt --all -- --check
This checks formatting without changing files.
cargo clippy --workspace --all-targets -- --deny warnings
This rejects lint warnings in workspace targets.
cargo test --workspace
This runs unit and integration contracts.
./scripts/zero-leak-check.sh
This runs hermetic leak, exfiltration, remote-probe, and shell checks.
The continuous-integration workflow runs these gates on Linux.
It also runs secret scanning and dependency checks.
It runs a macOS probe for keychain behavior.
These gates do not read production secrets.
Runtime checks
Section titled “Runtime checks”Run policy validation before changing a declaration.
mint policy check <policy-file>
Run doctor against the same effective paths as serve.
mint doctor
Add a synthetic self-test alias only when custody setup supports it.
mint doctor --self-test-alias secret://service/name
Doctor proves startup admission and declaration parsing.
Doctor does not bind or query a running listener.
Query live health after starting the service.
curl --fail http://127.0.0.1:4949/healthz
Health 200 proves live audit admission.
Health 503 proves live admission is blocked.
Health does not prove a credentialed call completed.
Behavior tests
Section titled “Behavior tests”Reload tests cover atomic policy and authenticator replacement.
Audit-gate tests cover unresolved effects and failed durable writes.
Breaker tests cover host independence and HTTP status classes.
Indeterminate tests cover body-read, connect, and timeout failures.
Release tests cover content-addressed activation and rollback.
Remote-probe tests cover sanitized evidence and forbidden artifacts.
The tests use local fakes or hermetic fixtures.
They do not prove production ACL configuration.
They do not prove every deployed declaration is current.
Zero-leak checks
Section titled “Zero-leak checks”The local probe generates a test value at runtime.
It sends a placeholder to a fake vendor.
The fake vendor receives the resolved value.
The caller response does not contain that value.
The audit and broker output do not contain that value.
The zero-leak script generates a separate sentinel.
It captures test output before scanning it.
A sentinel match fails the gate even if a test assertion is weakened.
These checks prove the exercised surfaces only.
They do not prove arbitrary external tools cannot leak a value.
They do not prove unexercised aliases or routes.
Remote probe boundaries
Section titled “Remote probe boundaries”The remote probe uses a harmless placeholder.
Its verifier receives sanitized artifacts.
Its final result contains no credential value.
The probe checks one allow route and one deny route.
It checks that the deny path contacts no vendor.
It checks correlated audit events and resolution counts.
It does not publish private receiver coordinates.
It does not publish production receipt contents.
It does not replace route-by-route consumer verification.
Release checks
Section titled “Release checks”Stage the bundle before activation.
Run the candidate's preflight.
Run the effective systemd contract check.
Activate only with an expected previous target.
Wait for health within the configured readiness budget.
Check restart count and unresolved audit effects.
Keep the candidate only after durable evidence succeeds.
A release digest proves the bundle bytes at staging time.
It does not prove the host loaded every intended environment setting.
Freshness
Section titled “Freshness”Each page frontmatter records generatedAtSha and its covered source globs. generatedAtSha is the sole committed freshness baseline for the page's covered source set.
The freshness script compares covered paths changed from generatedAtSha through HEAD, plus staged, unstaged, and untracked paths. Editing the page does not bypass a covered source change.
Refresh generatedAtSha and review the source map after source changes.
Source map
Section titled “Source map”- CI workflow declares formatter, compiler, test, leak, scan, platform, and public-site jobs.
- GitHub Pages workflow verifies the site, requests Pages enablement, uploads
site/dist, and deploys the verified artifact. - Secret-scan fixture policy permits only explicit fake credentials, the shared fixture stub, and Mint placeholders.
- Historical scan exceptions pin each false positive to one commit, file, rule, and line.
- Doctor checks define startup checks.
- Doctor boundaries define reload, readiness, and custody scope.
- Health endpoint defines live status.
- Release preflight defines candidate validation.
- Release activation defines readiness and rollback.
- Audit verification exposes secret-free ledger checks.
- Local probe exercises placeholder forwarding and zero-leak assertions.
- Remote probe exercises the production-shaped zero-disclosure path.
- Zero-leak gate scans hermetic test output for a fresh sentinel.
- Reload coverage covers atomic generations.
- Audit coverage covers fail-closed admission.
- Breaker coverage covers incomplete upstream responses.
- Release coverage covers activation and rollback.
- Remote verifier coverage covers sanitized receipts and artifact rules.
- Freshness checker compares committed and working-tree source changes against page coverage.
- Freshness fixture covers committed and uncommitted stale-page cases.