Add formal verification for critical contract invariants

[Smartdevs17]

Description

Critical invariants (total supply consistency, balance preservation) are untested formally. Implement formal verification using Certora or similar tools.

Acceptance Criteria

• Formal specification for critical invariants
• Certora Prover integration
• Invariant: total deposits = total debt + reserves
• Invariant: health factor consistency during operations
• Invariant: interest accrual monotonicity
• CI gate on verification failure

Technical Scope

• stellar-lend/contracts/lending/src/spec/
• .github/workflows/formal-verification.yml
• docs/FORMAL_VERIFICATION.md
• Edge: specification completeness, prover timeout, false positive handling

[TUPM96]

Opened PR: #398

This adds the protocol-level formal invariant suite requested here:

• total_deposits = total_debt + reserves across deposit/borrow/repay transitions
• health factor consistency with liquidation boundary and collateral/debt changes
• monotonic interest index accrual under non-decreasing timestamps
• Kani harnesses for bounded model checking
• CI workflow/docs updates for the focused protocol formal spec gate

Verified locally with:

• cargo fmt -p stellarlend-lending --check
• cargo check -p stellarlend-lending --features spec
• cargo test -p stellarlend-lending --features spec --test protocol_formal_specs -- --test-threads=4
• cargo test -p stellarlend-lending --features spec --release --test protocol_formal_specs -- --test-threads=4
• cargo clippy -p stellarlend-lending --features spec --test protocol_formal_specs -- -D warnings -A unused-imports -A dead-code -A unexpected-cfgs -A clippy::module_name_repetitions -A clippy::too-many-arguments -A clippy::manual-clamp -A clippy::manual-range-contains -A clippy::let-and-return
• git diff --check

[DevSolex]

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

Hi Maintainer,

I’m a smart contract and full-stack developer interested in contributing to this issue. I’m an experienced contributor with hands-on experience in Rust, Soroban, Cairo, and TypeScript.

I’m passionate about building secure and scalable blockchain solutions, with a strong focus on writing clean, maintainable code. Based on the scope of this issue, I’m confident I can deliver a complete solution within 24 hours of assignment(ETA).
I would appreciate the opportunity to contribute and help move this forward.

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

[Manuelshub]

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

Hello @Smartdevs17, I'd love to work on this issue, can I take a stab at it??

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

[Wetshakat]

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

Gm maintainer
I will like to work on this issue
ETA 2hrs

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

[Suzan-max]

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

I would like to work on this

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