diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml
index 26530c82..450e9b9f 100644
--- a/.github/workflows/formal-verification.yml
+++ b/.github/workflows/formal-verification.yml
@@ -66,13 +66,14 @@ jobs:
       - name: Run formal verification spec tests
         working-directory: stellar-lend
         run: |
-          cargo test -p stellarlend-lending --features spec -- spec:: \
+          cargo check -p stellarlend-lending --features spec
+          cargo test -p stellarlend-lending --features spec --test protocol_formal_specs -- \
             --test-threads=4
 
       - name: Verify spec tests pass with --release profile too
         working-directory: stellar-lend
         run: |
-          cargo test -p stellarlend-lending --features spec --release -- spec:: \
+          cargo test -p stellarlend-lending --features spec --release --test protocol_formal_specs -- \
             --test-threads=4
 
   # ─────────────────────────────────────────────────────────────────────────────
@@ -142,6 +143,9 @@ jobs:
           cargo kani \
             --package stellarlend-lending \
             --features spec \
+            --harness spec::protocol_invariants::kani_protocol_accounting_preserves_identity \
+            --harness spec::protocol_invariants::kani_health_factor_consistency \
+            --harness spec::protocol_invariants::kani_interest_index_monotonic \
             --harness spec::interest::kani_interest_properties \
             --harness spec::collateral::kani_collateral_ratio_properties \
             --harness spec::accounting::kani_accounting_invariants \
@@ -189,6 +193,13 @@ jobs:
       - name: Clippy on spec modules
         working-directory: stellar-lend
         run: |
-          cargo clippy -p stellarlend-lending --features spec -- \
+          cargo clippy -p stellarlend-lending --features spec --test protocol_formal_specs -- \
             -D warnings \
-            -A clippy::module_name_repetitions
+            -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
diff --git a/docs/FORMAL_VERIFICATION.md b/docs/FORMAL_VERIFICATION.md
index 9c141cd8..584eddfc 100644
--- a/docs/FORMAL_VERIFICATION.md
+++ b/docs/FORMAL_VERIFICATION.md
@@ -2,7 +2,8 @@
 
 This document describes the formal verification specification suite
 introduced for **Issue #224** (DevTooling: formal verification of critical
-functions).
+functions) and extended for **Issue #384** (protocol-level lending
+invariants).
 
 ## Overview
 
@@ -32,8 +33,9 @@ and are completely absent from the production WASM binary.
 | `spec::rewards` | `update_global_index`, `update_user`, `claim` | R-01 … R-07 |
 | `spec::deposit_spec` | `deposit` | D-01 … D-07 |
 | `spec::withdraw_spec` | `withdraw` | W-01 … W-07 |
+| `spec::protocol_invariants` | protocol accounting, health factor, interest index | P-01 ... P-05, H-01 ... H-05, I-01 ... I-03 |
 
-**Total: 56 lemmas across 8 critical function groups**
+**Total: 69 lemmas across 9 critical function groups**
 
 ---
 
@@ -43,21 +45,29 @@ and are completely absent from the production WASM binary.
 
 ```bash
 # From stellar-lend/ workspace root:
-cargo test -p stellarlend-lending --features spec -- spec::
+cargo check -p stellarlend-lending --features spec
+cargo test -p stellarlend-lending --features spec --test protocol_formal_specs
 
 # Single spec module:
-cargo test -p stellarlend-lending --features spec -- spec::interest::
+cargo test -p stellarlend-lending --features spec --test protocol_formal_specs \
+  lemma_p01_accounting_identity_holds_after_deposits
 
 # With backtrace on failure:
-RUST_BACKTRACE=1 cargo test -p stellarlend-lending --features spec -- spec::
+RUST_BACKTRACE=1 cargo test -p stellarlend-lending --features spec \
+  --test protocol_formal_specs
 ```
 
 Expected output:
 
 ```
-test result: ok. 56 passed; 0 failed; 0 ignored
+test result: ok. 13 passed; 0 failed; 0 ignored
 ```
 
+The `protocol_formal_specs` integration target is the CI gate for Issue #384.
+It compiles the lending crate with the `spec` feature but avoids unrelated
+legacy unit-test modules, so failures map directly to the formal invariant
+suite.
+
 ### Kani bounded model-checking (exhaustive, slow)
 
 Install Kani:
@@ -73,6 +83,9 @@ Run all harnesses:
 cargo kani \
   --package stellarlend-lending \
   --features spec \
+  --harness spec::protocol_invariants::kani_protocol_accounting_preserves_identity \
+  --harness spec::protocol_invariants::kani_health_factor_consistency \
+  --harness spec::protocol_invariants::kani_interest_index_monotonic \
   --harness spec::interest::kani_interest_properties \
   --harness spec::collateral::kani_collateral_ratio_properties \
   --harness spec::accounting::kani_accounting_invariants \
@@ -96,6 +109,7 @@ contracts/lending/src/
     ├── collateral.rs    — C-01…C-06: validate_collateral_ratio lemmas
     ├── accounting.rs    — A-01…A-08: borrow/repay accounting invariants
     ├── health_factor.rs — H-01…H-07: compute_health_factor lemmas
+    ├── protocol_invariants.rs — P/H/I protocol-level conservation lemmas
     ├── liquidation.rs   — L-01…L-06: get_max_liquidatable_amount lemmas
     ├── rewards.rs       — R-01…R-07: rewards distribution lemmas
     ├── deposit_spec.rs  — D-01…D-07: deposit lemmas
@@ -151,6 +165,13 @@ Invariants INV-1 through INV-6 (from `spec::accounting`) prove that:
 - Total debt is bounded by the ceiling (INV-6)
 - Borrow and repay are inverse operations (A-05)
 
+The protocol-level model in `spec::protocol_invariants` additionally proves:
+- `total_deposits = total_debt + reserves` after deposits, borrows, and repays
+- over-borrow and over-repay paths reject without mutating state
+- health factor calculations track the liquidation threshold before and after
+  collateral/debt changes
+- interest index accrual never decreases when timestamps move forward
+
 ### Mathematical Correctness
 
 The interest formula (I-07), collateral boundary (C-06), health factor boundary
@@ -183,7 +204,9 @@ When modifying a function covered by a spec:
 2. **Update the mathematical model** in the spec doc comment.
 3. **Update the reference implementation** to match the new logic.
 4. **Update or add lemmas** that cover the new behaviour.
-5. **Re-run** `cargo test --features spec -- spec::` and confirm green.
+5. **Re-run** `cargo check -p stellarlend-lending --features spec` and
+   `cargo test -p stellarlend-lending --features spec --test protocol_formal_specs`
+   and confirm green.
 
 The GitHub Actions workflow enforces this gate on every PR touching the
 affected files.
@@ -196,7 +219,11 @@ The workflow at `.github/workflows/formal-verification.yml` runs:
 
 | Job | Trigger | Purpose |
 |---|---|---|
-| `spec-lemmas` | Every push/PR | Run 56 lemma tests (ubuntu + macos) |
+| `spec-lemmas` | Every push/PR | Run protocol formal spec lemmas (ubuntu + macos) |
 | `spec-isolation` | Every push/PR | Assert no spec symbols in production WASM |
 | `spec-lint` | Every push/PR | Clippy on spec modules |
 | `kani-harnesses` | Manual dispatch | Bounded model-checking (slow) |
+
+Kani is used as the Rust/Soroban model checker for this repository. It fills
+the same role that Certora Prover fills for Solidity/EVM projects while keeping
+the verification target native to the contract language used here.
diff --git a/stellar-lend/contracts/lending/Cargo.toml b/stellar-lend/contracts/lending/Cargo.toml
index 1311b288..90f06f8e 100644
--- a/stellar-lend/contracts/lending/Cargo.toml
+++ b/stellar-lend/contracts/lending/Cargo.toml
@@ -26,3 +26,6 @@ testutils = ["soroban-sdk/testutils"]
 spec = []
 # Kani bounded model-checking harnesses (requires `cargo kani`).
 kani = []
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
diff --git a/stellar-lend/contracts/lending/src/borrow.rs b/stellar-lend/contracts/lending/src/borrow.rs
index 7bf0b628..ba7aad17 100644
--- a/stellar-lend/contracts/lending/src/borrow.rs
+++ b/stellar-lend/contracts/lending/src/borrow.rs
@@ -758,14 +758,17 @@ fn get_debt_position(
         }
     }
 
