Consumer-side verifier orchestration for the `#[cfg(kani)]` /
`#[test]` harnesses shipped throughout the workspace. The
runner-shape we need to actually exercise the proof harnesses
we've been adding all session.
Ported in spirit (not bytes) from ai-verify's `audit_core::proof`
+ `audit_core::process` modules per the user's wave-4 directive.
Refined per the SOTA brief:
- **`cargo kani --harnesses <regex>` and `cargo miri test
[filter]`** as the discovery mechanism. NO custom AST walk —
cargo already indexes harnesses; the brief was explicit there
is no public API for enumerating `#[kani::proof]` symbols
outside Kani's frontend.
- **CI/soak timeout convention** from the AWS Kani case study +
rustls/s2n-quic harnesses: 5 min per run in CI, 60 min in
nightly soak. Default `ProofConfig::timeout = 300 s`.
- **Prusti / Creusot deferred** — annotation-heavy research
tools, not orchestration targets in v1.
- **Skip cargo audit / cargo deny / clippy** — those have their
own runners; this crate is verification-specific.
Energy as the orthogonal trust anchor: every `ProofResult`
carries `joules_uj` computed from wall-clock elapsed × a
configurable `joules_per_cpu_sec` rate (default 20 J/s
≈ a laptop CPU under load). `energy_provenance` is `Estimator`
at v1 — consumer swaps in a hardware shunt when available. The
rolled-up `ProofReport.total_joules_uj` is the budget owner's
single number for "how much energy did verification cost?"
Surface:
- `ProofConfig { timeout, joules_per_cpu_sec, workdir, verbose }`
with sensible CI defaults.
- `ProofStatus { Passed, Failed, Timeout, Error }` — four-valued
so timeouts are distinguishable from failures.
- `ProofResult { tool, scope, status, joules_uj, elapsed_ms,
stderr_excerpt }`.
- `ProofReport { results, kani_available, miri_available,
total_joules_uj, energy_provenance }` with `passed()` +
`failed()` rollups.
- `run_kani(filter?, &config)` / `run_miri(filter?, &config)` /
`run_audit(&config)` (both tools) / `run_audit_in(path,
timeout)` (path-scoped convenience).
- `is_kani_available()` / `is_miri_available()` for environment
probes.
- Per-process wall-clock timeout via poll-every-100ms +
kill-on-expiry. Stderr captured + truncated to 400 chars for
the report.
Honest scope spelled out:
- Kani does NOT prove unbounded loops; `Passed` means "no
counterexample within `--default-unwind N`."
- MIRI does NOT prove the absence of UB; it finds UB on paths
it actually executes. Coverage is mandatory.
- Subprocess runner is NOT sandboxed.
12 tests cover: joule estimation default rate + zero-elapsed
edge; stderr truncation empty + 400-char cap; ProofReport
default clean; passed() + failed() rollups (Failed + Timeout
both count as failed); ProofStatus + ProofResult JSON round-
trip; tool-availability is pure query; missing-binary returns
SpawnError; ProofConfig default sensible; run_kani returns a
valid status regardless of whether kani is installed.
Co-Authored-By: Claude Opus 4.7 <[email protected]>
bd7074a797