Kani formal verification of stealth-registry invariants

[truthixify]

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.

[Michvista]

@Michvista has applied to work on this issue as part of the Stellar Wave Program's 7th wave.

Please assign this issue to me please

ℹ️ Repo Maintainers: To accept this application, review their application or assign @Michvista to this issue.

[drips-wave]

Congratulations, @Michvista! 🎉 Your application was accepted by the repo's maintainers, and the issue is due on July 30, 2026.

🧑‍💻 @Michvista: Please resolve the issue such that the repo's maintainers have enough time to review your contribution before the due date. You'll earn Points for completing the issue on-time, which will make you eligible for a share of the Stellar Wave Program's reward pool.

Warning

When opening a PR, please link it to this issue to ensure it gets tracked accurately. Points are awarded when this issue is marked as completed by the maintainer.

🤠 Repo maintainers: Please keep an eye on the contributor's progress and review their work before the due date. You can manage this issue, including adjusting its complexity and points, here.

🌊 Happy Wave 🌊