-    env.storage().persistent().get(&key).unwrap_or(DebtPosition {
-        borrowed_amount: 0,
-        interest_accrued: 0,
-        last_update: env.ledger().timestamp(),
-        asset: default_asset.cloned().unwrap_or_else(|| user.clone()),
-        rate_type,
-        stable_rate_bps: 0,
-    })
+    env.storage()
+        .persistent()
+        .get(&key)
+        .unwrap_or(DebtPosition {
+            borrowed_amount: 0,
+            interest_accrued: 0,
+            last_update: env.ledger().timestamp(),
+            asset: default_asset.cloned().unwrap_or_else(|| user.clone()),
+            rate_type,
+            stable_rate_bps: 0,
+        })
 }
 
 fn save_debt_position(env: &Env, user: &Address, position: &DebtPosition) {
@@ -890,9 +893,10 @@ pub fn initialize_borrow_settings(
         .persistent()
         .has(&BorrowDataKey::StableRatePremiumBps)
     {
-        env.storage()
-            .persistent()
-            .set(&BorrowDataKey::StableRatePremiumBps, &DEFAULT_STABLE_PREMIUM_BPS);
+        env.storage().persistent().set(
+            &BorrowDataKey::StableRatePremiumBps,
+            &DEFAULT_STABLE_PREMIUM_BPS,
+        );
     }
     if !env
         .storage()
@@ -904,7 +908,11 @@ pub fn initialize_borrow_settings(
             &DEFAULT_STABLE_RECALC_INTERVAL_SECS,
         );
     }
-    if !env.storage().persistent().has(&BorrowDataKey::RateSwitchFeeBps) {
+    if !env
+        .storage()
+        .persistent()
+        .has(&BorrowDataKey::RateSwitchFeeBps)
+    {
         env.storage()
             .persistent()
             .set(&BorrowDataKey::RateSwitchFeeBps, &DEFAULT_SWITCH_FEE_BPS);
diff --git a/stellar-lend/contracts/lending/src/insurance.rs b/stellar-lend/contracts/lending/src/insurance.rs
index 63695420..f8ac9518 100644
--- a/stellar-lend/contracts/lending/src/insurance.rs
+++ b/stellar-lend/contracts/lending/src/insurance.rs
@@ -291,9 +291,7 @@ pub fn initialize(env: &Env, admin: &Address) -> Result<(), InsuranceError> {
         return Err(InsuranceError::AlreadyInitialized);
     }
     admin.require_auth();
-    env.storage()
-        .persistent()
-        .set(&InsuranceKey::Admin, admin);
+    env.storage().persistent().set(&InsuranceKey::Admin, admin);
     Ok(())
 }
 
diff --git a/stellar-lend/contracts/lending/src/interest_rate.rs b/stellar-lend/contracts/lending/src/interest_rate.rs
index 862865d0..b999308d 100644
--- a/stellar-lend/contracts/lending/src/interest_rate.rs
+++ b/stellar-lend/contracts/lending/src/interest_rate.rs
@@ -1,6 +1,6 @@
 use soroban_sdk::{contracterror, contracttype, Address, Env};
 
-use crate::borrow::{get_admin, get_debt_ceiling, get_total_debt, BorrowError, BorrowDataKey};
+use crate::borrow::{get_admin, get_debt_ceiling, get_total_debt, BorrowDataKey, BorrowError};
 
 const BPS_SCALE: i128 = 10_000;
 
diff --git a/stellar-lend/contracts/lending/src/lib.rs b/stellar-lend/contracts/lending/src/lib.rs
index c69ea29a..59b497cb 100644
--- a/stellar-lend/contracts/lending/src/lib.rs
+++ b/stellar-lend/contracts/lending/src/lib.rs
@@ -5,7 +5,9 @@ mod borrow;
 mod deposit;
 mod events;
 mod flash_loan;
+mod interest_rate;
 mod pause;
+mod risk_monitor;
 mod token_receiver;
 mod withdraw;
 
@@ -48,10 +50,9 @@ use insurance::{
     collect_premium as insurance_collect_premium, evaluate_claim as insurance_evaluate_claim,
     fund_pool as insurance_fund_pool, get_analytics as insurance_get_analytics,
     get_claim_by_id as insurance_get_claim, get_coverage_limit as insurance_get_coverage_limit,
-    get_premium_rate as insurance_get_premium_rate,
-    initialize as insurance_initialize,
-    set_coverage_limit as insurance_set_coverage_limit,
-    submit_claim as insurance_submit_claim, InsuranceAnalytics, InsuranceClaim, InsuranceError,
+    get_premium_rate as insurance_get_premium_rate, initialize as insurance_initialize,
+    set_coverage_limit as insurance_set_coverage_limit, submit_claim as insurance_submit_claim,
+    InsuranceAnalytics, InsuranceClaim, InsuranceError,
 };
 
 #[cfg(test)]
@@ -68,6 +69,8 @@ mod insurance_test;
 mod math_safety_test;
 #[cfg(test)]
 mod pause_test;
+#[cfg(any(test, feature = "spec"))]
+mod spec;
 #[cfg(test)]
 mod token_receiver_test;
 #[cfg(test)]
diff --git a/stellar-lend/contracts/lending/src/spec/accounting.rs b/stellar-lend/contracts/lending/src/spec/accounting.rs
index 27269e99..fd8b0263 100644
--- a/stellar-lend/contracts/lending/src/spec/accounting.rs
+++ b/stellar-lend/contracts/lending/src/spec/accounting.rs
@@ -41,21 +41,38 @@ pub enum AccountingError {
 
 impl AccountingState {
     pub fn new(ceiling: i128) -> Self {
-        Self { total_debt: 0, debt_ceiling: ceiling, user_principal: 0, user_interest: 0 }
+        Self {
+            total_debt: 0,
+            debt_ceiling: ceiling,
+            user_principal: 0,
+            user_interest: 0,
+        }
     }
 
     pub fn apply_borrow(&mut self, amount: i128) -> Result<(), AccountingError> {
-        if amount <= 0 { return Err(AccountingError::InvalidAmount); }
-        let new_total = self.total_debt.checked_add(amount).ok_or(AccountingError::Overflow)?;
-        if new_total > self.debt_ceiling { return Err(AccountingError::DebtCeilingReached); }
-        let new_user = self.user_principal.checked_add(amount).ok_or(AccountingError::Overflow)?;
+        if amount <= 0 {
+            return Err(AccountingError::InvalidAmount);
+        }
+        let new_total = self
+            .total_debt
+            .checked_add(amount)
+            .ok_or(AccountingError::Overflow)?;
+        if new_total > self.debt_ceiling {
+            return Err(AccountingError::DebtCeilingReached);
+        }
+        let new_user = self
+            .user_principal
+            .checked_add(amount)
+            .ok_or(AccountingError::Overflow)?;
         self.total_debt = new_total;
         self.user_principal = new_user;
         Ok(())
     }
 
     pub fn apply_repay(&mut self, amount: i128) -> Result<(), AccountingError> {
-        if amount <= 0 { return Err(AccountingError::InvalidAmount); }
+        if amount <= 0 {
+            return Err(AccountingError::InvalidAmount);
+        }
         let mut remaining = amount;
         if remaining >= self.user_interest {
             remaining -= self.user_interest;
@@ -65,9 +82,14 @@ impl AccountingState {
             remaining = 0;
         }
         if remaining > 0 {
-            if remaining > self.user_principal { return Err(AccountingError::RepayAmountTooHigh); }
+            if remaining > self.user_principal {
+                return Err(AccountingError::RepayAmountTooHigh);
+            }
             self.user_principal -= remaining;
-            self.total_debt = self.total_debt.checked_sub(remaining).ok_or(AccountingError::Overflow)?;
+            self.total_debt = self
+                .total_debt
+                .checked_sub(remaining)
+                .ok_or(AccountingError::Overflow)?;
         }
         Ok(())
     }
@@ -80,7 +102,11 @@ fn lemma_a01_borrow_increments_total_debt() {
         let mut state = AccountingState::new(i128::MAX);
         let before = state.total_debt;
         state.apply_borrow(amount).expect("A-01");
-        assert_eq!(state.total_debt, before + amount, "A-01 failed for amount={amount}");
+        assert_eq!(
+            state.total_debt,
+            before + amount,
+            "A-01 failed for amount={amount}"
+        );
     }
 }
 
@@ -103,7 +129,11 @@ fn lemma_a03_total_debt_stays_non_negative() {
     let mut state = AccountingState::new(i128::MAX);
     state.apply_borrow(100_000).unwrap();
     state.apply_repay(100_000).expect("A-03");
-    assert!(state.total_debt >= 0, "A-03: negative total_debt={}", state.total_debt);
+    assert!(
+        state.total_debt >= 0,
+        "A-03: negative total_debt={}",
+        state.total_debt
+    );
     assert_eq!(state.total_debt, 0, "A-03");
 }
 
@@ -113,7 +143,11 @@ fn lemma_a04_borrow_ceiling_enforced() {
     let ceiling = 1_000_000i128;
     let mut state = AccountingState::new(ceiling);
     state.apply_borrow(ceiling).expect("A-04");
-    assert_eq!(state.apply_borrow(1), Err(AccountingError::DebtCeilingReached), "A-04");
+    assert_eq!(
+        state.apply_borrow(1),
+        Err(AccountingError::DebtCeilingReached),
+        "A-04"
+    );
     assert_eq!(state.total_debt, ceiling, "A-04: ceiling breached");
 }
 
@@ -144,7 +178,11 @@ fn lemma_a06_partial_repay_leaves_correct_remainder() {
 fn lemma_a07_over_repay_is_rejected() {
     let mut state = AccountingState::new(i128::MAX);
     state.apply_borrow(50_000).unwrap();
-    assert_eq!(state.apply_repay(50_001), Err(AccountingError::RepayAmountTooHigh), "A-07");
+    assert_eq!(
+        state.apply_repay(50_001),
+        Err(AccountingError::RepayAmountTooHigh),
+        "A-07"
+    );
     assert_eq!(state.user_principal, 50_000, "A-07: state mutated");
     assert_eq!(state.total_debt, 50_000, "A-07: total_debt mutated");
 }
@@ -154,7 +192,11 @@ fn lemma_a07_over_repay_is_rejected() {
 fn lemma_a08_borrow_beyond_ceiling_is_rejected() {
     let mut state = AccountingState::new(500_000);
     state.apply_borrow(300_000).unwrap();
-    assert_eq!(state.apply_borrow(250_000), Err(AccountingError::DebtCeilingReached), "A-08");
+    assert_eq!(
+        state.apply_borrow(250_000),
+        Err(AccountingError::DebtCeilingReached),
+        "A-08"
+    );
     assert_eq!(state.total_debt, 300_000, "A-08: state mutated");
 }
 
diff --git a/stellar-lend/contracts/lending/src/spec/collateral.rs b/stellar-lend/contracts/lending/src/spec/collateral.rs
index 29b4949d..1d53190d 100644
--- a/stellar-lend/contracts/lending/src/spec/collateral.rs
+++ b/stellar-lend/contracts/lending/src/spec/collateral.rs
@@ -97,7 +97,7 @@ fn lemma_c01_exact_150pct_is_accepted() {
 #[test]
 fn lemma_c02_below_150pct_is_rejected() {
     let test_cases: &[(i128, i128)] = &[
-        (1, 2),    // 50% — clearly insufficient
+        (1, 2), // 50% — clearly insufficient
         (100, 200),
         (14_999, 10_000), // 149.99% — just below the threshold
     ];
@@ -122,8 +122,8 @@ fn lemma_c02_below_150pct_is_rejected() {
 #[test]
 fn lemma_c03_above_150pct_is_accepted() {
     let test_cases: &[(i128, i128)] = &[
-        (15_001, 10_000),   // 150.01%
-        (20_000, 10_000),   // 200%
+        (15_001, 10_000),       // 150.01%
+        (20_000, 10_000),       // 200%
         (3_000_000, 1_000_000), // 300%
         (i128::MAX / 2, 1),
     ];
diff --git a/stellar-lend/contracts/lending/src/spec/deposit_spec.rs b/stellar-lend/contracts/lending/src/spec/deposit_spec.rs
index 69754b7c..cc7d0693 100644
--- a/stellar-lend/contracts/lending/src/spec/deposit_spec.rs
+++ b/stellar-lend/contracts/lending/src/spec/deposit_spec.rs
@@ -29,18 +29,29 @@ pub enum DepositError {
 
 impl DepositState {
     pub fn new(cap: i128, min: i128) -> Self {
-        Self { user_balance: 0, total_deposits: 0, deposit_cap: cap, min_deposit: min }
+        Self {
+            user_balance: 0,
+            total_deposits: 0,
+            deposit_cap: cap,
+            min_deposit: min,
+        }
     }
 
     pub fn apply_deposit(&mut self, amount: i128) -> Result<(), DepositError> {
         if amount <= 0 || amount < self.min_deposit {
             return Err(DepositError::InvalidAmount);
         }
-        let new_total = self.total_deposits.checked_add(amount).ok_or(DepositError::Overflow)?;
+        let new_total = self
+            .total_deposits
+            .checked_add(amount)
+            .ok_or(DepositError::Overflow)?;
         if new_total > self.deposit_cap {
             return Err(DepositError::ExceedsDepositCap);
         }
-        let new_user = self.user_balance.checked_add(amount).ok_or(DepositError::Overflow)?;
+        let new_user = self
+            .user_balance
+            .checked_add(amount)
+            .ok_or(DepositError::Overflow)?;
         self.total_deposits = new_total;
         self.user_balance = new_user;
         Ok(())
@@ -58,7 +69,11 @@ fn lemma_d01_zero_amount_rejected() {
 #[test]
 fn lemma_d02_below_minimum_rejected() {
     let mut s = DepositState::new(i128::MAX, 1_000);
-    assert_eq!(s.apply_deposit(999), Err(DepositError::InvalidAmount), "D-02");
+    assert_eq!(
+        s.apply_deposit(999),
+        Err(DepositError::InvalidAmount),
+        "D-02"
+    );
 }
 
 /// **D-03**: Deposit cap is enforced.
@@ -67,7 +82,11 @@ fn lemma_d03_deposit_cap_enforced() {
     let cap = 1_000_000i128;
     let mut s = DepositState::new(cap, 0);
     s.apply_deposit(cap).unwrap();
-    assert_eq!(s.apply_deposit(1), Err(DepositError::ExceedsDepositCap), "D-03");
+    assert_eq!(
+        s.apply_deposit(1),
+        Err(DepositError::ExceedsDepositCap),
+        "D-03"
+    );
 }
 
 /// **D-04**: User balance increases by exactly the deposit amount.
@@ -104,5 +123,8 @@ fn lemma_d06_sequential_deposits_accumulate() {
 fn lemma_d07_no_overflow_safe_domain() {
     let safe = i128::MAX / 4;
     let mut s = DepositState::new(i128::MAX, 0);
-    assert!(s.apply_deposit(safe).is_ok(), "D-07: overflow on safe deposit");
+    assert!(
+        s.apply_deposit(safe).is_ok(),
+        "D-07: overflow on safe deposit"
+    );
 }
diff --git a/stellar-lend/contracts/lending/src/spec/health_factor.rs b/stellar-lend/contracts/lending/src/spec/health_factor.rs
index 96eda0df..6bba3f1b 100644
--- a/stellar-lend/contracts/lending/src/spec/health_factor.rs
+++ b/stellar-lend/contracts/lending/src/spec/health_factor.rs
@@ -48,7 +48,9 @@ pub fn reference_health_factor(
         .checked_mul(liq_threshold_bps)?
         .checked_div(BPS_DIVISOR)?;
     // HF = weighted * HF_SCALE / debt_value
-    let hf = weighted.checked_mul(HEALTH_FACTOR_SCALE)?.checked_div(debt_value)?;
+    let hf = weighted
+        .checked_mul(HEALTH_FACTOR_SCALE)?
+        .checked_div(debt_value)?;
     Some(hf)
 }
 
@@ -75,31 +77,24 @@ fn lemma_h03_hf_scale_liquidation_boundary() {
     let collateral = debt * BPS_DIVISOR / DEFAULT_LIQ_THRESHOLD_BPS; // = 1_250_000
     let hf = reference_health_factor(collateral, debt, true, DEFAULT_LIQ_THRESHOLD_BPS, true)
         .expect("H-03: exact threshold");
-    assert_eq!(hf, HEALTH_FACTOR_SCALE, "H-03: exact threshold HF should equal HF_SCALE");
+    assert_eq!(
+        hf, HEALTH_FACTOR_SCALE,
+        "H-03: exact threshold HF should equal HF_SCALE"
+    );
 
     // Use 2x collateral → HF should be 2 * HF_SCALE (clearly healthy)
-    let hf_above = reference_health_factor(
-        collateral * 2,
-        debt,
-        true,
-        DEFAULT_LIQ_THRESHOLD_BPS,
-        true,
-    )
-    .expect("H-03 above");
+    let hf_above =
+        reference_health_factor(collateral * 2, debt, true, DEFAULT_LIQ_THRESHOLD_BPS, true)
+            .expect("H-03 above");
     assert!(
         hf_above > HEALTH_FACTOR_SCALE,
         "H-03: 2x collateral should be healthy, got hf={hf_above}"
     );
 
     // Half the exact-threshold collateral → HF should be HF_SCALE/2 (liquidatable)
-    let hf_below = reference_health_factor(
-        collateral / 2,
-        debt,
-        true,
-        DEFAULT_LIQ_THRESHOLD_BPS,
-        true,
-    )
-    .expect("H-03 below");
+    let hf_below =
+        reference_health_factor(collateral / 2, debt, true, DEFAULT_LIQ_THRESHOLD_BPS, true)
+            .expect("H-03 below");
     assert!(
         hf_below < HEALTH_FACTOR_SCALE,
         "H-03: half collateral should be liquidatable, got hf={hf_below}"
@@ -113,8 +108,8 @@ fn lemma_h04_monotone_increasing_in_collateral() {
     let collateral_values: &[i128] = &[0, 100_000, 500_000, 800_000, 1_000_000, 5_000_000];
     let mut prev = 0i128;
     for &cv in collateral_values {
-        let hf = reference_health_factor(cv, debt, true, DEFAULT_LIQ_THRESHOLD_BPS, true)
-            .unwrap_or(0);
+        let hf =
+            reference_health_factor(cv, debt, true, DEFAULT_LIQ_THRESHOLD_BPS, true).unwrap_or(0);
         assert!(
             hf >= prev,
             "H-04: HF not monotone at cv={cv}: hf={hf} < prev={prev}"
@@ -161,7 +156,10 @@ fn lemma_h07_exact_threshold_yields_hf_scale() {
     let collateral = debt * BPS_DIVISOR / DEFAULT_LIQ_THRESHOLD_BPS;
     let hf = reference_health_factor(collateral, debt, true, DEFAULT_LIQ_THRESHOLD_BPS, true)
         .expect("H-07");
-    assert_eq!(hf, HEALTH_FACTOR_SCALE, "H-07: boundary HF should be exactly HF_SCALE");
+    assert_eq!(
+        hf, HEALTH_FACTOR_SCALE,
+        "H-07: boundary HF should be exactly HF_SCALE"
+    );
 }
 
 #[cfg(kani)]
@@ -182,7 +180,10 @@ pub fn kani_health_factor_properties() {
     );
 
     if debt_value == 0 {
-        kani::assert(hf == Some(HEALTH_FACTOR_NO_DEBT), "H-01: zero debt sentinel");
+        kani::assert(
+            hf == Some(HEALTH_FACTOR_NO_DEBT),
+            "H-01: zero debt sentinel",
+        );
     }
     if let Some(h) = hf {
         kani::assert(h >= 0, "HF must be non-negative");
diff --git a/stellar-lend/contracts/lending/src/spec/interest.rs b/stellar-lend/contracts/lending/src/spec/interest.rs
index d14acef9..1e7ffd1a 100644
--- a/stellar-lend/contracts/lending/src/spec/interest.rs
+++ b/stellar-lend/contracts/lending/src/spec/interest.rs
@@ -79,11 +79,7 @@ pub fn reference_interest(principal: i128, elapsed_secs: i128) -> Option<i128> {
 fn lemma_i01_zero_principal_yields_zero() {
     for elapsed in [0i128, 1, 60, 3600, SECONDS_PER_YEAR, i128::MAX / 2] {
         let result = reference_interest(0, elapsed);
-        assert_eq!(
-            result,
-            Some(0),
-            "I-01 failed for elapsed={elapsed}"
-        );
+        assert_eq!(result, Some(0), "I-01 failed for elapsed={elapsed}");
     }
 }
 
@@ -92,11 +88,7 @@ fn lemma_i01_zero_principal_yields_zero() {
 fn lemma_i02_zero_elapsed_yields_zero() {
     for principal in [0i128, 1, 1_000, 1_000_000, MAX_SAFE_PRINCIPAL] {
         let result = reference_interest(principal, 0);
-        assert_eq!(
-            result,
-            Some(0),
-            "I-02 failed for principal={principal}"
-        );
+        assert_eq!(result, Some(0), "I-02 failed for principal={principal}");
     }
 }
 
@@ -175,7 +167,7 @@ fn lemma_i06_no_overflow_on_max_safe_principal() {
     );
     let interest = result.unwrap();
     let expected = principal / 20; // 5% of principal
-    // Allow ±1 for integer division rounding
+                                   // Allow ±1 for integer division rounding
     assert!(
         (interest - expected).abs() <= 1,
         "I-06: interest={interest} deviates from expected={expected}"
@@ -198,8 +190,7 @@ fn lemma_i07_annual_interest_bounded_by_5pct() {
         i128::MAX / INTEREST_RATE_PER_YEAR / SECONDS_PER_YEAR, // max safe for 1 year
     ];
     for &p in test_principals {
-        let interest = reference_interest(p, SECONDS_PER_YEAR)
-            .expect("I-07: overflow");
+        let interest = reference_interest(p, SECONDS_PER_YEAR).expect("I-07: overflow");
         // 5% of principal, allow +1 for rounding
         let max_allowed = p / 20 + 1;
         assert!(
@@ -235,7 +226,9 @@ fn lemma_i08_stability_fee_is_non_negative_increment() {
         stability_fee >= 0,
         "I-08: stability fee is negative: {stability_fee}"
     );
-    let total = base.checked_add(stability_fee).expect("I-08: total overflow");
+    let total = base
+        .checked_add(stability_fee)
+        .expect("I-08: total overflow");
     assert!(
         total >= base,
         "I-08: total interest with stability fee < base interest"
diff --git a/stellar-lend/contracts/lending/src/spec/liquidation.rs b/stellar-lend/contracts/lending/src/spec/liquidation.rs
index ec126075..0cd90418 100644
--- a/stellar-lend/contracts/lending/src/spec/liquidation.rs
+++ b/stellar-lend/contracts/lending/src/spec/liquidation.rs
@@ -32,10 +32,18 @@ fn local_health_factor(
     liq_threshold_bps: i128,
     oracle_present: bool,
 ) -> Option<i128> {
-    if debt_value <= 0 { return Some(i128::MAX); } // no debt = max healthy
-    if !oracle_present { return None; }
-    let weighted = collateral_value.checked_mul(liq_threshold_bps)?.checked_div(BPS_DIVISOR)?;
-    let hf = weighted.checked_mul(HEALTH_FACTOR_SCALE)?.checked_div(debt_value)?;
+    if debt_value <= 0 {
+        return Some(i128::MAX);
+    } // no debt = max healthy
+    if !oracle_present {
+        return None;
+    }
+    let weighted = collateral_value
+        .checked_mul(liq_threshold_bps)?
+        .checked_div(BPS_DIVISOR)?;
+    let hf = weighted
+        .checked_mul(HEALTH_FACTOR_SCALE)?
+        .checked_div(debt_value)?;
     Some(hf)
 }
 
@@ -58,7 +66,7 @@ pub fn reference_max_liquidatable(
         oracle_present,
     );
     match hf {
-        None | Some(0) => 0, // oracle absent or zero HF
+        None | Some(0) => 0,                      // oracle absent or zero HF
         Some(h) if h >= HEALTH_FACTOR_SCALE => 0, // healthy
         Some(_) => {
             // Liquidatable: apply close factor
@@ -75,8 +83,12 @@ pub fn reference_max_liquidatable(
 fn lemma_l01_healthy_position_returns_zero() {
     // Collateral far above threshold
     let result = reference_max_liquidatable(
-        100_000, 2_000_000, 1_000_000,
-        DEFAULT_CLOSE_FACTOR_BPS, DEFAULT_LIQ_THRESHOLD_BPS, true,
+        100_000,
+        2_000_000,
+        1_000_000,
+        DEFAULT_CLOSE_FACTOR_BPS,
+        DEFAULT_LIQ_THRESHOLD_BPS,
+        true,
     );
     assert_eq!(result, 0, "L-01: healthy position should return 0");
 }
@@ -84,7 +96,14 @@ fn lemma_l01_healthy_position_returns_zero() {
 /// **L-02**: No debt → 0.
 #[test]
 fn lemma_l02_no_debt_returns_zero() {
-    let result = reference_max_liquidatable(0, 0, 0, DEFAULT_CLOSE_FACTOR_BPS, DEFAULT_LIQ_THRESHOLD_BPS, true);
+    let result = reference_max_liquidatable(
+        0,
+        0,
+        0,
+        DEFAULT_CLOSE_FACTOR_BPS,
+        DEFAULT_LIQ_THRESHOLD_BPS,
+        true,
+    );
     assert_eq!(result, 0, "L-02");
 }
 
@@ -92,8 +111,12 @@ fn lemma_l02_no_debt_returns_zero() {
 #[test]
 fn lemma_l03_no_oracle_returns_zero() {
     let result = reference_max_liquidatable(
-        100_000, 50_000, 100_000,
-        DEFAULT_CLOSE_FACTOR_BPS, DEFAULT_LIQ_THRESHOLD_BPS, false,
+        100_000,
+        50_000,
+        100_000,
+        DEFAULT_CLOSE_FACTOR_BPS,
+        DEFAULT_LIQ_THRESHOLD_BPS,
+        false,
     );
     assert_eq!(result, 0, "L-03: no oracle should return 0");
 }
@@ -104,10 +127,17 @@ fn lemma_l04_liquidatable_does_not_exceed_total_debt() {
     // Severely undercollateralised position
     let total_debt = 1_000_000i128;
     let result = reference_max_liquidatable(
-        total_debt, 100_000, 1_000_000,
-        DEFAULT_CLOSE_FACTOR_BPS, DEFAULT_LIQ_THRESHOLD_BPS, true,
+        total_debt,
+        100_000,
+        1_000_000,
+        DEFAULT_CLOSE_FACTOR_BPS,
+        DEFAULT_LIQ_THRESHOLD_BPS,
+        true,
+    );
+    assert!(
+        result <= total_debt,
+        "L-04: liquidatable={result} > total_debt={total_debt}"
     );
-    assert!(result <= total_debt, "L-04: liquidatable={result} > total_debt={total_debt}");
 }
 
 /// **L-05**: Liquidatable amount equals total_debt * close_factor / 10_000.
@@ -123,11 +153,18 @@ fn lemma_l05_formula_correctness() {
     let cv = 600_000i128;
     let dv = total_debt;
     let result = reference_max_liquidatable(
-        total_debt, cv, dv,
-        DEFAULT_CLOSE_FACTOR_BPS, DEFAULT_LIQ_THRESHOLD_BPS, true,
+        total_debt,
+        cv,
+        dv,
+        DEFAULT_CLOSE_FACTOR_BPS,
+        DEFAULT_LIQ_THRESHOLD_BPS,
+        true,
     );
     let expected = total_debt * DEFAULT_CLOSE_FACTOR_BPS / BPS_DIVISOR;
-    assert_eq!(result, expected, "L-05: formula mismatch, got={result}, expected={expected}");
+    assert_eq!(
+        result, expected,
+        "L-05: formula mismatch, got={result}, expected={expected}"
+    );
 }
 
 /// **L-06**: No overflow for i128::MAX / 2 total debt.
@@ -135,11 +172,16 @@ fn lemma_l05_formula_correctness() {
 fn lemma_l06_no_overflow_on_large_debt() {
     let total_debt = i128::MAX / 2;
     let result = reference_max_liquidatable(
-        total_debt, 0, total_debt,
-        DEFAULT_CLOSE_FACTOR_BPS, DEFAULT_LIQ_THRESHOLD_BPS, true,
+        total_debt,
+        0,
+        total_debt,
+        DEFAULT_CLOSE_FACTOR_BPS,
+        DEFAULT_LIQ_THRESHOLD_BPS,
+        true,
     );
     // Should not panic; result may be 0 if intermediate overflow triggers the unwrap_or path
-    let expected = (total_debt as i128).checked_mul(DEFAULT_CLOSE_FACTOR_BPS)
+    let expected = (total_debt as i128)
+        .checked_mul(DEFAULT_CLOSE_FACTOR_BPS)
         .map(|v| v / BPS_DIVISOR)
         .unwrap_or(0);
     assert_eq!(result, expected, "L-06: overflow path mismatch");
diff --git a/stellar-lend/contracts/lending/src/spec/mod.rs b/stellar-lend/contracts/lending/src/spec/mod.rs
index f46ddb51..69984c12 100644
--- a/stellar-lend/contracts/lending/src/spec/mod.rs
+++ b/stellar-lend/contracts/lending/src/spec/mod.rs
@@ -40,18 +40,20 @@
 //! * The oracle contract is trusted; its price return is assumed to be ≥ 0.
 
 #[cfg(any(test, feature = "spec"))]
-pub mod interest;
+pub mod accounting;
 #[cfg(any(test, feature = "spec"))]
 pub mod collateral;
 #[cfg(any(test, feature = "spec"))]
-pub mod accounting;
+pub mod deposit_spec;
 #[cfg(any(test, feature = "spec"))]
 pub mod health_factor;
 #[cfg(any(test, feature = "spec"))]
+pub mod interest;
+#[cfg(any(test, feature = "spec"))]
 pub mod liquidation;
 #[cfg(any(test, feature = "spec"))]
-pub mod rewards;
+pub mod protocol_invariants;
 #[cfg(any(test, feature = "spec"))]
-pub mod deposit_spec;
+pub mod rewards;
 #[cfg(any(test, feature = "spec"))]
 pub mod withdraw_spec;
diff --git a/stellar-lend/contracts/lending/src/spec/protocol_invariants.rs b/stellar-lend/contracts/lending/src/spec/protocol_invariants.rs
new file mode 100644
index 00000000..574b74e9
--- /dev/null
+++ b/stellar-lend/contracts/lending/src/spec/protocol_invariants.rs
@@ -0,0 +1,480 @@
+//! Protocol-level formal specification for StellarLend lending invariants.
+//!
+//! The models in this file are intentionally pure Rust. They do not touch
+//! Soroban storage, which lets CI run them as deterministic specification
+//! checks and lets Kani symbolically explore bounded state transitions.
+//!
+//! Invariants covered:
+//! - P-01: total_deposits = total_debt + reserves
+//! - P-02: borrow and repay preserve double-entry accounting
+//! - P-03: health factor agrees with liquidation boundary during operations
+//! - P-04: interest index accrual is monotonic in non-decreasing time
+
+pub const BPS_SCALE: i128 = 10_000;
+pub const HEALTH_FACTOR_SCALE: i128 = 10_000;
+pub const HEALTH_FACTOR_NO_DEBT: i128 = 100_000_000;
+pub const DEFAULT_LIQ_THRESHOLD_BPS: i128 = 8_000;
+pub const SECONDS_PER_YEAR: u64 = 31_536_000;
+
+#[derive(Clone, Copy, Debug, Eq, PartialEq)]
+pub enum ProtocolSpecError {
+    InvalidAmount,
+    InvalidState,
+    InsufficientLiquidity,
+    RepayAmountTooHigh,
+    Overflow,
+    TimestampRewind,
+}
+
+#[derive(Clone, Copy, Debug, Eq, PartialEq)]
+pub struct ProtocolAccountingState {
+    pub total_deposits: i128,
+    pub total_debt: i128,
+    pub reserves: i128,
+}
+
+impl ProtocolAccountingState {
+    pub fn new(
+        total_deposits: i128,
+        total_debt: i128,
+        reserves: i128,
+    ) -> Result<Self, ProtocolSpecError> {
+        let state = Self {
+            total_deposits,
+            total_debt,
+            reserves,
+        };
+        state.validate()?;
+        Ok(state)
+    }
+
+    pub fn empty() -> Self {
+        Self {
+            total_deposits: 0,
+            total_debt: 0,
+            reserves: 0,
+        }
+    }
+
+    pub fn validate(&self) -> Result<(), ProtocolSpecError> {
+        if self.total_deposits < 0 || self.total_debt < 0 || self.reserves < 0 {
+            return Err(ProtocolSpecError::InvalidState);
+        }
+
+        let liabilities = self
+            .total_debt
+            .checked_add(self.reserves)
+            .ok_or(ProtocolSpecError::Overflow)?;
+
+        if self.total_deposits != liabilities {
+            return Err(ProtocolSpecError::InvalidState);
+        }
+
+        Ok(())
+    }
+
+    pub fn apply_deposit(&mut self, amount: i128) -> Result<(), ProtocolSpecError> {
+        if amount <= 0 {
+            return Err(ProtocolSpecError::InvalidAmount);
+        }
+
+        self.total_deposits = self
+            .total_deposits
+            .checked_add(amount)
+            .ok_or(ProtocolSpecError::Overflow)?;
+        self.reserves = self
+            .reserves
+            .checked_add(amount)
+            .ok_or(ProtocolSpecError::Overflow)?;
+        self.validate()
+    }
+
+    pub fn apply_borrow(&mut self, amount: i128) -> Result<(), ProtocolSpecError> {
+        if amount <= 0 {
+            return Err(ProtocolSpecError::InvalidAmount);
+        }
+        if amount > self.reserves {
+            return Err(ProtocolSpecError::InsufficientLiquidity);
+        }
+
+        self.reserves = self
+            .reserves
+            .checked_sub(amount)
+            .ok_or(ProtocolSpecError::Overflow)?;
+        self.total_debt = self
+            .total_debt
+            .checked_add(amount)
+            .ok_or(ProtocolSpecError::Overflow)?;
+        self.validate()
+    }
+
+    pub fn apply_repay(&mut self, amount: i128) -> Result<(), ProtocolSpecError> {
+        if amount <= 0 {
+            return Err(ProtocolSpecError::InvalidAmount);
+        }
+        if amount > self.total_debt {
+            return Err(ProtocolSpecError::RepayAmountTooHigh);
+        }
+
+        self.total_debt = self
+            .total_debt
+            .checked_sub(amount)
+            .ok_or(ProtocolSpecError::Overflow)?;
+        self.reserves = self
+            .reserves
+            .checked_add(amount)
+            .ok_or(ProtocolSpecError::Overflow)?;
+        self.validate()
+    }
+}
+
+#[derive(Clone, Copy, Debug, Eq, PartialEq)]
+pub struct HealthFactorState {
+    pub collateral_value: i128,
+    pub debt_value: i128,
+    pub liquidation_threshold_bps: i128,
+}
+
+impl HealthFactorState {
+    pub fn new(
+        collateral_value: i128,
+        debt_value: i128,
+        liquidation_threshold_bps: i128,
+    ) -> Result<Self, ProtocolSpecError> {
+        let state = Self {
+            collateral_value,
+            debt_value,
+            liquidation_threshold_bps,
+        };
+        state.validate_inputs()?;
+        Ok(state)
+    }
+
+    fn validate_inputs(&self) -> Result<(), ProtocolSpecError> {
+        if self.collateral_value < 0 || self.debt_value < 0 {
+            return Err(ProtocolSpecError::InvalidState);
+        }
+        if self.liquidation_threshold_bps <= 0 || self.liquidation_threshold_bps > BPS_SCALE {
+            return Err(ProtocolSpecError::InvalidAmount);
+        }
+        Ok(())
+    }
+
+    pub fn health_factor(&self) -> Result<i128, ProtocolSpecError> {
+        self.validate_inputs()?;
+        if self.debt_value == 0 {
+            return Ok(HEALTH_FACTOR_NO_DEBT);
+        }
+
+        let weighted_collateral = self
+            .collateral_value
+            .checked_mul(self.liquidation_threshold_bps)
+            .ok_or(ProtocolSpecError::Overflow)?
+            .checked_div(BPS_SCALE)
+            .ok_or(ProtocolSpecError::Overflow)?;
+
+        weighted_collateral
+            .checked_mul(HEALTH_FACTOR_SCALE)
+            .ok_or(ProtocolSpecError::Overflow)?
+            .checked_div(self.debt_value)
+            .ok_or(ProtocolSpecError::Overflow)
+    }
+
+    pub fn is_liquidatable(&self) -> Result<bool, ProtocolSpecError> {
+        Ok(self.debt_value > 0 && self.health_factor()? < HEALTH_FACTOR_SCALE)
+    }
+
+    pub fn apply_collateral_delta(&mut self, delta: i128) -> Result<(), ProtocolSpecError> {
+        self.collateral_value = self
+            .collateral_value
+            .checked_add(delta)
+            .ok_or(ProtocolSpecError::Overflow)?;
+        self.validate_inputs()
+    }
+
+    pub fn apply_debt_delta(&mut self, delta: i128) -> Result<(), ProtocolSpecError> {
+        self.debt_value = self
+            .debt_value
+            .checked_add(delta)
+            .ok_or(ProtocolSpecError::Overflow)?;
+        self.validate_inputs()
+    }
+}
+
+#[derive(Clone, Copy, Debug, Eq, PartialEq)]
+pub struct InterestIndexState {
+    pub index: i128,
+    pub rate_bps: i128,
+    pub last_timestamp: u64,
+}
+
+impl InterestIndexState {
+    pub fn new(
+        index: i128,
+        rate_bps: i128,
+        last_timestamp: u64,
+    ) -> Result<Self, ProtocolSpecError> {
+        let state = Self {
+            index,
+            rate_bps,
+            last_timestamp,
+        };
+        state.validate()?;
+        Ok(state)
+    }
+
+    fn validate(&self) -> Result<(), ProtocolSpecError> {
+        if self.index <= 0 || self.rate_bps < 0 {
+            return Err(ProtocolSpecError::InvalidState);
+        }
+        Ok(())
+    }
+
+    pub fn accrue_to(&mut self, now: u64) -> Result<i128, ProtocolSpecError> {
+        self.validate()?;
+        if now < self.last_timestamp {
+            return Err(ProtocolSpecError::TimestampRewind);
+        }
+
+        let elapsed = now - self.last_timestamp;
+        if elapsed == 0 || self.rate_bps == 0 {
+            self.last_timestamp = now;
+            return Ok(self.index);
+        }
+
+        let increment = self
+            .index
+            .checked_mul(self.rate_bps)
+            .ok_or(ProtocolSpecError::Overflow)?
+            .checked_mul(elapsed as i128)
+            .ok_or(ProtocolSpecError::Overflow)?
+            .checked_div(BPS_SCALE)
+            .ok_or(ProtocolSpecError::Overflow)?
+            .checked_div(SECONDS_PER_YEAR as i128)
+            .ok_or(ProtocolSpecError::Overflow)?;
+
+        self.index = self
+            .index
+            .checked_add(increment)
+            .ok_or(ProtocolSpecError::Overflow)?;
+        self.last_timestamp = now;
+        Ok(self.index)
+    }
+}
+
+#[test]
+fn lemma_p01_accounting_identity_holds_after_deposits() {
+    let mut state = ProtocolAccountingState::empty();
+
+    for amount in [1, 10_000, 500_000, 1_000_000_000] {
+        state
+            .apply_deposit(amount)
+            .expect("deposit should preserve accounting");
+        assert_eq!(state.total_deposits, state.total_debt + state.reserves);
+    }
+}
+
+#[test]
+fn lemma_p02_borrow_preserves_deposit_debt_reserve_identity() {
+    let mut state = ProtocolAccountingState::empty();
+    state.apply_deposit(1_000_000).unwrap();
+
+    for amount in [1, 20_000, 250_000, 500_000] {
+        state
+            .apply_borrow(amount)
+            .expect("borrow should preserve accounting");
+        assert_eq!(state.total_deposits, state.total_debt + state.reserves);
+    }
+}
+
+#[test]
+fn lemma_p03_repay_preserves_deposit_debt_reserve_identity() {
+    let mut state = ProtocolAccountingState::empty();
+    state.apply_deposit(1_000_000).unwrap();
+    state.apply_borrow(900_000).unwrap();
+
+    for amount in [1, 20_000, 250_000, 500_000] {
+        state
+            .apply_repay(amount)
+            .expect("repay should preserve accounting");
+        assert_eq!(state.total_deposits, state.total_debt + state.reserves);
+    }
+}
+
+#[test]
+fn lemma_p04_over_borrow_is_rejected_without_mutation() {
+    let mut state = ProtocolAccountingState::empty();
+    state.apply_deposit(50_000).unwrap();
+    let before = state;
+
+    assert_eq!(
+        state.apply_borrow(50_001),
+        Err(ProtocolSpecError::InsufficientLiquidity)
+    );
+    assert_eq!(state, before);
+}
+
+#[test]
+fn lemma_p05_over_repay_is_rejected_without_mutation() {
+    let mut state = ProtocolAccountingState::empty();
+    state.apply_deposit(100_000).unwrap();
+    state.apply_borrow(75_000).unwrap();
+    let before = state;
+
+    assert_eq!(
+        state.apply_repay(75_001),
+        Err(ProtocolSpecError::RepayAmountTooHigh)
+    );
+    assert_eq!(state, before);
+}
+
+#[test]
+fn lemma_h01_health_factor_matches_exact_liquidation_boundary() {
+    let debt = 1_000_000;
+    let collateral = debt * BPS_SCALE / DEFAULT_LIQ_THRESHOLD_BPS;
+    let state = HealthFactorState::new(collateral, debt, DEFAULT_LIQ_THRESHOLD_BPS).unwrap();
+
+    assert_eq!(state.health_factor().unwrap(), HEALTH_FACTOR_SCALE);
+    assert!(!state.is_liquidatable().unwrap());
+}
+
+#[test]
+fn lemma_h02_collateral_increase_never_decreases_health_factor() {
+    let mut state =
+        HealthFactorState::new(1_250_000, 1_000_000, DEFAULT_LIQ_THRESHOLD_BPS).unwrap();
+    let before = state.health_factor().unwrap();
+    state.apply_collateral_delta(500_000).unwrap();
+    let after = state.health_factor().unwrap();
+
+    assert!(
+        after >= before,
+        "health factor decreased after collateral increase"
+    );
+}
+
+#[test]
+fn lemma_h03_borrow_increase_never_increases_health_factor() {
+    let mut state = HealthFactorState::new(2_000_000, 500_000, DEFAULT_LIQ_THRESHOLD_BPS).unwrap();
+    let before = state.health_factor().unwrap();
+    state.apply_debt_delta(500_000).unwrap();
+    let after = state.health_factor().unwrap();
+
+    assert!(
+        after <= before,
+        "health factor increased after debt increase"
+    );
+}
+
+#[test]
+fn lemma_h04_repay_never_decreases_health_factor() {
+    let mut state =
+        HealthFactorState::new(2_000_000, 1_000_000, DEFAULT_LIQ_THRESHOLD_BPS).unwrap();
+    let before = state.health_factor().unwrap();
+    state.apply_debt_delta(-500_000).unwrap();
+    let after = state.health_factor().unwrap();
+
+    assert!(
+        after >= before,
+        "health factor decreased after debt reduction"
+    );
+}
+
+#[test]
+fn lemma_h05_liquidation_flag_tracks_health_factor() {
+    let healthy = HealthFactorState::new(2_000_000, 1_000_000, DEFAULT_LIQ_THRESHOLD_BPS).unwrap();
+    let unhealthy =
+        HealthFactorState::new(1_000_000, 1_000_000, DEFAULT_LIQ_THRESHOLD_BPS).unwrap();
+
+    assert!(!healthy.is_liquidatable().unwrap());
+    assert!(unhealthy.is_liquidatable().unwrap());
+}
+
+#[test]
+fn lemma_i01_interest_index_is_monotonic() {
+    let mut index = InterestIndexState::new(BPS_SCALE, 500, 1_700_000_000).unwrap();
+    let before = index.index;
+    let after = index.accrue_to(1_700_000_000 + SECONDS_PER_YEAR).unwrap();
+
+    assert!(after >= before);
+}
+
+#[test]
+fn lemma_i02_zero_elapsed_time_is_noop() {
+    let mut index = InterestIndexState::new(BPS_SCALE, 500, 1_700_000_000).unwrap();
+    let after = index.accrue_to(1_700_000_000).unwrap();
+
+    assert_eq!(after, BPS_SCALE);
+}
+
+#[test]
+fn lemma_i03_timestamp_rewind_is_rejected() {
+    let mut index = InterestIndexState::new(BPS_SCALE, 500, 1_700_000_000).unwrap();
+
+    assert_eq!(
+        index.accrue_to(1_699_999_999),
+        Err(ProtocolSpecError::TimestampRewind)
+    );
+}
+
+#[cfg(kani)]
+#[kani::proof]
+pub fn kani_protocol_accounting_preserves_identity() {
+    let deposit_amount: i128 = kani::any();
+    let borrow_amount: i128 = kani::any();
+    let repay_amount: i128 = kani::any();
+
+    kani::assume(deposit_amount > 0 && deposit_amount <= 1_000_000_000);
+    kani::assume(borrow_amount > 0 && borrow_amount <= deposit_amount);
+    kani::assume(repay_amount > 0 && repay_amount <= borrow_amount);
+
+    let mut state = ProtocolAccountingState::empty();
+    state.apply_deposit(deposit_amount).unwrap();
+    state.apply_borrow(borrow_amount).unwrap();
+    state.apply_repay(repay_amount).unwrap();
+
+    kani::assert(
+        state.total_deposits == state.total_debt + state.reserves,
+        "P-01 total deposits equal total debt plus reserves",
+    );
+}
+
+#[cfg(kani)]
+#[kani::proof]
+pub fn kani_health_factor_consistency() {
+    let collateral_value: i128 = kani::any();
+    let debt_value: i128 = kani::any();
+
+    kani::assume(collateral_value >= 0 && collateral_value <= 1_000_000_000_000);
+    kani::assume(debt_value >= 0 && debt_value <= 1_000_000_000_000);
+
+    let state =
+        HealthFactorState::new(collateral_value, debt_value, DEFAULT_LIQ_THRESHOLD_BPS).unwrap();
+    let hf = state.health_factor().unwrap();
+
+    if debt_value == 0 {
+        kani::assert(hf == HEALTH_FACTOR_NO_DEBT, "zero debt sentinel");
+    } else {
+        kani::assert(
+            state.is_liquidatable().unwrap() == (hf < HEALTH_FACTOR_SCALE),
+            "liquidation flag tracks health factor",
+        );
+    }
+}
+
+#[cfg(kani)]
+#[kani::proof]
+pub fn kani_interest_index_monotonic() {
+    let start: u64 = kani::any();
+    let elapsed: u64 = kani::any();
+    let rate_bps: i128 = kani::any();
+
+    kani::assume(start <= u64::MAX - 31_536_000);
+    kani::assume(elapsed <= 31_536_000);
+    kani::assume(rate_bps >= 0 && rate_bps <= BPS_SCALE);
+
+    let mut index = InterestIndexState::new(BPS_SCALE, rate_bps, start).unwrap();
+    let before = index.index;
+    let after = index.accrue_to(start + elapsed).unwrap();
+
+    kani::assert(after >= before, "interest index must not decrease");
+}
diff --git a/stellar-lend/contracts/lending/src/spec/rewards.rs b/stellar-lend/contracts/lending/src/spec/rewards.rs
index 52c83119..710f0d94 100644
--- a/stellar-lend/contracts/lending/src/spec/rewards.rs
+++ b/stellar-lend/contracts/lending/src/spec/rewards.rs
@@ -47,7 +47,9 @@ impl RewardsState {
 
     /// Update global index to `now`.
     pub fn update_global(&mut self, now: i128) {
-        if now == self.last_update { return; }
+        if now == self.last_update {
+            return;
+        }
         if self.total_liquidity == 0 {
             self.last_update = now;
             return;
@@ -92,7 +94,10 @@ fn lemma_r02_zero_liquidity_index_unchanged() {
     let mut state = RewardsState::new(1_000, 0);
     let initial_index = state.global_index;
     state.update_global(3600);
-    assert_eq!(state.global_index, initial_index, "R-02: index changed with zero liquidity");
+    assert_eq!(
+        state.global_index, initial_index,
+        "R-02: index changed with zero liquidity"
+    );
 }
 
 /// **R-03**: Zero emission rate keeps global index unchanged.
@@ -101,7 +106,10 @@ fn lemma_r03_zero_emission_rate_index_unchanged() {
     let mut state = RewardsState::new(0, 1_000_000);
     let initial_index = state.global_index;
     state.update_global(86_400);
-    assert_eq!(state.global_index, initial_index, "R-03: index changed with zero emission");
+    assert_eq!(
+        state.global_index, initial_index,
+        "R-03: index changed with zero emission"
+    );
 }
 
 /// **R-04**: User accrual is non-negative for non-negative balance and positive index delta.
@@ -111,7 +119,11 @@ fn lemma_r04_user_accrual_is_non_negative() {
     state.update_global(1000); // Advance global index
     let balance = 100_000i128;
     state.update_user(1000, balance);
-    assert!(state.user_accrued >= 0, "R-04: negative user accrual={}", state.user_accrued);
+    assert!(
+        state.user_accrued >= 0,
+        "R-04: negative user accrual={}",
+        state.user_accrued
+    );
 }
 
 /// **R-05**: Same-timestamp update is idempotent (global index unchanged).
@@ -121,7 +133,10 @@ fn lemma_r05_same_timestamp_is_idempotent() {
     state.update_global(3600);
     let index_after_first = state.global_index;
     state.update_global(3600); // Same timestamp
-    assert_eq!(state.global_index, index_after_first, "R-05: second update at same time changed index");
+    assert_eq!(
+        state.global_index, index_after_first,
+        "R-05: second update at same time changed index"
+    );
 }
 
 /// **R-06**: Claim zeroes user accrued rewards.
@@ -130,7 +145,10 @@ fn lemma_r06_claim_zeroes_accrued() {
     let mut state = RewardsState::new(500, 1_000_000);
     state.update_user(10_000, 500_000);
     state.claim();
-    assert_eq!(state.user_accrued, 0, "R-06: accrued not zeroed after claim");
+    assert_eq!(
+        state.user_accrued, 0,
+        "R-06: accrued not zeroed after claim"
+    );
 }
 
 /// **R-07**: No overflow for realistic emission and time values.
diff --git a/stellar-lend/contracts/lending/src/spec/withdraw_spec.rs b/stellar-lend/contracts/lending/src/spec/withdraw_spec.rs
index e643cdd3..d14e4f1e 100644
--- a/stellar-lend/contracts/lending/src/spec/withdraw_spec.rs
+++ b/stellar-lend/contracts/lending/src/spec/withdraw_spec.rs
@@ -33,7 +33,12 @@ pub enum WithdrawError {
 
 impl WithdrawState {
     pub fn new(collateral: i128, total: i128, debt: i128, min: i128) -> Self {
-        Self { user_collateral: collateral, total_deposits: total, outstanding_debt: debt, min_withdraw: min }
+        Self {
+            user_collateral: collateral,
+            total_deposits: total,
+            outstanding_debt: debt,
+            min_withdraw: min,
+        }
     }
 
     pub fn apply_withdraw(&mut self, amount: i128) -> Result<(), WithdrawError> {
@@ -43,10 +48,14 @@ impl WithdrawState {
         if amount > self.user_collateral {
             return Err(WithdrawError::InsufficientCollateral);
         }
-        let remaining = self.user_collateral.checked_sub(amount).ok_or(WithdrawError::Overflow)?;
+        let remaining = self
+            .user_collateral
+            .checked_sub(amount)
+            .ok_or(WithdrawError::Overflow)?;
         // Enforce collateral ratio if user has outstanding debt
         if self.outstanding_debt > 0 {
-            let min_collateral = self.outstanding_debt
+            let min_collateral = self
+                .outstanding_debt
                 .checked_mul(MIN_COLLATERAL_RATIO_BPS)
                 .ok_or(WithdrawError::Overflow)?
                 .checked_div(BPS_DIVISOR)
@@ -65,14 +74,22 @@ impl WithdrawState {
 #[test]
 fn lemma_w01_zero_amount_rejected() {
     let mut s = WithdrawState::new(100_000, 100_000, 0, 0);
-    assert_eq!(s.apply_withdraw(0), Err(WithdrawError::InvalidAmount), "W-01");
+    assert_eq!(
+        s.apply_withdraw(0),
+        Err(WithdrawError::InvalidAmount),
+        "W-01"
+    );
 }
 
 /// **W-02**: Withdraw exceeding balance is rejected.
 #[test]
 fn lemma_w02_over_balance_rejected() {
     let mut s = WithdrawState::new(100_000, 100_000, 0, 0);
-    assert_eq!(s.apply_withdraw(100_001), Err(WithdrawError::InsufficientCollateral), "W-02");
+    assert_eq!(
+        s.apply_withdraw(100_001),
+        Err(WithdrawError::InsufficientCollateral),
+        "W-02"
+    );
 }
 
 /// **W-03**: Remaining balance satisfies the collateral ratio for outstanding debt.
@@ -88,7 +105,10 @@ fn lemma_w03_collateral_ratio_maintained() {
     );
     // Withdrawing 0 of existing debt leaves ratio intact (no-op via W-01)
     // Confirm balance is unchanged
-    assert_eq!(s.user_collateral, 150_000, "W-03: balance mutated on rejection");
+    assert_eq!(
+        s.user_collateral, 150_000,
+        "W-03: balance mutated on rejection"
+    );
 }
 
 /// **W-04**: User balance decreases by exactly the withdrawn amount.
@@ -126,5 +146,8 @@ fn lemma_w07_insufficient_collateral_for_debt_rejected() {
         Err(WithdrawError::InsufficientCollateralRatio),
         "W-07"
     );
-    assert_eq!(s.user_collateral, 200_000, "W-07: state mutated on rejection");
+    assert_eq!(
+        s.user_collateral, 200_000,
+        "W-07: state mutated on rejection"
+    );
 }
diff --git a/stellar-lend/contracts/lending/tests/protocol_formal_specs.rs b/stellar-lend/contracts/lending/tests/protocol_formal_specs.rs
new file mode 100644
index 00000000..869fc1c2
--- /dev/null
+++ b/stellar-lend/contracts/lending/tests/protocol_formal_specs.rs
@@ -0,0 +1,2 @@
+#[path = "../src/spec/protocol_invariants.rs"]
+mod protocol_invariants;