Formal-verification (Kani) harnesses cover only contracts/lib (balance/access-control/oracle proofs) - extend to lending, fees, and border math

[nanaf6203-bit]

Context: .github/workflows/formal-verification.yml runs Kani on contracts/lib harnesses (balance_proofs, access_control_proofs, oracle_proofs) only; lending (LTV/interest), fees (rounding invariant), and staking (snapshot arithmetic) have unsafe-by-design arithmetic that formal methods would pin.

Problem: The workflow provides proof airtightness for one helper crate while the entities with real value-movement math (lending borrow overflow handled but rate math unwired, fees distribute remainder) remain unchecked; a saturating/overflow regression there ships with no formal backstop.

Proposed approach: Add Kani harnesses for borrow_rate::compute_borrow_rate, fee rounding (derive dust-bound), and staking reward-points math; wire them in formal-verification.yml; keep mdbook-verification docs in sync.

Acceptance criteria: lending/fees/staking harnesses added and green in CI; docs list the new proofs.

[NickiM84]

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

Hello, I'm a fullStack developer with years of experience, I have worked on several projects, can I please work on this

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

[drips-wave]

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

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