Formal verification of share accounting math

[robertocarlous]

Description

Perform formal verification of the vault's share accounting math using a proof assistant or model checker to mathematically prove correctness properties.

Use Case

Share accounting is the core economic mechanism. Bugs here could lead to fund loss. Formal verification provides the highest level of assurance.

Properties to Verify

• TotalShares never exceeds sum of all user shares
• No user share balance can go negative
• Exchange rate is monotonically non-decreasing (with yield)
• Deposit/withdrawal round-trip preserves value within rounding tolerance
• Rounding always favors the vault (never the user)

Acceptance Criteria

• Property specification document
• Kani model checker proofs for key properties
• Automated proof runs in CI
• All properties pass on current codebase
• Proof maintenance process for code changes
• Document properties and proofs in docs/FORMAL_VERIFICATION.md

Technical Notes

• Kani is well-suited for Rust formal verification
• Build on existing property tests as specification

[bobo-24]

Hi! I came across this issue and would love to work on it. I have experience with similar tasks and I'm confident I can investigate, implement a clean solution, and thoroughly test it before submitting a PR. If the issue is still open, I would appreciate it if you could assign it to me. I’ll prioritize this immediately and ensure a reliable solution is delivered as soon as possible. Thank you!

[josephchimebuka]

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

Hi GM, I have reviewed this issue and taken the time to understand the requirements, current implementation, and the expected outcome. Based on my analysis, I believe this is something I can successfully handle and contribute to... Kindly assign

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

[karanjadavi]

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

can i work on this issue

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

[shadrackmanfred]

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

Hi Maintainer! I'm a senior developer with experience building high-quality, production-ready software. I'd love to take on this issue and deliver a clean, well-tested solution that aligns with the project's standards. Please assign it to me—I'm ready to get started and contribute effectively.

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

[Hayatt74]

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

Hi I’d love to work on this issue

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

[drips-wave]

Congratulations, @josephchimebuka! 🎉 Your application was accepted by the repo's maintainers, and the issue is due on August 31, 2026.

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

[josephchimebuka]

Delivered in merged PR #721. GitHub only auto-closed #673 because the PR used Closes #673, #672, #668, and #669 — only the first number after a closing keyword is recognized. Closing this issue now to match that PR.