Kani formal verification of stealth-registry invariants #108

Extra labels: security, formal-verification
Tier: L (5-7 days) | Type: security

Context. stealth-registry has correctness-critical invariants (registration → resolution round trip, no double-registration, expiry monotonicity). Property-tests catch bugs by sampling; Kani proves them. Prove the top 3 invariants.

Scope.

• Set up Kani in stealth-registry/src/proofs/.
• Prove: (a) register-then-resolve returns the exact registered payload, (b) no two active registrations share the same key, (c) expiry strictly monotonic per key.
• Add CI job that runs proofs on push.
• Document the shape of each proof in stealth-registry/README.md.

Acceptance.

• Three named proofs pass in CI in under 5 minutes
• Failure of any proof fails the CI job
• stealth-registry/README.md documents each proof's claim and its non-goal

Files. stealth-registry/src/proofs/, .github/workflows/ci.yml, stealth-registry/README.md.