tools/evidence/generate.sh regenerates every tier (traceability, tests, Lean, Tamarin, lint) from a clean checkout into the verification report — the page you are reading quotes that artifact.

tools/evidence/generate.sh

Jobs: rust-core (fmt, clippy -D warnings, tests) · supply-chain (cargo-deny, cargo-audit, CycloneDX SBOM) · tier1 (bounded fuzz + Kani) · tier2 (Lean build + oracle-trace staleness gate + replay) · tier3 (Tamarin, advisory) · ios-shell (swift build + test) · traceability import.

.github/workflows/ci.yml

Rust 1.97.1, Lean v4.32.0 and the dependency graph are pinned; a written dependency budget bounds what may enter the build, enforced by cargo-deny (two documented build-time-only advisory ignores).

docs/dependency-budget.md · deny.toml

A reproducible harness fetches the reference issuer's live OpenID4VCI metadata over platform TLS (HTTP 200, 27 configurations — 11 in the SD-JWT VC format this wallet implements) and confirms the reference verifier is reachable. The iOS app runs the same fetch on its real URLSession stack. Reachability + wire-shape only — not a conformance pass.

tools/interop/probe.sh · docs/certification-evidence/interop.md

CycloneDX 1.3 SBOMs are published in-repo (21 crates; wallet-core = 111 runtime components), regenerable from a clean checkout — not just generated transiently in CI.

docs/certification-evidence/sbom/ · tools/evidence/sbom.sh

Published hot-path numbers against the real backend (ES256 sign ~28.7µs / verify ~83.6µs, SHA-256 ~58ns, SD-JWT parse ~430ns; release, 2026-07-19), reproducible with one command.

docs/certification-evidence/perf-benchmarks.md · crates/benches/

Release signing, build provenance/reproducibility, and a published vulnerability-disclosure policy are planned. Threat model, DPIA, key-lifecycle and KAT documents remain stubs pending publication in the certification-evidence set.

docs/certification-evidence/

No published disclosure policy yet — planned alongside the certification evidence set.

docs/certification-evidence/ (pending)