Formal-verification annotations (kani-ready)

[Miracle656]

Background

Adding #[kani::proof] annotations to invariants pays off later when full kani runs are feasible. Even without running, the annotations document intent.

What to build

Annotate key invariants (signature low-S, nonce monotonicity, expiration) with #[kani::proof] proof harnesses guarded by #[cfg(kani)].

Key files

• contracts/wallet/src/auth/proofs.rs (new)

Acceptance criteria

• At least 3 proof harnesses
• Documented in contracts/wallet/PROOFS.md

Drips Wave · Complexity: Advanced · 200 points

[GauravKarakoti]

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

Allow me to work on this one

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

[samad13]

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

hi, let me work on this

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

[QueenColly]

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

I am an experience rust developer, I can help with this

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

[Jaydbrown]

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

hello maintainer, kindly assign this issue, i am sure of my expertise in resolving it

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

[drips-wave]

Congratulations, @Jaydbrown! 🎉 Your application was accepted by the repo's maintainers, and the issue is due on June 2, 2026.

🧑‍💻 @Jaydbrown: 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 🌊