Verification
Every load-bearing claim in AgentTrust has an independently checkable artifact — a Kani proof, a devnet tx signature, a localnet test, a cron job. This section indexes them.
If you're a judge with five minutes, start with Live evidence — every claim with a clickable Explorer URL.
If you're a developer debugging a specific property, jump straight to the relevant per-claim page below.
Pages
Live evidence
Consolidated index — Kani 6/6 + 635 sub-checks, devnet smoke, chained validation, capability namespaces, daily-smoke cron. Every claim with an Explorer URL.
Kani proofs
Six machine-checked invariants over the pure-Rust composer. Per-harness deep-dive: file path, sub-check count, time, what it proves, what it doesn't.
Devnet smoke
The Pay.sh + AgentTrust atomic-settlement trace on Solana devnet — gate, transfer, emit_feedback CPI, all in one tx, with reproduction commands.
Chained validation
The four-signature RequireValidation → respond → Allow trace that proves the third ERC-8004 leg actually closes the loop.
Atomic-tx invariant
Three layers of proof — compile-time literal-type guard, runtime throw, composer structure — plus the on-chain Kani strict-correctness binding.
Adversarial harness
Fourteen hostile-scenario assertions in tests/adversarial.spec.ts that exercise the gate against malformed PDAs, replayed proofs, and corrupted state.
Custom attestor
Register an AttestorProfile, respond to validation requests, revoke attestations. Full lifecycle with the live four-signature devnet trace.
Live evidence
Every AgentTrust claim with an independently checkable artifact — Kani proofs, devnet tx signatures, localnet tests, cron jobs, hosted endpoints. One page.