Add lending protocol formal invariant specs

[TUPM96]

Resolves #384

Summary

• wire the lending spec modules so the spec feature compiles cleanly
• add a pure Rust protocol model for deposits = debt + reserves, health factor consistency, and monotonic interest accrual
• add 13 focused protocol invariant lemmas plus Kani harnesses for bounded model checking
• add a focused integration test target and update the formal verification workflow/docs so the new invariants are CI-gated
• apply rustfmt to the lending package files touched by the spec feature

Verification

• 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

Note

Kani is used here as the Rust/Soroban model checker, analogous to Certora for Solidity/EVM projects, while keeping the verification target native to this repository.

[vercel]

@TUPM96 is attempting to deploy a commit to the smartdevs17's projects Team on Vercel.

A member of the Team first needs to authorize it.

[Copilot]

Copilot encountered an error and was unable to review this pull request. You can try again by re-requesting a review.