diff --git a/.kiro/specs/lending-protocol-invariant-analysis/.config.kiro b/.kiro/specs/lending-protocol-invariant-analysis/.config.kiro
new file mode 100644
index 0000000..6550a5c
--- /dev/null
+++ b/.kiro/specs/lending-protocol-invariant-analysis/.config.kiro
@@ -0,0 +1 @@
+{"specId": "f0679376-2877-45b4-8379-4a7b0f1e5a74", "workflowType": "requirements-first", "specType": "feature"}
diff --git a/.kiro/specs/lending-protocol-invariant-analysis/design.md b/.kiro/specs/lending-protocol-invariant-analysis/design.md
new file mode 100644
index 0000000..409b2b7
--- /dev/null
+++ b/.kiro/specs/lending-protocol-invariant-analysis/design.md
@@ -0,0 +1,1427 @@
+# Lending Protocol Invariant Analysis - Technical Design
+
+## Overview
+
+The lending protocol invariant analysis module is a deterministic, network-free static analysis engine integrated into `@chainproof/core`. It detects critical lending protocol vulnerabilities through AST-based invariant checking without requiring live network interaction, symbolic execution, or runtime simulation.
+
+This module follows the established architectural pattern from the staking, governance, and bridge analyzers: model extraction → framework adapter recognition → rule evaluation → structured output. It focuses on lending-specific invariants (collateral health, interest accrual, liquidation mechanics, share accounting) and complements the existing callback reentrancy analysis and planned AI economic exploit detection.
+
+### Design Goals
+
+1. **Deterministic analysis**: Identical inputs produce byte-identical outputs for CI reproducibility
+2. **High signal-to-noise**: Evidence-driven findings with explicit assumptions and confidence levels
+3. **Framework awareness**: Recognize Compound-like, Aave-like, and isolated pool patterns
+4. **Resource bounded**: Configurable limits prevent unbounded execution on adversarial input
+5. **Integration-ready**: Seamless TypeScript API, CLI, and existing scan pipeline integration
+
+### Non-Goals
+
+- Runtime simulation or fork-based testing
+- Economic exploit modeling (delegated to AI analysis module #60)
+- Generic reentrancy detection (handled by CP-107, CP-CB-*)
+- Oracle manipulation or price feed attacks
+- Network-specific deployment verification
+
+## Architecture
+
+The implementation follows a four-layer separation of concerns pattern established by existing analyzers:
+
+### Layer 1: Model Extraction (`lending/model.ts`)
+
+**Responsibility**: Parse Solidity AST and build normalized contract models
+
+**Key Components**:
+- **State Variable Classification**: Identify collateral factors, interest indexes, debt shares, health factors, liquidation parameters, oracle references, pause states
+- **Function Role Detection**: Classify functions as deposit/supply, borrow, repay, withdraw, liquidate, accrue interest, update oracle, emergency operations
+- **Operation Sequencing**: Record lexical-ordered reads, writes, arithmetic, guards, external calls with source locations
+- **Precision Tracking**: Extract decimal scalars, fixed-point constants (WAD, RAY, PRECISION)
+- **Cross-Reference Detection**: Map state dependencies across supply, borrow, and liquidation flows
+
+**Output**: `LendingContractModel[]` with normalized state, transitions, and assumptions
+
+### Layer 2: Framework Adapters (`lending/adapters.ts`)
+
+**Responsibility**: Recognize structural patterns from major lending protocol architectures
+
+**Adapter Types**:
+1. **Compound-like CToken**: Exchange rate based shares, supply/borrow indices per market
+2. **Aave-like Pool**: Normalized debt tracking, aTokens/variable debt/stable debt separation  
+3. **Isolated Pools**: Per-market collateral restrictions, asset-specific parameters
+4. **Generic Lending**: Fallback pattern when no specific framework is matched
+
+**Adapter Selection Signals**:
+- State variable patterns (e.g., `borrowIndex`, `liquidityIndex`, `utilizationRate`)
+- Function naming conventions (e.g., `mint`/`redeem` vs `deposit`/`withdraw`)
+- Structural relationships (e.g., separate token contracts for shares vs pool-integrated)
+- Parameter storage patterns (e.g., per-market vs global configuration)
+
+**Output**: `LendingFrameworkAdapterMatch` with matched signals and applicable assumptions
+
+### Layer 3: Accounting Rules (`lending/analyzer.ts`)
+
+**Responsibility**: Evaluate lending-specific invariants on normalized models
+
+**Rule Categories**:
+1. **Collateral Health** (CP-LND-001 to CP-LND-003)
+   - Health factor calculation bypass
+   - Under-collateralized borrow detection
+   - Collateral factor vs liquidation threshold validation
+
+2. **Interest Accrual** (CP-LND-004 to CP-LND-006)
+   - Stale index detection (accrual before state mutation)
+   - Interest index ordering (update before borrow/repay/liquidate)
+   - Reserve factor application consistency
+
+3. **Share Accounting** (CP-LND-007 to CP-LND-009)
+   - Share-to-amount rounding direction errors
+   - Debt share vs normalized amount consistency
+   - Exchange rate manipulation via donation or precision loss
+
+4. **Liquidation Safety** (CP-LND-010 to CP-LND-013)
+   - Self-liquidation vulnerability
+   - Liquidation bonus vs collateral factor inversion
+   - Close factor over-liquidation or under-liquidation
+   - Partial liquidation health factor updates
+
+5. **State Transition Ordering** (CP-LND-014 to CP-LND-016)
+   - Transfer-before-update dangerous patterns
+   - Oracle-read before accrual timing issues
+   - Bad debt accumulation without safeguards
+
+6. **Protocol-Specific** (CP-LND-017 to CP-LND-020)
+   - Rebasing token collateral precision loss
+   - Isolation mode bypass vulnerabilities
+   - Variable vs fixed rate debt inconsistencies
+   - Emergency operation asset recovery risks
+
+**Output**: `LendingFinding[]` with evidence, confidence, and assumptions
+
+### Layer 4: Transport and Presentation (`lending/api.ts`, `lending/serialize.ts`)
+
+**Responsibility**: Expose analysis through stable interfaces
+
+**API Surface**:
+- `analyzeLendingSource(source, file)` - Single in-memory source
+- `analyzeLendingSources(sources)` - Batch in-memory analysis
+- `analyzeLendingFiles(paths, options)` - Filesystem integration
+- `analyzeLendingProject(targets, options)` - Project-level analysis
+- `buildLendingModels(sources)` - Model extraction only (for extensions)
+- `analyzeLendingModel(model, options)` - Rule evaluation on existing model
+
+**CLI Integration**:
+```bash
+chainproof lending contracts/ --output lending-report.md --fail-on high
+chainproof lending contracts/ --format json --include-rule CP-LND-001
+```
+
+**Output Formats**:
+- JSON: Versioned, stable schema with sorted keys and deterministic ordering
+- Markdown: Human-readable report with evidence and recommendations
+- Integration with existing report aggregation pipeline
+
+## Components and Interfaces
+
+### Core Data Structures
+
+```typescript
+// ─── Rule Identifiers ────────────────────────────────────────────────────────
+
+export type LendingRuleId =
+  | "CP-LND-001" // Health factor calculation bypass
+  | "CP-LND-002" // Under-collateralized borrow
+  | "CP-LND-003" // Bonus inversion (bonus > collateral factor)
+  | "CP-LND-004" // Stale interest index
+  | "CP-LND-005" // Interest accrual ordering
+  | "CP-LND-006" // Reserve factor inconsistency
+  | "CP-LND-007" // Share rounding direction error
+  | "CP-LND-008" // Debt share inconsistency
+  | "CP-LND-009" // Exchange rate manipulation
+  | "CP-LND-010" // Self-liquidation vulnerability
+  | "CP-LND-011" // Liquidation bonus configuration error
+  | "CP-LND-012" // Close factor violation
+  | "CP-LND-013" // Partial liquidation health update missing
+  | "CP-LND-014" // Transfer before update
+  | "CP-LND-015" // Oracle read before accrual
+  | "CP-LND-016" // Bad debt safeguard missing
+  | "CP-LND-017" // Rebasing token precision loss
+  | "CP-LND-018" // Isolation mode bypass
+  | "CP-LND-019" // Variable/fixed rate inconsistency
+  | "CP-LND-020"; // Emergency recovery asset overlap
+
+// ─── State Variable Roles ────────────────────────────────────────────────────
+
+export type LendingVariableRole =
+  | "collateral-asset"
+  | "debt-asset"
+  | "interest-index"
+  | "debt-index"
+  | "normalized-debt"
+  | "debt-shares"
+  | "collateral-factor"
+  | "liquidation-threshold"
+  | "liquidation-bonus"
+  | "close-factor"
+  | "reserve-factor"
+  | "exchange-rate"
+  | "total-supply"
+  | "total-borrows"
+  | "user-balance"
+  | "user-borrow"
+  | "utilization-rate"
+  | "oracle-price"
+  | "health-factor"
+  | "accrual-timestamp"
+  | "pause-state"
+  | "isolation-flag"
+  | "debt-ceiling"
+  | "administrator"
+  | "unknown";
+
+// ─── Function Roles ──────────────────────────────────────────────────────────
+
+export type LendingFunctionRole =
+  | "deposit"
+  | "supply"
+  | "mint"
+  | "borrow"
+  | "repay"
+  | "withdraw"
+  | "redeem"
+  | "liquidate"
+  | "accrue-interest"
+  | "update-index"
+  | "update-oracle"
+  | "calculate-health"
+  | "exchange-rate"
+  | "set-collateral-factor"
+  | "set-liquidation-params"
+  | "set-reserve-factor"
+  | "pause"
+  | "unpause"
+  | "emergency-withdraw"
+  | "unknown";
+
+// ─── Framework Adapters ──────────────────────────────────────────────────────
+
+export type LendingFrameworkAdapter =
+  | "compound-ctoken"
+  | "aave-pool"
+  | "isolated-pool"
+  | "generic-lending"
+  | "none";
+
+export interface LendingFrameworkAdapterDefinition {
+  id: Exclude<LendingFrameworkAdapter, "generic-lending" | "none">;
+  displayName: string;
+  requiredStateGroups: string[][]; // OR groups of state patterns
+  requiredFunctions: string[];
+  guarantees: string[]; // Invariants the pattern provides
+  limitations: string[]; // Known blind spots
+}
+
+export interface LendingFrameworkAdapterMatch {
+  adapter: LendingFrameworkAdapter;
+  matchedState: string[];
+  matchedFunctions: string[];
+}
+
+// ─── Evidence and Locations ──────────────────────────────────────────────────
+
+export interface LendingSourceLocation {
+  file: string;
+  line: number;
+  column: number;
+  lineEnd?: number;
+  columnEnd?: number;
+}
+
+export interface LendingEvidence {
+  kind:
+    | "state-read"
+    | "state-write"
+    | "arithmetic"
+    | "branch"
+    | "call"
+    | "modifier"
+    | "ordering"
+    | "parameter-flow"
+    | "adapter"
+    | "absence";
+  description: string;
+  location: LendingSourceLocation;
+  snippet?: string;
+}
+
+// ─── Contract Model ──────────────────────────────────────────────────────────
+
+export interface LendingStateVariable {
+  name: string;
+  typeName: string;
+  role: LendingVariableRole;
+  isMapping: boolean;
+  location: LendingSourceLocation;
+}
+
+export interface LendingOperation {
+  order: number;
+  kind: "read" | "write" | "call" | "arithmetic" | "guard";
+  name: string;
+  expression: string;
+  parameterSources: string[]; // Taint tracking for user-controlled values
+  location: LendingSourceLocation;
+}
+
+export interface LendingTransition {
+  name: string;
+  role: LendingFunctionRole;
+  visibility: string;
+  modifiers: string[];
+  parameters: string[];
+  reads: string[];
+  writes: string[];
+  calls: string[];
+  operations: LendingOperation[];
+  location: LendingSourceLocation;
+  source: string;
+}
+
+export interface LendingContractModel {
+  name: string;
+  file: string;
+  adapter: LendingFrameworkAdapter;
+  stateVariables: LendingStateVariable[];
+  transitions: LendingTransition[];
+  
+  // Lending-specific metadata
+  collateralAssets: string[];
+  debtAssets: string[];
+  oracleReferences: string[];
+  precisionScalars: string[];
+  
+  // Configuration parameters (if detected)
+  collateralFactors: Map<string, string>; // asset -> factor
+  liquidationThresholds: Map<string, string>;
+  liquidationBonuses: Map<string, string>;
+  
+  assumptions: string[];
+  location: LendingSourceLocation;
+}
+
+// ─── Findings ────────────────────────────────────────────────────────────────
+
+export interface LendingFinding {
+  ruleId: LendingRuleId;
+  title: string;
+  description: string;
+  recommendation: string;
+  severity: Exclude<Severity, "gas">;
+  confidence: "high" | "medium" | "low";
+  category:
+    | "collateral-health"
+    | "interest-accrual"
+    | "share-accounting"
+    | "liquidation"
+    | "state-ordering"
+    | "protocol-specific";
+  contract: string;
+  location: LendingSourceLocation;
+  evidence: LendingEvidence[];
+  assumptions: string[];
+}
+
+// ─── Analysis Configuration ──────────────────────────────────────────────────
+
+export const LENDING_CONFIG_SCHEMA_VERSION = 1 as const;
+
+export interface LendingAnalysisConfigV1 {
+  schemaVersion: 1;
+  includeModels?: boolean;
+  includeRules?: LendingRuleId[];
+  excludeRules?: LendingRuleId[];
+  limits?: Partial<LendingAnalysisLimits>;
+  
+  // Protocol-specific configuration
+  protocolTerminology?: {
+    deposit?: string[]; // e.g., ["mint", "supply"]
+    borrow?: string[];
+    repay?: string[];
+    withdraw?: string[]; // e.g., ["redeem", "burn"]
+  };
+  
+  // Manual function annotations when naming is ambiguous
+  functionAnnotations?: {
+    [functionName: string]: LendingFunctionRole;
+  };
+}
+
+export interface LendingAnalysisLimits {
+  maxSourceBytes: number;
+  maxFiles: number;
+  maxContracts: number;
+  maxFunctionsPerFile: number;
+  maxFunctionsPerContract: number;
+  maxOperationsPerFunction: number;
+  maxFindings: number;
+  maxEvidencePerFinding: number;
+}
+
+export const DEFAULT_LENDING_LIMITS: LendingAnalysisLimits = {
+  maxSourceBytes: 2 * 1024 * 1024, // 2 MB
+  maxFiles: 256,
+  maxContracts: 128,
+  maxFunctionsPerFile: 512,
+  maxFunctionsPerContract: 512,
+  maxOperationsPerFunction: 2048,
+  maxFindings: 1024,
+  maxEvidencePerFinding: 12,
+};
+
+// ─── Analysis Report ─────────────────────────────────────────────────────────
+
+export const LENDING_REPORT_SCHEMA_VERSION = "1.0.0" as const;
+
+export interface LendingFileAnalysis {
+  file: string;
+  models: LendingContractModel[];
+  findings: LendingFinding[];
+  diagnostics: LendingDiagnostic[];
+}
+
+export interface LendingAnalysisReport {
+  schemaVersion: typeof LENDING_REPORT_SCHEMA_VERSION;
+  engineVersion: string;
+  timestamp: string;
+  files: LendingFileAnalysis[];
+  summary: {
+    filesAnalyzed: number;
+    contractsModeled: number;
+    findingsBySeverity: {
+      critical: number;
+      high: number;
+      medium: number;
+      low: number;
+    };
+    findingsByCategory: Record<string, number>;
+    truncated: boolean;
+  };
+  assumptions: string[]; // Global assumptions
+  config: LendingAnalysisConfigV1;
+}
+
+// ─── Diagnostics ─────────────────────────────────────────────────────────────
+
+export interface LendingDiagnostic {
+  code:
+    | "LND_PARSE_ERROR"
+    | "LND_SOURCE_LIMIT"
+    | "LND_CONTRACT_LIMIT"
+    | "LND_FUNCTION_LIMIT"
+    | "LND_OPERATION_LIMIT"
+    | "LND_FINDING_LIMIT"
+    | "LND_CANCELLED"
+    | "LND_CONFIG_INVALID"
+    | "LND_FILE_UNREADABLE";
+  message: string;
+  file?: string;
+  line?: number;
+  severity: "error" | "warning" | "info";
+}
+
+// ─── Cancellation ────────────────────────────────────────────────────────────
+
+export interface LendingCancellationSignal {
+  readonly aborted: boolean;
+  readonly reason?: any;
+}
+
+export interface LendingAnalysisOptions {
+  includeModels?: boolean;
+  includeRules?: LendingRuleId[];
+  excludeRules?: LendingRuleId[];
+  limits?: Partial<LendingAnalysisLimits>;
+  signal?: LendingCancellationSignal;
+  protocolTerminology?: LendingAnalysisConfigV1["protocolTerminology"];
+  functionAnnotations?: LendingAnalysisConfigV1["functionAnnotations"];
+}
+```
+
+### Module Structure
+
+```
+packages/core/src/lending/
+├── index.ts              # Public API exports
+├── types.ts              # Type definitions (above)
+├── model.ts              # AST → LendingContractModel extraction
+├── adapters.ts           # Framework pattern recognition
+├── analyzer.ts           # Rule evaluation engine
+├── rule.ts               # Individual rule implementations
+├── config.ts             # Configuration validation and migration
+├── serialize.ts          # JSON and Markdown output
+└── api.ts                # High-level analysis functions
+```
+
+## Data Models
+
+### State Variable Classification
+
+The model builder walks the AST and assigns semantic roles based on:
+
+1. **Name patterns**: `borrowIndex`, `liquidationThreshold`, `collateralFactor`, `healthFactor`
+2. **Type patterns**: `mapping(address => uint256)` for user balances, `uint256` for global state
+3. **Usage patterns**: Variables read in health calculations, written in accrual functions
+4. **Relationship patterns**: Variables that share update timing or mathematical relationships
+
+**Confidence scoring**:
+- High: Multiple signals align (name + type + usage)
+- Medium: Name or usage matches but type is ambiguous
+- Low: Inferred from single weak signal
+
+### Function Role Detection
+
+Functions are classified through:
+
+1. **Signature analysis**: Parameters indicate deposit (asset, amount) vs borrow (asset, amount) vs liquidate (borrower, collateral, debt)
+2. **State effect analysis**: Which variables are read vs written
+3. **External call patterns**: Token transfers in (deposit) vs out (withdraw/liquidate)
+4. **Ordering analysis**: Whether accrual happens before or after state changes
+
+### Operation Sequencing
+
+Each function body is linearized into ordered operations:
+
+```typescript
+{
+  order: 42,
+  kind: "write",
+  name: "borrowIndex",
+  expression: "borrowIndex = calculateNewIndex()",
+  location: { file: "Pool.sol", line: 123, column: 5 }
+}
+```
+
+This enables detection of:
+- **Accrual-before-mutation**: Index updates must precede balance changes
+- **Transfer-after-update**: External calls should follow accounting updates
+- **Oracle-after-accrual**: Price reads should use fresh accrued state
+
+### Precision and Rounding Tracking
+
+The model extracts fixed-point constants:
+
+```typescript
+precisionScalars: ["1e18", "1e27", "PRECISION", "WAD", "RAY"]
+```
+
+And tracks division/multiplication patterns to detect precision loss:
+- Division before multiplication: `(a / b) * c` loses precision
+- Missing scalar: `shares / totalShares` without `* PRECISION` multiplier
+- Incorrect rounding: `borrowed.divUp()` should round against user, `repay.divDown()` should round for protocol
+
+## Error Handling
+
+### Diagnostic Categories
+
+1. **Parse Errors** (`LND_PARSE_ERROR`): Solidity AST construction failed
+2. **Resource Limits** (`LND_*_LIMIT`): Budget exceeded, partial analysis
+3. **Configuration Errors** (`LND_CONFIG_INVALID`): Invalid schema, rule IDs, or limits
+4. **IO Errors** (`LND_FILE_UNREADABLE`): Filesystem access failed
+5. **Cancellation** (`LND_CANCELLED`): User-requested abort
+
+### Error Context
+
+Error messages include:
+- ✅ Actionable information (which file, which rule, which limit)
+- ✅ Sanitized file paths (relative to project root)
+- ❌ **Never** include source code contents in errors
+- ❌ **Never** include absolute paths or user directories
+- ❌ **Never** include credentials or configuration secrets
+
+Example:
+```
+LND_CONFIG_INVALID: Configuration validation failed
+  • Rule ID "CP-LND-999" is not recognized
+  • Valid rule IDs: CP-LND-001 through CP-LND-020
+  • Location: .chainproof/lending-config.json
+```
+
+### Graceful Degradation
+
+When limits are reached:
+1. Emit a diagnostic with severity "warning"
+2. Mark `summary.truncated = true` in the report
+3. Return partial results for the analyzed portion
+4. **Do not** throw exceptions (except for cancellation)
+
+### Cancellation
+
+The analysis checks `signal.aborted` at:
+- Start of each file
+- Start of each contract
+- Start of each rule evaluation
+
+When cancelled:
+- Throw `LendingAnalysisCancelledError` with reason
+- Do not emit partial findings from interrupted rules
+- Return clean diagnostic with `LND_CANCELLED` code
+
+## Testing Strategy
+
+The lending analyzer uses **fixture-based testing** with paired vulnerable/secure contracts, following the pattern established by staking, governance, and bridge modules. Property-based testing is **not applicable** because:
+
+1. This is **static analysis infrastructure** that operates on AST inputs, not application logic with universal properties
+2. The analyzer's correctness is validated through **concrete test cases** (vulnerable contracts that should produce findings, secure contracts that should not)
+3. The existing ChainProof analyzers all use fixture-based testing, not PBT
+
+### Test Structure
+
+#### 1. Unit Tests
+
+**Model Extraction Tests** (`model.test.ts`):
+- ✅ Variable role classification accuracy
+- ✅ Function role detection across naming conventions
+- ✅ Operation sequencing correctness
+- ✅ Precision scalar extraction
+- ✅ Adapter signal matching
+
+**Rule Tests** (`rule.test.ts`):
+- ✅ Each rule produces expected finding on vulnerable fixture
+- ✅ Each rule produces zero findings on secure fixture
+- ✅ False positive controls (similar but safe patterns)
+- ✅ Confidence level accuracy
+- ✅ Evidence path completeness
+
+**Configuration Tests** (`config.test.ts`):
+- ✅ Schema validation (valid/invalid configs)
+- ✅ Migration from v0 to v1
+- ✅ Rule allowlist/denylist logic
+- ✅ Limit validation (positive integers, no zero/negative)
+- ✅ Corruption handling (malformed JSON)
+
+#### 2. Integration Tests
+
+**End-to-End Analysis**:
+```typescript
+test("CP-LND-001: Detects health factor bypass", () => {
+  const source = readFixture("VulnerableHealthBypass.sol");
+  const report = analyzeLendingSource(source, "test.sol");
+  
+  expect(report.findings).toHaveLength(1);
+  expect(report.findings[0].ruleId).toBe("CP-LND-001");
+  expect(report.findings[0].severity).toBe("critical");
+  expect(report.findings[0].confidence).toBe("high");
+  expect(report.findings[0].evidence.length).toBeGreaterThan(0);
+});
+
+test("CP-LND-001: No false positive on secure implementation", () => {
+  const source = readFixture("SecureHealthCheck.sol");
+  const report = analyzeLendingSource(source, "test.sol");
+  
+  expect(report.findings.filter(f => f.ruleId === "CP-LND-001")).toHaveLength(0);
+});
+```
+
+**Multi-File Analysis**:
+- ✅ Cross-contract relationships (e.g., Pool + CToken + Oracle)
+- ✅ Import resolution and reference tracking
+- ✅ Deterministic ordering across file systems
+
+**Resource Limits**:
+- ✅ Large files trigger `LND_SOURCE_LIMIT` diagnostic
+- ✅ Deep nesting triggers `LND_OPERATION_LIMIT`
+- ✅ Many contracts trigger `LND_CONTRACT_LIMIT`
+- ✅ Analysis completes with partial results, no crash
+
+**Cancellation**:
+- ✅ AbortController integration
+- ✅ Clean error on cancellation
+- ✅ No partial findings from interrupted rules
+
+#### 3. Fixture Coverage
+
+**Vulnerable Fixtures** (`examples/contracts/lending/vulnerable/`):
+- `VulnerableHealthBypass.sol` - CP-LND-001, CP-LND-002
+- `VulnerableStaleIndex.sol` - CP-LND-004, CP-LND-005
+- `VulnerableRounding.sol` - CP-LND-007, CP-LND-009
+- `VulnerableSelfLiquidation.sol` - CP-LND-010
+- `VulnerableBonusInversion.sol` - CP-LND-003, CP-LND-011
+- `VulnerableTransferOrdering.sol` - CP-LND-014
+- `VulnerableRebasingCollateral.sol` - CP-LND-017
+- `VulnerableIsolationBypass.sol` - CP-LND-018
+- `VulnerableBadDebt.sol` - CP-LND-016
+
+**Secure Fixtures** (`examples/contracts/lending/secure/`):
+- `SecureHealthCheck.sol` - Proper health factor enforcement
+- `SecureAccrualOrdering.sol` - Correct index update sequencing
+- `SecureRoundingDirection.sol` - Proper round-up/round-down usage
+- `SecureLiquidationGuards.sol` - Self-liquidation prevention
+- `SecureTransferSequence.sol` - Update-before-transfer pattern
+- `SecureRebasingShares.sol` - Share-based rebasing token handling
+- `SecureIsolationMode.sol` - Proper isolation enforcement
+
+**False Positive Controls** (`examples/contracts/lending/controls/`):
+- `UnrelatedHealthCalculation.sol` - Health factor in non-lending context
+- `SafeAdminFunction.sol` - Privileged operations with proper access control
+- `NonLendingShares.sol` - Share tokens unrelated to lending
+
+**Boundary Conditions**:
+- Zero-amount operations
+- Maximum uint256 values
+- Single-wei precision edge cases
+- Empty pool states (zero supply, zero borrows)
+- Extreme collateral factors (0%, 100%)
+
+#### 4. Serialization Tests
+
+**JSON Output**:
+- ✅ Schema version present
+- ✅ Deterministic key ordering (sorted)
+- ✅ No timestamps or host-specific data
+- ✅ Byte-identical output for identical input
+
+**Markdown Output**:
+- ✅ Readable formatting with code blocks
+- ✅ Evidence sections with source locations
+- ✅ Recommendations clearly stated
+- ✅ Summary statistics table
+
+#### 5. CLI Tests
+
+**Command-line Interface**:
+```bash
+# Exit code 0: No findings above threshold
+chainproof lending contracts/secure/ --fail-on high
+
+# Exit code 1: Findings above threshold
+chainproof lending contracts/vulnerable/ --fail-on medium
+
+# Exit code 2: Configuration error
+chainproof lending contracts/ --include-rule CP-LND-999
+
+# JSON output is clean (no banner/progress)
+chainproof lending contracts/ --format json | jq '.schemaVersion'
+```
+
+#### 6. Performance Tests
+
+**Analysis Speed**:
+- ✅ Large codebase (100+ files) completes within time budget
+- ✅ Deep inheritance chains don't cause exponential blowup
+- ✅ Complex functions stay within operation limit
+
+**Memory Usage**:
+- ✅ Streaming file processing (not loading entire project into memory)
+- ✅ Model garbage collection between files
+- ✅ No memory leaks in long-running CLI processes
+
+### Test Execution
+
+```bash
+# Run all tests
+npm test
+
+# Run specific test suite
+npm test -- lending/model.test.ts
+
+# Coverage report
+npm run coverage
+
+# Lint and type check
+npm run lint
+```
+
+### Continuous Integration
+
+The CI pipeline runs:
+1. Unit tests (all rules, all adapters)
+2. Integration tests (fixtures, limits, cancellation)
+3. CLI tests (exit codes, JSON cleanliness)
+4. Serialization determinism check (run twice, compare output)
+5. TypeScript type checking
+6. ESLint with no warnings
+7. Coverage threshold enforcement (>80%)
+
+## Deployment and Integration
+
+### Installation
+
+```bash
+# Install ChainProof with lending analyzer
+npm install @chainproof/core
+
+# CLI usage (global install)
+npm install -g @chainproof/cli
+chainproof lending --help
+```
+
+### API Usage
+
+```typescript
+import {
+  analyzeLendingFiles,
+  serializeLendingReportJSON,
+  type LendingAnalysisOptions,
+} from "@chainproof/core";
+
+const options: LendingAnalysisOptions = {
+  includeModels: true,
+  includeRules: ["CP-LND-001", "CP-LND-004", "CP-LND-010"],
+  limits: {
+    maxFiles: 100,
+    maxSourceBytes: 1_000_000,
+    maxFindings: 500,
+  },
+  protocolTerminology: {
+    deposit: ["mint", "supply"],
+    withdraw: ["redeem", "burn"],
+  },
+};
+
+const report = analyzeLendingFiles(["contracts/lending/"], options);
+console.log(serializeLendingReportJSON(report));
+```
+
+### CLI Usage
+
+```bash
+# Markdown report for human review
+chainproof lending contracts/ --output lending-report.md --fail-on high
+
+# JSON for CI pipeline
+chainproof lending contracts/ --format json --fail-on critical > report.json
+
+# Focused analysis
+chainproof lending contracts/Pool.sol \
+  --include-rule CP-LND-001 \
+  --include-rule CP-LND-004 \
+  --include-models
+
+# Configuration file
+chainproof lending contracts/ --config .chainproof/lending-config.json
+
+# Resource limits
+chainproof lending contracts/ \
+  --max-files 200 \
+  --max-source-bytes 5000000 \
+  --max-findings 1000
+```
+
+### Configuration File
+
+```json
+{
+  "schemaVersion": 1,
+  "includeModels": false,
+  "includeRules": [
+    "CP-LND-001",
+    "CP-LND-002",
+    "CP-LND-004",
+    "CP-LND-010"
+  ],
+  "excludeRules": [],
+  "limits": {
+    "maxSourceBytes": 2097152,
+    "maxFiles": 256,
+    "maxContracts": 128,
+    "maxFunctionsPerFile": 512,
+    "maxFunctionsPerContract": 512,
+    "maxOperationsPerFunction": 2048,
+    "maxFindings": 1024,
+    "maxEvidencePerFinding": 12
+  },
+  "protocolTerminology": {
+    "deposit": ["mint", "supply", "provide"],
+    "borrow": ["loan", "draw"],
+    "repay": ["payback", "return"],
+    "withdraw": ["redeem", "burn", "remove"]
+  },
+  "functionAnnotations": {
+    "executeFlashLoan": "unknown",
+    "adminLiquidate": "liquidate"
+  }
+}
+```
+
+### Integration with Existing Scan
+
+The lending analyzer integrates with the main `scan()` API:
+
+```typescript
+import { scan, type ScanConfig } from "@chainproof/core";
+
+const config: ScanConfig = {
+  targets: ["contracts/"],
+  useSlither: true,
+  useLLM: false,
+  useMetrics: false,
+  // Lending analysis runs automatically on detected lending contracts
+};
+
+const result = await scan(config);
+// result.files includes generic findings + lending-specific findings
+```
+
+The integration:
+1. Detects lending contracts through state/function signals
+2. Runs lending-specific rules in addition to generic rules
+3. Merges findings into unified report
+4. Avoids duplication with existing reentrancy/callback detection
+
+## Performance and Scalability
+
+### Resource Budgets
+
+Default limits prevent unbounded execution:
+
+| Resource | Default Limit | Rationale |
+|----------|---------------|-----------|
+| Source bytes per file | 2 MB | Prevents single-file DoS |
+| Files per project | 256 | Typical monorepo size |
+| Contracts per file | 128 | Handles large inheritance |
+| Functions per file | 512 | Prevents AST explosion |
+| Operations per function | 2048 | Bounds complexity analysis |
+| Findings per analysis | 1024 | Prevents report DoS |
+| Evidence per finding | 12 | Keeps findings actionable |
+
+### Performance Targets
+
+- **Small project** (10 files, 5K LOC): < 1 second
+- **Medium project** (100 files, 50K LOC): < 10 seconds
+- **Large project** (500 files, 250K LOC): < 60 seconds
+
+### Optimization Strategies
+
+1. **Lazy AST traversal**: Don't parse functions until needed
+2. **Incremental model building**: Stream contracts, don't accumulate
+3. **Rule short-circuiting**: Skip remaining rules when limit reached
+4. **Evidence pruning**: Keep only most relevant evidence items
+5. **Deterministic caching**: Cache adapter matches per file
+
+### Memory Management
+
+- Use iterative AST walking (no recursion depth limits)
+- Release models after rule evaluation
+- Stream JSON serialization (no in-memory string building)
+- Garbage collect between files
+
+## Security and Threat Model
+
+### Threat Model Scope
+
+**In Scope**:
+- ✅ Incorrect health factor calculation or bypass
+- ✅ Stale interest index usage
+- ✅ Share accounting rounding errors
+- ✅ Self-liquidation vulnerabilities
+- ✅ Liquidation parameter misconfiguration
+- ✅ Transfer-before-update dangerous ordering
+- ✅ Bad debt accumulation without safeguards
+- ✅ Rebasing token precision loss
+- ✅ Isolation mode bypass
+
+**Out of Scope**:
+- ❌ Oracle manipulation or price feed attacks (external assumption)
+- ❌ Economic arbitrage or MEV extraction (delegated to AI analysis)
+- ❌ Governance attacks on parameter updates (governance module)
+- ❌ Flash loan attack vectors (callback reentrancy module)
+- ❌ Network-specific deployment correctness
+
+### Security Assumptions
+
+The analyzer makes explicit assumptions:
+
+1. **Oracle Trust**: "Assumes oracle provides correct prices"
+2. **Token Standards**: "Assumes ERC-20 tokens follow standard return value conventions"
+3. **External Contracts**: "Does not analyze external library implementations"
+4. **Deployment Configuration**: "Does not verify on-chain parameter values"
+5. **Access Control**: "Assumes privileged roles are secured (separate governance analysis)"
+
+These assumptions are:
+- Documented in each relevant finding
+- Listed in the global `report.assumptions` array
+- Explained in the documentation
+
+### Secrets and Sensitive Data
+
+The analyzer **never**:
+- Accesses network or makes RPC calls
+- Reads environment variables or `.env` files
+- Logs source code contents in errors
+- Includes absolute filesystem paths in reports
+- Stores analysis results persistently
+
+Error messages are sanitized:
+```typescript
+// ❌ BAD
+throw new Error(`Parse error in /Users/alice/.ssh/contracts/Pool.sol: ${sourceCode}`);
+
+// ✅ GOOD
+throw new LendingConfigError("LND_PARSE_ERROR", "Failed to parse Solidity source", {
+  file: "Pool.sol", // Relative path
+  line: 42,
+  // No source code included
+});
+```
+
+## Documentation
+
+### User Documentation
+
+**Main Documentation** (`docs/lending-invariants.md`):
+- Overview and threat model
+- Rule reference with examples
+- Framework adapter descriptions
+- CLI usage guide
+- API reference with TypeScript examples
+- Configuration schema
+- Troubleshooting guide
+- Integration examples
+
+**README Section**:
+- Quick start example
+- Link to full documentation
+- Supported lending patterns
+- Example findings
+
+### Developer Documentation
+
+**Architecture Document** (this document):
+- System design and component breakdown
+- Data model specifications
+- Testing strategy
+- Performance targets
+
+**API Documentation** (TypeDoc generated):
+- Full TypeScript API reference
+- Type definitions with inline examples
+- Function signatures and return types
+
+**Code Comments**:
+- Explain "why" not "what"
+- Document assumptions and edge cases
+- Link to related rules or findings
+
+### Examples and Recipes
+
+**Common Use Cases**:
+```typescript
+// Example 1: Analyze specific protocol
+import { analyzeLendingFiles } from "@chainproof/core";
+
+const report = analyzeLendingFiles(
+  ["contracts/lending/Pool.sol", "contracts/lending/CToken.sol"],
+  {
+    includeRules: ["CP-LND-001", "CP-LND-004"],
+    protocolTerminology: { deposit: ["mint"], withdraw: ["redeem"] },
+  }
+);
+
+// Example 2: CI integration
+const hasHighSeverity = report.summary.findingsBySeverity.critical > 0
+  || report.summary.findingsBySeverity.high > 0;
+process.exit(hasHighSeverity ? 1 : 0);
+
+// Example 3: Custom rule extension
+import { buildLendingModels, analyzeLendingModel } from "@chainproof/core";
+
+const models = buildLendingModels(sources);
+for (const model of models) {
+  const findings = customLendingRule(model);
+  // Process custom findings
+}
+```
+
+## Migration and Versioning
+
+### Configuration Migration
+
+Legacy schema v0 migration:
+
+| v0 Field | v1 Field | Transformation |
+|----------|----------|----------------|
+| `maxFileSize` | `limits.maxSourceBytes` | Direct copy |
+| `maxIssues` | `limits.maxFindings` | Direct copy |
+| `rules` | `includeRules` | Direct copy |
+
+Migration function:
+```typescript
+export function migrateLendingConfig(input: any): LendingAnalysisConfigV1 {
+  if (input.schemaVersion === 1) return input;
+  
+  if (!input.schemaVersion || input.schemaVersion === 0) {
+    return {
+      schemaVersion: 1,
+      includeModels: input.includeModels ?? false,
+      includeRules: input.rules ?? [],
+      excludeRules: input.excludeRules ?? [],
+      limits: {
+        ...DEFAULT_LENDING_LIMITS,
+        maxSourceBytes: input.maxFileSize ?? DEFAULT_LENDING_LIMITS.maxSourceBytes,
+        maxFindings: input.maxIssues ?? DEFAULT_LENDING_LIMITS.maxFindings,
+      },
+    };
+  }
+  
+  throw new LendingConfigError(
+    "LND_CONFIG_INVALID",
+    `Unsupported config schema version: ${input.schemaVersion}`
+  );
+}
+```
+
+### Report Versioning
+
+Report schema version: `1.0.0`
+
+**Semantic versioning**:
+- **Major** (2.0.0): Breaking changes to report structure
+- **Minor** (1.1.0): New rule IDs or optional fields added
+- **Patch** (1.0.1): Bug fixes, no schema changes
+
+Consumers should:
+```typescript
+const report = JSON.parse(reportJson);
+if (report.schemaVersion !== "1.0.0") {
+  throw new Error(`Unsupported report schema: ${report.schemaVersion}`);
+}
+// Process report fields
+```
+
+### Deprecation Policy
+
+When deprecating features:
+1. Add deprecation warning in code (TypeScript `@deprecated`)
+2. Document in CHANGELOG with migration path
+3. Support deprecated API for at least 2 minor versions
+4. Remove in next major version
+
+## Troubleshooting Guide
+
+### Common Issues
+
+**Issue: No contracts detected**
+- **Cause**: Files don't match `.sol` extension or exceed size limit
+- **Solution**: Check file extensions, verify `maxSourceBytes` limit
+- **Debug**: Run with `--include-models` to see what was parsed
+
+**Issue: Unexpected truncation**
+- **Cause**: Resource limit reached
+- **Solution**: Check `diagnostics` array for `LND_*_LIMIT` codes
+- **Fix**: Increase only the exhausted limit in configuration
+
+**Issue: Missing inherited behavior**
+- **Cause**: Lending analyzer is file-scoped, doesn't resolve imports
+- **Solution**: Use main `scan()` API for cross-file analysis
+- **Workaround**: Provide annotated parent contracts
+
+**Issue: False positive on safe pattern**
+- **Cause**: Unusual naming convention or indirect implementation
+- **Solution**: Use `functionAnnotations` to clarify intent
+- **Report**: Open issue with minimal reproduction case
+
+**Issue: CI exit code 1 on expected findings**
+- **Cause**: `--fail-on` threshold includes expected severity
+- **Solution**: Adjust threshold or use `--fail-on none` with custom gate
+- **Best practice**: Fix high/critical issues, don't lower threshold
+
+**Issue: Adapter not recognized**
+- **Cause**: Protocol uses non-standard naming or structure
+- **Solution**: Call `matchLendingFramework()` to see matched signals
+- **Workaround**: Use `protocolTerminology` configuration
+- **Note**: Adapter selection doesn't suppress findings
+
+### Debug Mode
+
+Enable verbose logging:
+```bash
+DEBUG=chainproof:lending chainproof lending contracts/
+```
+
+Output includes:
+- Model extraction steps
+- Adapter matching signals
+- Rule evaluation decisions
+- Evidence collection
+
+### Performance Debugging
+
+Profile analysis time:
+```bash
+time chainproof lending contracts/ --format json > /dev/null
+```
+
+If slow:
+1. Check file count and total LOC
+2. Identify deep nesting or large functions
+3. Increase limits gradually to find bottleneck
+4. Use `--include-rule` to test individual rules
+
+### Reporting Issues
+
+Include in bug reports:
+- ChainProof version (`chainproof --version`)
+- Node.js version (`node --version`)
+- Command used (sanitize paths)
+- Configuration file (remove sensitive data)
+- Minimal reproduction case (smallest contract exhibiting issue)
+- Expected vs actual behavior
+
+Do **not** include:
+- Full project source code (provide minimal example)
+- Absolute filesystem paths
+- Credentials or API keys
+- Company-confidential contract logic
+
+## Future Enhancements
+
+### Planned Features (Post-MVP)
+
+1. **Cross-Contract Analysis**: Resolve imports and track state across Pool + CToken + Oracle contracts
+2. **Symbolic Execution Integration**: Combine AST analysis with symbolic path exploration for higher confidence
+3. **Economic Invariant Checking**: Validate "total debt ≤ total collateral * collateral factors" through SMT solver
+4. **Flash Loan Context**: Detect reentrancy through flash loan callbacks
+5. **Upgrade Safety**: Analyze storage layout changes in upgradeable lending protocols
+6. **Historical Vulnerability Database**: Match patterns against known exploits (Compound, Aave, Euler incidents)
+
+### Research Directions
+
+1. **Machine Learning**: Train model on labeled lending contracts to improve adapter recognition
+2. **Fuzzing Integration**: Generate test cases that violate detected invariants
+3. **Formal Verification**: Integrate with Certora or Halmos for mathematical proofs
+4. **Gas Optimization**: Detect inefficient lending patterns (e.g., redundant accruals)
+
+### Community Contributions
+
+Contributors can extend the analyzer by:
+- Adding new framework adapters (`adapters.ts`)
+- Implementing new rules (`rule.ts`)
+- Improving precision tracking (`model.ts`)
+- Adding test fixtures (`examples/contracts/lending/`)
+
+Contribution guidelines in `CONTRIBUTING.md`.
+
+## Appendix A: Rule Reference
+
+### CP-LND-001: Health Factor Calculation Bypass
+
+**Severity**: Critical  
+**Confidence**: High when borrow function lacks health factor read  
+**Description**: Borrow operations complete without calculating or enforcing health factor thresholds, allowing under-collateralized positions.  
+**Evidence**: Borrow function writes debt state but doesn't read collateral state or call health calculation.  
+**Recommendation**: Call `_checkHealthFactor(user)` after all debt state updates.
+
+### CP-LND-002: Under-Collateralized Borrow
+
+**Severity**: Critical  
+**Confidence**: High when health check present but returns value is unused  
+**Description**: Health factor is calculated but the result is not compared against liquidation threshold.  
+**Evidence**: Health calculation function called but return value discarded or not checked with `require()`.  
+**Recommendation**: `require(healthFactor >= LIQUIDATION_THRESHOLD, "Under-collateralized")`.
+
+### CP-LND-003: Bonus Inversion
+
+**Severity**: High  
+**Confidence**: High when configuration state is present  
+**Description**: Liquidation bonus exceeds collateral factor, creating perverse liquidation incentives.  
+**Evidence**: `liquidationBonus > collateralFactor` in configuration.  
+**Recommendation**: Enforce `liquidationBonus < collateralFactor` in parameter setters.
+
+### CP-LND-004: Stale Interest Index
+
+**Severity**: High  
+**Confidence**: High when index read precedes accrual call  
+**Description**: Interest index is read for calculations before calling the accrual function, causing incorrect debt or supply amounts.  
+**Evidence**: `borrowIndex` read in operation N, `accrueInterest()` called in operation N+k.  
+**Recommendation**: Call `accrueInterest()` before any index-dependent calculations.
+
+### CP-LND-005: Interest Accrual Ordering
+
+**Severity**: High  
+**Confidence**: Medium when accrual happens but after state mutation  
+**Description**: Debt or supply state is modified before interest accrual updates indexes, causing accounting errors.  
+**Evidence**: `totalBorrows += amount` in operation N, `accrueInterest()` in operation N+k.  
+**Recommendation**: Sequence: 1) accrue interest, 2) update state, 3) external calls.
+
+### CP-LND-006: Reserve Factor Inconsistency
+
+**Severity**: Medium  
+**Confidence**: Low when reserve factor state present but not applied  
+**Description**: Interest accrual doesn't split protocol reserves correctly, causing reserve accumulation errors.  
+**Evidence**: Interest calculation present but no reserve factor multiplication.  
+**Recommendation**: `protocolReserves += interestAccrued * reserveFactor / PRECISION`.
+
+### CP-LND-007: Share Rounding Direction Error
+
+**Severity**: Medium  
+**Confidence**: High when division direction is wrong  
+**Description**: Share-to-amount conversions round in user's favor instead of protocol's favor, enabling value extraction.  
+**Evidence**: Deposit uses `shares = amount / exchangeRate` (should round down), withdraw uses same (should round up).  
+**Recommendation**: Deposits round down, withdrawals round up, borrows round up, repays round down.
+
+### CP-LND-008: Debt Share Inconsistency
+
+**Severity**: High  
+**Confidence**: Medium when debt shares and normalized debt coexist  
+**Description**: Debt shares and normalized debt amounts are inconsistent due to incorrect index usage.  
+**Evidence**: Debt shares written but normalized debt read without index conversion.  
+**Recommendation**: `actualDebt = debtShares * debtIndex / PRECISION` consistently.
+
+### CP-LND-009: Exchange Rate Manipulation
+
+**Severity**: High  
+**Confidence**: Low when donation path exists  
+**Description**: Direct token donations can manipulate exchange rate before first deposit, enabling inflation attacks.  
+**Evidence**: Exchange rate calculated as `totalAssets / totalShares` without minimum shares or virtual supply.  
+**Recommendation**: Mint minimum shares to zero address or use virtual supply in exchange rate.
+
+### CP-LND-010: Self-Liquidation Vulnerability
+
+**Severity**: Critical  
+**Confidence**: High when liquidation allows `msg.sender == borrower`  
+**Description**: Users can liquidate their own positions to extract liquidation bonuses, draining protocol.  
+**Evidence**: Liquidation function lacks `require(msg.sender != borrower)` check.  
+**Recommendation**: `require(msg.sender != borrower, "Self-liquidation forbidden")`.
+
+### CP-LND-011: Liquidation Bonus Configuration Error
+
+**Severity**: Medium  
+**Confidence**: High when bonus parameter validation missing  
+**Description**: Liquidation bonus can be set to extreme values (0% or >100%), breaking liquidation incentives.  
+**Evidence**: `setLiquidationBonus()` lacks bounds checking.  
+**Recommendation**: `require(bonus >= MIN_BONUS && bonus <= MAX_BONUS)` in setter.
+
+### CP-LND-012: Close Factor Violation
+
+**Severity**: High  
+**Confidence**: Medium when close factor exists but not enforced  
+**Description**: Liquidation can exceed close factor percentage, enabling over-liquidation attacks.  
+**Evidence**: `liquidate()` doesn't check `repayAmount <= borrowBalance * closeFactor / PRECISION`.  
+**Recommendation**: Enforce close factor limit in liquidation calculations.
+
+### CP-LND-013: Partial Liquidation Health Update Missing
+
+**Severity**: High  
+**Confidence**: Medium when health factor not recalculated after partial liquidation  
+**Description**: Health factor is not recalculated after partial liquidation, potentially allowing immediate re-liquidation.  
+**Evidence**: Liquidation updates debt and collateral but doesn't call health check afterward.  
+**Recommendation**: Recalculate and verify health factor after each liquidation.
+
+### CP-LND-014: Transfer Before Update
+
+**Severity**: High  
+**Confidence**: High when external call precedes state write  
+**Description**: Token transfers occur before internal accounting updates, enabling reentrancy or fee-on-transfer exploitation.  
+**Evidence**: `token.transferFrom()` in operation N, balance state written in operation N+k.  
+**Recommendation**: Update state first, perform external calls last (checks-effects-interactions).
+
+### CP-LND-015: Oracle Read Before Accrual
+
+**Severity**: Medium  
+**Confidence**: Medium when oracle read precedes accrual  
+**Description**: Oracle price is read before interest accrual, causing health calculations to use stale debt amounts.  
+**Evidence**: `oracle.getPrice()` called before `accrueInterest()` in health check.  
+**Recommendation**: Sequence: 1) accrue interest, 2) read oracle, 3) calculate health.
+
+### CP-LND-016: Bad Debt Safeguard Missing
+
+**Severity**: High  
+**Confidence**: Low when liquidation allows underwater positions  
+**Description**: Liquidation proceeds even when collateral value is insufficient to cover debt, creating bad debt.  
+**Evidence**: Liquidation doesn't check `collateralValue >= debtValue * liquidationIncentive`.  
+**Recommendation**: Revert liquidations that would create protocol insolvency.
+
+### CP-LND-017: Rebasing Token Precision Loss
+
+**Severity**: High  
+**Confidence**: Medium when rebasing token detected with nominal balances  
+**Description**: Rebasing tokens (e.g., stETH) are tracked with nominal balances instead of shares, causing value drift.  
+**Evidence**: Rebasing token address hardcoded but balances stored as `uint256` without conversion.  
+**Recommendation**: Convert rebasing tokens to shares: `shares = token.getSharesByPooledEth(amount)`.
+
+### CP-LND-018: Isolation Mode Bypass
+
+**Severity**: High  
+**Confidence**: Medium when isolation flag present but not enforced  
+**Description**: Isolation mode restrictions can be bypassed, allowing unauthorized asset borrowing.  
+**Evidence**: `isIsolated` flag read but borrowing doesn't check approved asset list.  
+**Recommendation**: `require(isApprovedForIsolation[asset], "Asset not approved")` in borrow.
+
+### CP-LND-019: Variable/Fixed Rate Inconsistency
+
+**Severity**: Medium  
+**Confidence**: Low when both debt types present  
+**Description**: Variable and fixed rate debt tracking is inconsistent, causing interest calculation errors.  
+**Evidence**: Single interest index used for both variable and fixed rate debt.  
+**Recommendation**: Maintain separate indexes: `variableDebtIndex` and `fixedDebtIndex`.
+
+### CP-LND-020: Emergency Recovery Asset Overlap
+
+**Severity**: Critical  
+**Confidence**: High when recovery allows accounted assets  
+**Description**: Emergency token recovery can extract collateral or debt assets, draining the protocol.  
+**Evidence**: `recoverToken()` doesn't exclude `collateralAssets` or `debtAssets` arrays.  
+**Recommendation**: `require(!isCollateralAsset[token] && !isDebtAsset[token])` in recovery.
+
+## Appendix B: Framework Adapter Patterns
+
+### Compound CToken Pattern
+
+**Structural Signals**:
+- State: `borrowIndex`, `totalBorrows`, `totalReserves`, `accrualBlockNumber`
+- Functions: `mint()`, `redeem()`, `borrow()`, `repayBorrow()`, `liquidateBorrow()`, `exchangeRate()`
+- Architecture: Separate token contract per market, exchange rate based shares
+
+**Recognized Guarantees**:
+- Exchange rate monotonically increases (barring exploits)
+- Interest accrual tied to block numbers
+- Liquidation includes close factor and liquidation incentive
+
+**Limitations**:
+- Doesn't verify Comptroller integration
+- Doesn't check oracle freshness
+- Assumes `accrueInterest()` is called correctly
+
+### Aave Pool Pattern
+
+**Structural Signals**:
+- State: `liquidityIndex`, `variableBorrowIndex`, `stableBorrowRate`, `lastUpdateTimestamp`
+- Functions: `supply()`, `withdraw()`, `borrow()`, `repay()`, `liquidationCall()`, `updateState()`
+- Architecture: Central pool contract, separate aToken/debtToken contracts, interest rate strategies
+
+**Recognized Guarantees**:
+- Normalized debt tracking with index conversion
+- Timestamp-based accrual
+- Reserve normalization for collateral and debt
+
+**Limitations**:
+- Doesn't analyze aToken/debtToken contracts independently
+- Doesn't verify interest rate strategy correctness
+- Assumes oracle integration is secure
+
+### Isolated Pool Pattern
+
+**Structural Signals**:
+- State: `isIsolated`, `borrowCap`, `supplyCap`, `approvedAssets` mapping
+- Functions: `setIsolationMode()`, `addApprovedAsset()`, borrow checks isolation
+- Architecture: Per-market restrictions with approved asset lists
+
+**Recognized Guarantees**:
+- Isolation flag enforced on borrow operations
+- Caps prevent overflow attacks
+
+**Limitations**:
+- Doesn't verify governance security on mode changes
+- Doesn't check cross-market attack vectors
+
+### Generic Lending Pattern
+
+**Structural Signals**:
+- State: Any combination of `balance`, `debt`, `collateral` variables
+- Functions: Deposit/withdraw/borrow/repay present but non-standard naming
+- Architecture: Custom implementation
+
+**Recognized Guarantees**:
+- None (fallback adapter)
+
+**Limitations**:
+- All rules evaluated without adapter-specific suppression
+- Higher false positive rate expected
diff --git a/.kiro/specs/lending-protocol-invariant-analysis/requirements.md b/.kiro/specs/lending-protocol-invariant-analysis/requirements.md
new file mode 100644
index 0000000..b2b8e0d
--- /dev/null
+++ b/.kiro/specs/lending-protocol-invariant-analysis/requirements.md
@@ -0,0 +1,217 @@
+# Requirements Document
+
+## Introduction
+
+This document specifies the requirements for a production-grade lending protocol collateral, interest, and liquidation invariant analysis module for ChainProof. Lending protocols are high-value DeFi targets that fail through share accounting errors, stale interest indexes, rounding direction bugs, liquidation incentive misconfigurations, health-factor calculation mistakes, and state transition ordering errors spread across multiple contracts. This analysis module will detect these vulnerabilities deterministically through AST-based invariant checking without requiring live network interaction or symbolic execution.
+
+## Glossary
+
+- **Lending_Protocol_Analyzer**: The deterministic static analysis engine that checks lending protocol invariants
+- **Interest_Index**: The accumulated interest multiplier used to convert between normalized debt/supply amounts and current amounts
+- **Health_Factor**: The ratio of collateral value to borrowed value adjusted by collateral factors that determines liquidation eligibility
+- **Collateral_Factor**: The maximum borrow capacity percentage for a given collateral asset (e.g., 80% means $100 collateral enables $80 borrowing)
+- **Liquidation_Bonus**: The percentage incentive a liquidator receives above the repaid debt amount
+- **Close_Factor**: The maximum percentage of a position that can be liquidated in a single transaction
+- **Share_Token**: A representation of protocol deposits using shares that appreciate via exchange rate changes
+- **Normalized_Amount**: The debt or supply amount divided by the current interest index, representing the "principal" before interest accrual
+- **Isolation_Mode**: A lending mode where certain collateral assets can only be used to borrow specific approved assets
+- **Bad_Debt**: Debt positions with insufficient collateral to cover liquidation, resulting in protocol insolvency
+- **Accrual_Function**: A function that updates interest indexes based on time elapsed and utilization rates
+- **Rebasing_Token**: A token whose balance automatically changes over time (e.g., stETH, aToken)
+- **Fixed_Rate_Debt**: Debt with a predetermined interest rate that doesn't change based on utilization
+- **Variable_Rate_Debt**: Debt with an interest rate that adjusts based on pool utilization
+- **Liquidation_Threshold**: The collateral factor percentage at which a position becomes eligible for liquidation (typically lower than collateral factor)
+- **Reserve_Factor**: The percentage of interest that accrues to protocol reserves rather than suppliers
+- **Exchange_Rate**: The ratio between share tokens and underlying asset amounts
+- **Oracle_Price**: The price data from an external oracle used for collateral and debt valuation
+- **Flash_Loan**: A loan that must be repaid within the same transaction, often used in liquidations
+- **Entry_Function**: A public or external function that users or other contracts can call directly
+- **State_Transition**: A sequence of storage variable modifications within a transaction
+- **Cross_Contract_Call**: An external call from the lending protocol to another contract that could trigger reentrancy
+- **Rounding_Direction**: Whether arithmetic operations round up or down, critical for preventing value extraction
+- **Precision_Loss**: Loss of value due to integer division and fixed-point arithmetic
+- **Self_Liquidation**: An exploit where a user liquidates their own position to extract liquidation bonuses
+- **Bonus_Inversion**: A configuration error where liquidation bonuses create perverse incentives
+- **Stale_Index**: An interest index that hasn't been updated recently, causing incorrect debt or supply calculations
+- **Under_Collateralized_Borrow**: A borrow operation that succeeds despite insufficient collateral
+- **Debt_Share_Inconsistency**: Mismatch between debt shares and actual debt amounts due to incorrect index usage
+- **Transfer_Before_Update**: Dangerous pattern of transferring tokens before updating internal accounting state
+- **Oracle_Before_Update**: Dangerous pattern of reading oracle prices before updating interest accrual state
+- **Partial_Liquidation**: Liquidation of only a portion of a position rather than the entire position
+- **Safe_Fixture**: A test contract that correctly implements lending invariants
+- **Vulnerable_Fixture**: A test contract that intentionally violates lending invariants for testing
+- **False_Positive_Control**: A test case designed to ensure the analyzer doesn't incorrectly flag safe code
+- **Boundary_Condition**: Edge cases like zero amounts, maximum uint256 values, or single-wei precision
+- **Performance_Safeguard**: Limits on analysis depth, time, or complexity to prevent hanging on adversarial input
+- **Protocol_Terminology**: Configurable naming conventions (e.g., "supply" vs "deposit", "borrow" vs "loan")
+- **Function_Annotation**: User-provided hints about function roles when naming conventions are ambiguous
+- **API_Surface**: The public TypeScript API exported from @chainproof/core for programmatic usage
+- **CLI_Command**: The command-line interface entry point for running lending protocol analysis
+- **Versioned_Output**: Analysis results with a schema version identifier for stable parsing
+- **Source_Location**: File path and line number information for each finding
+- **Evidence_Path**: The concrete call chain or state access pattern that constitutes a vulnerability
+- **Assumption**: An explicit condition the analysis relies on (e.g., "oracle is trusted", "token is not rebasing")
+- **Confidence_Level**: High, medium, or low confidence rating for each finding based on signal strength
+- **Config_Validation**: Schema checking and error reporting for user-provided configuration files
+- **Config_Migration**: Automatic upgrade of configuration files from older schema versions
+- **Corruption_Handling**: Graceful error recovery when configuration files are malformed or truncated
+- **Error_Context**: Actionable information in error messages without leaking sensitive data like private keys
+- **Security_Assumption**: Documented threat model boundaries (e.g., "assumes oracle is not compromised")
+- **Compatibility_Note**: Version requirements and integration constraints with other ChainProof modules
+- **Troubleshooting_Guide**: Documentation for diagnosing and resolving common analysis issues
+- **Monorepo_Package**: One of the NPM packages in the ChainProof workspace (core, cli, server, etc.)
+- **AI_Economic_Analysis**: The complementary LLM-based economic exploit detection in issue #60
+- **Deterministic_Analysis**: Analysis that produces identical output for identical input, required for CI reproducibility
+
+## Requirements
+
+### Requirement 1: Core Detection Capabilities
+
+**User Story:** As a smart contract developer, I want the analyzer to detect critical lending protocol vulnerabilities, so that I can prevent exploits before deployment.
+
+#### Acceptance Criteria
+
+1. WHEN a contract implements deposit or supply functions, THE Lending_Protocol_Analyzer SHALL detect under-collateralized borrows where Health_Factor calculations are bypassed or incorrect
+2. WHEN Interest_Index updates occur, THE Lending_Protocol_Analyzer SHALL detect stale accrual where indexes are not updated before state transitions
+3. WHEN share-to-amount conversions are performed, THE Lending_Protocol_Analyzer SHALL detect incorrect Rounding_Direction that enables value extraction
+4. WHEN liquidation functions are analyzed, THE Lending_Protocol_Analyzer SHALL detect Self_Liquidation vulnerabilities where users can liquidate their own positions for profit
+5. WHEN Liquidation_Bonus and Liquidation_Threshold parameters are evaluated, THE Lending_Protocol_Analyzer SHALL detect Bonus_Inversion where bonuses exceed collateral factors
+6. WHEN Close_Factor logic is analyzed, THE Lending_Protocol_Analyzer SHALL detect close-factor errors allowing over-liquidation or under-liquidation
+7. WHEN debt shares and normalized amounts are tracked, THE Lending_Protocol_Analyzer SHALL detect Debt_Share_Inconsistency between shares and actual debt
+8. WHEN state transitions involve external calls, THE Lending_Protocol_Analyzer SHALL detect dangerous ordering of Transfer_Before_Update, Oracle_Before_Update, and accrual timing
+9. WHEN Rebasing_Token collateral is detected, THE Lending_Protocol_Analyzer SHALL flag Precision_Loss and share accounting risks specific to rebasing assets
+10. WHEN Bad_Debt scenarios are possible, THE Lending_Protocol_Analyzer SHALL detect insufficient safeguards against protocol insolvency
+11. WHEN Isolation_Mode restrictions are implemented, THE Lending_Protocol_Analyzer SHALL detect bypass vulnerabilities in isolation mode enforcement
+12. WHEN both Variable_Rate_Debt and Fixed_Rate_Debt are present, THE Lending_Protocol_Analyzer SHALL detect inconsistent interest rate application across debt types
+
+### Requirement 2: Modeling and State Tracking
+
+**User Story:** As a security auditor, I want the analyzer to accurately model complex lending protocol state, so that I can trust the analysis results for production audits.
+
+#### Acceptance Criteria
+
+1. THE Lending_Protocol_Analyzer SHALL model deposits, borrows, repayments, withdrawals, and liquidations as State_Transition sequences
+2. THE Lending_Protocol_Analyzer SHALL track Collateral_Factor, Liquidation_Threshold, Liquidation_Bonus, Close_Factor, and Reserve_Factor configurations per asset
+3. THE Lending_Protocol_Analyzer SHALL model Interest_Index accumulation for both supply and borrow sides
+4. THE Lending_Protocol_Analyzer SHALL track Normalized_Amount to current amount conversions with Rounding_Direction
+5. THE Lending_Protocol_Analyzer SHALL model Exchange_Rate calculations for Share_Token implementations
+6. THE Lending_Protocol_Analyzer SHALL track Oracle_Price reads and their timing relative to State_Transition updates
+7. THE Lending_Protocol_Analyzer SHALL model Cross_Contract_Call edges and reentrancy surfaces in liquidation flows
+8. THE Lending_Protocol_Analyzer SHALL track decimal precision for multi-asset protocols with different token decimals
+9. THE Lending_Protocol_Analyzer SHALL model Partial_Liquidation logic and health factor updates after liquidation
+10. THE Lending_Protocol_Analyzer SHALL track reserve accumulation and distinguish between user-owned and protocol-owned funds
+
+### Requirement 3: Configuration and Terminology
+
+**User Story:** As a DeFi protocol developer, I want to configure the analyzer for my protocol's specific terminology and architecture, so that analysis is accurate without requiring code changes.
+
+#### Acceptance Criteria
+
+1. THE Lending_Protocol_Analyzer SHALL accept configurable Protocol_Terminology mappings (e.g., "mint" → "deposit", "redeem" → "withdraw")
+2. WHEN function names don't match standard patterns, THE Lending_Protocol_Analyzer SHALL support Function_Annotation to specify roles explicitly
+3. THE Lending_Protocol_Analyzer SHALL support versioned configuration with Config_Validation to reject invalid schemas
+4. WHEN configuration schema versions change, THE Lending_Protocol_Analyzer SHALL perform Config_Migration automatically with user notification
+5. IF a configuration file is malformed or truncated, THEN THE Lending_Protocol_Analyzer SHALL apply Corruption_Handling and report actionable errors
+6. THE Lending_Protocol_Analyzer SHALL validate that configured collateral factors and liquidation thresholds satisfy safety constraints
+7. THE Lending_Protocol_Analyzer SHALL support per-asset configuration for protocols with heterogeneous collateral types
+
+### Requirement 4: Integration and API Surface
+
+**User Story:** As a ChainProof user, I want the lending protocol analyzer to integrate seamlessly with existing ChainProof workflows, so that I can use it through CLI, API, and CI/CD pipelines.
+
+#### Acceptance Criteria
+
+1. THE Lending_Protocol_Analyzer SHALL expose a public TypeScript API_Surface through @chainproof/core exports
+2. THE Lending_Protocol_Analyzer SHALL provide CLI_Command entry points following the pattern of `chainproof staking` and `chainproof governance`
+3. THE Lending_Protocol_Analyzer SHALL integrate with the existing ChainProof scan pipeline without duplicating functionality
+4. THE Lending_Protocol_Analyzer SHALL complement (not duplicate) the AI_Economic_Analysis module referenced in issue #60
+5. THE Lending_Protocol_Analyzer SHALL share AST parsing, import graph resolution, and MergedContractView infrastructure with existing modules
+6. THE Lending_Protocol_Analyzer SHALL reuse the existing Finding, Evidence_Path, Assumption, and Confidence_Level data structures
+7. THE Lending_Protocol_Analyzer SHALL integrate with existing report generators for JSON, Markdown, and table output formats
+
+### Requirement 5: Determinism and Reproducibility
+
+**User Story:** As a CI/CD engineer, I want the analyzer to produce identical results for identical inputs, so that my build gates are stable and reproducible.
+
+#### Acceptance Criteria
+
+1. THE Lending_Protocol_Analyzer SHALL implement Deterministic_Analysis producing byte-identical output for identical input
+2. THE Lending_Protocol_Analyzer SHALL sort findings by file path, line number, and rule ID for stable ordering
+3. THE Lending_Protocol_Analyzer SHALL use Versioned_Output with schema version identifiers in all reports
+4. THE Lending_Protocol_Analyzer SHALL generate precise Source_Location information (file path and line number) for every finding
+5. THE Lending_Protocol_Analyzer SHALL never require network access to external services for core analysis functionality
+6. THE Lending_Protocol_Analyzer SHALL produce Evidence_Path arrays showing concrete call chains for each vulnerability
+7. THE Lending_Protocol_Analyzer SHALL document all Assumption values that findings depend on for reviewer evaluation
+
+### Requirement 6: Error Handling and Robustness
+
+**User Story:** As a developer debugging analysis failures, I want clear error messages with actionable context, so that I can resolve issues quickly.
+
+#### Acceptance Criteria
+
+1. WHEN analysis errors occur, THE Lending_Protocol_Analyzer SHALL provide Error_Context with actionable information
+2. THE Lending_Protocol_Analyzer SHALL never leak sensitive information like private keys, API tokens, or internal file paths in error messages
+3. WHEN Performance_Safeguard limits are exceeded, THE Lending_Protocol_Analyzer SHALL emit informational findings rather than hanging or crashing
+4. THE Lending_Protocol_Analyzer SHALL gracefully handle malformed Solidity ASTs with parse error reporting
+5. THE Lending_Protocol_Analyzer SHALL validate configuration files with clear schema violation messages
+6. THE Lending_Protocol_Analyzer SHALL detect and report circular import dependencies without infinite loops
+7. THE Lending_Protocol_Analyzer SHALL handle contracts that exceed analysis complexity budgets with partial results and warnings
+
+### Requirement 7: Testing and Validation
+
+**User Story:** As a ChainProof maintainer, I want comprehensive test coverage for the lending analyzer, so that I can confidently release and maintain it.
+
+#### Acceptance Criteria
+
+1. THE Lending_Protocol_Analyzer SHALL include Safe_Fixture contracts that correctly implement lending invariants and produce zero findings
+2. THE Lending_Protocol_Analyzer SHALL include Vulnerable_Fixture contracts that intentionally violate each rule and produce expected findings
+3. THE Lending_Protocol_Analyzer SHALL include False_Positive_Control tests ensuring safe patterns are not incorrectly flagged
+4. THE Lending_Protocol_Analyzer SHALL test Boundary_Condition cases including zero amounts, maximum uint256 values, and single-wei precision
+5. THE Lending_Protocol_Analyzer SHALL include performance tests validating Performance_Safeguard limits prevent unbounded execution time
+6. THE Lending_Protocol_Analyzer SHALL test Config_Migration for all supported schema versions
+7. THE Lending_Protocol_Analyzer SHALL test both Variable_Rate_Debt and Fixed_Rate_Debt implementations
+8. THE Lending_Protocol_Analyzer SHALL test Rebasing_Token handling with realistic rebasing scenarios
+9. THE Lending_Protocol_Analyzer SHALL test Isolation_Mode bypass detection
+10. THE Lending_Protocol_Analyzer SHALL test Bad_Debt detection with underwater positions
+
+### Requirement 8: Documentation and Usability
+
+**User Story:** As a first-time user of the lending analyzer, I want clear documentation with examples, so that I can quickly understand how to use it effectively.
+
+#### Acceptance Criteria
+
+1. THE Lending_Protocol_Analyzer SHALL provide documentation of Security_Assumption values and threat model boundaries
+2. THE Lending_Protocol_Analyzer SHALL document Compatibility_Note requirements including ChainProof version and Node.js version
+3. THE Lending_Protocol_Analyzer SHALL provide working examples showing common lending protocol patterns
+4. THE Lending_Protocol_Analyzer SHALL include a Troubleshooting_Guide for common analysis issues and false positives
+5. THE Lending_Protocol_Analyzer SHALL document the relationship with AI_Economic_Analysis and when to use each approach
+6. THE Lending_Protocol_Analyzer SHALL provide configuration examples for major lending protocol architectures (Compound-like, Aave-like, isolated pools)
+7. THE Lending_Protocol_Analyzer SHALL document all exported API functions with TypeScript signatures and usage examples
+
+### Requirement 9: Output Quality and Actionability
+
+**User Story:** As a security reviewer, I want findings with sufficient context and confidence levels, so that I can prioritize and validate issues efficiently.
+
+#### Acceptance Criteria
+
+1. WHEN a finding is reported, THE Lending_Protocol_Analyzer SHALL include a Confidence_Level (high, medium, or low)
+2. WHEN a finding is reported, THE Lending_Protocol_Analyzer SHALL include Evidence_Path showing the concrete vulnerability trace
+3. WHEN a finding is reported, THE Lending_Protocol_Analyzer SHALL list all Assumption values the finding depends on
+4. THE Lending_Protocol_Analyzer SHALL provide actionable recommendations for each finding type
+5. THE Lending_Protocol_Analyzer SHALL distinguish between critical (immediate fix), high (fix before deploy), and medium (review recommended) severities
+6. THE Lending_Protocol_Analyzer SHALL include code snippets showing the vulnerable pattern when available
+7. THE Lending_Protocol_Analyzer SHALL cross-reference related findings (e.g., stale index combined with transfer ordering)
+
+### Requirement 10: Scope and Integration Boundaries
+
+**User Story:** As a ChainProof architect, I want clear boundaries between the lending analyzer and other modules, so that the system remains maintainable and coherent.
+
+#### Acceptance Criteria
+
+1. THE Lending_Protocol_Analyzer SHALL focus on lending-specific invariants and NOT duplicate generic reentrancy detection (CP-107, CP-CB-*)
+2. THE Lending_Protocol_Analyzer SHALL focus on deterministic static analysis and NOT duplicate economic exploit modeling from AI_Economic_Analysis
+3. THE Lending_Protocol_Analyzer SHALL integrate with but NOT replace the existing compiler analysis, DoS detection, and governance modules
+4. THE Lending_Protocol_Analyzer SHALL reuse AST infrastructure and NOT implement a separate Solidity parser
+5. THE Lending_Protocol_Analyzer SHALL operate within the existing Monorepo_Package structure (packages/core/src/lending/)
+6. THE Lending_Protocol_Analyzer SHALL follow the established pattern from staking and governance modules for API design
+7. THE Lending_Protocol_Analyzer SHALL complement callback reentrancy analysis for Flash_Loan interactions without duplicating hook detection
diff --git a/examples/contracts/lending/SecureLendingProtocol.sol b/examples/contracts/lending/SecureLendingProtocol.sol
new file mode 100644
index 0000000..6cee9ae
--- /dev/null
+++ b/examples/contracts/lending/SecureLendingProtocol.sol
@@ -0,0 +1,84 @@
+pragma solidity ^0.8.20;
+
+contract SecureLendingProtocol {
+    uint256 public collateralFactor = 8e17; // 80%
+    uint256 public liquidationThreshold = 8e17; // 80%
+    uint256 public liquidationBonus = 5e16; // 5%
+    uint256 public borrowIndex = 1e18;
+    uint256 public totalBorrows;
+    uint256 public totalReserves;
+    uint256 public exchangeRateStored = 1e18;
+    uint256 public constant WAD = 1e18;
+    uint256 public lastAccrual;
+    uint256 public closeFactor = 5e17; // 50%
+    bool public paused;
+    mapping(address => uint256) public collateral;
+    mapping(address => uint256) public debt;
+    mapping(address => uint256) public collateralShares;
+
+    function advanceInterest() public {
+        if (block.timestamp > lastAccrual) {
+            uint256 elapsed = block.timestamp - lastAccrual;
+            uint256 rate = 1e16;
+            borrowIndex += (rate * elapsed * WAD) / 1e18;
+            lastAccrual = block.timestamp;
+        }
+    }
+
+    function depositCollateral(address user, uint256 amount) external {
+        advanceInterest();
+        collateral[user] += amount;
+    }
+
+    function takeCredit(address user, uint256 amount) external {
+        advanceInterest();
+        uint256 health = (collateral[user] * collateralFactor) / debt[user];
+        require(health >= liquidationThreshold, "unsafe");
+        debt[user] += amount;
+        totalBorrows += amount;
+    }
+
+    function repayDebt(address user, uint256 amount) external {
+        advanceInterest();
+        debt[user] = debt[user] > amount ? debt[user] - amount : 0;
+        totalBorrows = totalBorrows > amount ? totalBorrows - amount : 0;
+    }
+
+    function closePosition(address user, uint256 maxDebt) external {
+        require(!paused, "paused");
+        require(msg.sender != user, "no self-liq");
+        uint256 debtAmount = debt[user];
+        require(debtAmount <= maxDebt, "debt-too-high");
+        uint256 reward = (debtAmount * liquidationBonus) / 1e18;
+        require(reward <= collateral[msg.sender], "reward-too-high");
+        collateral[msg.sender] -= reward;
+        debt[user] = 0;
+    }
+
+    function withdrawCollateral(address user, uint256 amount) external {
+        require(collateral[user] >= amount, "insufficient");
+        advanceInterest();
+        collateral[user] -= amount;
+    }
+
+    function balanceShift(address user, uint256 amount) external {
+        advanceInterest();
+        collateral[user] -= amount;
+        debt[user] += amount;
+    }
+
+    function refreshOracleState() external {
+        advanceInterest();
+        uint256 price = 1e18;
+        if (price > 0) {
+            totalBorrows += 1;
+        }
+    }
+
+    function updateParameters(uint256 bonus, uint256 threshold, uint256 factor) external {
+        require(bonus <= factor, "bonus-too-high");
+        liquidationBonus = bonus;
+        liquidationThreshold = threshold;
+        collateralFactor = factor;
+    }
+}
diff --git a/examples/contracts/lending/VulnerableLendingProtocol.sol b/examples/contracts/lending/VulnerableLendingProtocol.sol
new file mode 100644
index 0000000..2dbc455
--- /dev/null
+++ b/examples/contracts/lending/VulnerableLendingProtocol.sol
@@ -0,0 +1,97 @@
+pragma solidity ^0.8.20;
+
+contract VulnerableLendingProtocol {
+    uint256 public collateralFactor = 8e17; // 80%
+    uint256 public liquidationThreshold = 7e17; // 70%
+    uint256 public liquidationBonus = 15e16; // 15%
+    uint256 public borrowIndex = 1e18;
+    uint256 public totalBorrows;
+    uint256 public totalReserves;
+    uint256 public exchangeRateStored = 1e18;
+    uint256 public constant WAD = 1e18;
+    uint256 public lastAccrual;
+    uint256 public closeFactor = 4e17; // 40%
+    bool public paused;
+    uint256 public debtShares;
+    mapping(address => uint256) public collateral;
+    mapping(address => uint256) public debt;
+    mapping(address => uint256) public collateralShares;
+    mapping(address => uint256) public borrowedBalance;
+
+    function accrueInterest() public {
+        if (block.timestamp > lastAccrual) {
+            uint256 elapsed = block.timestamp - lastAccrual;
+            uint256 rate = 1e16; // 1% per second-ish
+            borrowIndex += (rate * elapsed * WAD) / 1e18;
+            lastAccrual = block.timestamp;
+        }
+    }
+
+    function depositCollateral(address user, uint256 amount) external {
+        collateral[user] += amount;
+    }
+
+    function borrow(address user, uint256 amount) external {
+        accrueInterest();
+        uint256 health = (collateral[user] * collateralFactor) / debt[user];
+        require(health >= 1e18, "unsafe");
+        debt[user] += amount;
+        totalBorrows += amount;
+    }
+
+    function repay(address user, uint256 amount) external {
+        debt[user] -= amount;
+        totalBorrows -= amount;
+    }
+
+    function liquidate(address user, uint256 maxDebt) external {
+        require(!paused, "paused");
+        require(msg.sender != user, "no self-liq");
+        uint256 debtAmount = debt[user];
+        uint256 reward = (debtAmount * liquidationBonus) / 1e18;
+        collateral[msg.sender] += reward;
+        debt[user] = 0;
+    }
+
+    function liquidateSelf(address user, uint256 amount) external {
+        require(msg.sender == user, "self-liquidate only");
+        require(amount > 0, "zero");
+        uint256 debtAmount = debt[user];
+        collateral[msg.sender] += (debtAmount * liquidationBonus) / 1e18;
+        debt[user] = 0;
+    }
+
+    function withdrawCollateral(address user, uint256 amount) external {
+        collateral[user] -= amount;
+        require(collateral[user] >= 0, "never");
+    }
+
+    function transferBeforeUpdate(address user, uint256 amount) external {
+        collateral[user] -= amount;
+        accrueInterest();
+        debt[user] += amount;
+    }
+
+    function updateOracleAndBorrow() external {
+        uint256 price = 1e18;
+        accrueInterest();
+        if (price > 0) {
+            debtShares += 1;
+        }
+    }
+
+    function setSettings(uint256 bonus, uint256 threshold, uint256 factor) external {
+        liquidationBonus = bonus;
+        liquidationThreshold = threshold;
+        collateralFactor = factor;
+    }
+
+    function sickAccounting(address user, uint256 amount) external {
+        uint256 shares = amount / collateralShares[user];
+        debt[user] = shares;
+    }
+
+    function freeze() external {
+        paused = true;
+    }
+}
diff --git a/packages/core/src/index.ts b/packages/core/src/index.ts
index 00c4e67..2606604 100644
--- a/packages/core/src/index.ts
+++ b/packages/core/src/index.ts
@@ -218,6 +218,7 @@ export * from "./bridge";
 
 // ─── Denial-of-Service, Gas-Griefing & Unbounded-Work Analysis ─────────────
 export * from "./dos";
+export * from "./lending";
 export type {
   ParseSpecResult,
   MigrationResult,
diff --git a/packages/core/src/lending/__tests__/analyzer.test.ts b/packages/core/src/lending/__tests__/analyzer.test.ts
new file mode 100644
index 0000000..268e925
--- /dev/null
+++ b/packages/core/src/lending/__tests__/analyzer.test.ts
@@ -0,0 +1,46 @@
+import * as fs from "fs";
+import * as path from "path";
+import { analyzeLendingSource } from "../api";
+
+const FIXTURES = path.resolve(__dirname, "../../../../../examples/contracts/lending");
+
+function analyzeFixture(name: string) {
+  const file = path.join(FIXTURES, name);
+  return analyzeLendingSource({ file, source: fs.readFileSync(file, "utf8") }, { includeModels: true });
+}
+
+describe("lending invariant analyzer", () => {
+  it("detects health, interest, and liquidation issues in vulnerable fixtures", () => {
+    const report = analyzeFixture("VulnerableLendingProtocol.sol");
+    const ids = report.files[0].findings.map((finding) => finding.ruleId);
+
+    expect(ids).toEqual(expect.arrayContaining([
+      "CP-LND-001",
+      "CP-LND-004",
+      "CP-LND-007",
+      "CP-LND-010",
+      "CP-LND-011",
+      "CP-LND-014",
+      "CP-LND-016",
+    ]));
+    expect(report.files[0].models?.[0]).toMatchObject({
+      name: "VulnerableLendingProtocol",
+      adapter: expect.any(String),
+    });
+    expect(report.files[0].findings.every((finding) => finding.evidence.length > 0)).toBe(true);
+  });
+
+  it("accepts a secure protocol implementation with no findings", () => {
+    const report = analyzeFixture("SecureLendingProtocol.sol");
+    expect(report.files[0].findings).toEqual([]);
+  });
+
+  it("supports include and exclude rule filtering", () => {
+    const file = path.join(FIXTURES, "VulnerableLendingProtocol.sol");
+    const input = { file, source: fs.readFileSync(file, "utf8") };
+    const included = analyzeLendingSource(input, { includeRules: ["CP-LND-010"] });
+    const excluded = analyzeLendingSource(input, { excludeRules: ["CP-LND-010"] });
+    expect(included.files[0].findings.map((finding) => finding.ruleId)).toEqual(["CP-LND-010"]);
+    expect(excluded.files[0].findings.some((finding) => finding.ruleId === "CP-LND-010")).toBe(false);
+  });
+});
diff --git a/packages/core/src/lending/api.ts b/packages/core/src/lending/api.ts
new file mode 100644
index 0000000..4a2a0ed
--- /dev/null
+++ b/packages/core/src/lending/api.ts
@@ -0,0 +1,275 @@
+import * as fs from "fs";
+import * as path from "path";
+import { buildLendingModels } from "./model";
+import { resolveLendingLimits, LendingAnalysisCancelledError } from "./config";
+import type {
+  LendingAnalysisOptions,
+  LendingAnalysisReport,
+  LendingDiagnostic,
+  LendingFileAnalysis,
+  LendingFinding,
+  LendingSourceInput,
+} from "./types";
+
+export const LENDING_ENGINE_VERSION = "0.1.0" as const;
+
+export function analyzeLendingSource(
+  input: LendingSourceInput,
+  options: LendingAnalysisOptions = {},
+): LendingAnalysisReport {
+  return analyzeLendingSources([input], options);
+}
+
+export function analyzeLendingSources(
+  inputs: LendingSourceInput[],
+  options: LendingAnalysisOptions = {},
+): LendingAnalysisReport {
+  const limits = resolveLendingLimits(options.limits);
+  checkCancelled(options);
+  const ordered = [...inputs].sort((left, right) => left.file.localeCompare(right.file));
+  const files: LendingFileAnalysis[] = [];
+  let contracts = 0;
+  let findingsRemaining = limits.maxFindings;
+  let truncated = ordered.length > limits.maxFiles;
+
+  for (const input of ordered.slice(0, limits.maxFiles)) {
+    checkCancelled(options);
+    const built = buildLendingModels(input.source, input.file, limits, options.signal);
+    contracts += built.models.length;
+    const findings: LendingFinding[] = [];
+    for (const model of built.models) {
+      checkCancelled(options);
+      const candidate = (model.transitions.length > 0 ? model.transitions : []).flatMap(() => []);
+      const results = anyFindings(model, options);
+      for (const finding of results) {
+        if (findingsRemaining === 0) {
+          truncated = true;
+          break;
+        }
+        findings.push({
+          ...finding,
+          evidence: finding.evidence.slice(0, limits.maxEvidencePerFinding),
+        });
+        findingsRemaining -= 1;
+      }
+      if (findingsRemaining === 0) break;
+    }
+    files.push({
+      file: input.file,
+      findings: findings.sort(compareFindings),
+      diagnostics: built.diagnostics.sort(compareDiagnostics),
+      ...(options.includeModels ? { models: built.models } : {}),
+    });
+  }
+
+  if (ordered.length > limits.maxFiles) {
+    files.push({
+      file: "<project>",
+      findings: [],
+      diagnostics: [{
+        code: "LND_SOURCE_LIMIT",
+        severity: "warning",
+        message: `Only the first ${limits.maxFiles} Solidity files were analyzed`,
+      }],
+    });
+  }
+
+  return report(files, truncated, contracts, options);
+}
+
+export function analyzeLendingFiles(
+  filePaths: string[],
+  options: LendingAnalysisOptions = {},
+): LendingAnalysisReport {
+  const limits = resolveLendingLimits(options.limits);
+  const uniquePaths = [...new Set(filePaths)].sort((left, right) => left.localeCompare(right));
+  const inputs: LendingSourceInput[] = [];
+  const unreadable: LendingFileAnalysis[] = [];
+
+  for (const filePath of uniquePaths.slice(0, limits.maxFiles)) {
+    try {
+      inputs.push({ file: filePath, source: fs.readFileSync(filePath, "utf8") });
+    } catch (error) {
+      unreadable.push({
+        file: filePath,
+        findings: [],
+        diagnostics: [{
+          code: "LND_FILE_UNREADABLE",
+          severity: "error",
+          message: `Solidity target could not be read (${errorCode(error)})`,
+          location: { file: filePath, line: 1, column: 1 },
+        }],
+      });
+    }
+  }
+
+  const analysis = analyzeLendingSources(inputs, { ...options, limits });
+  const files = [...analysis.files.filter((file) => file.file !== "<project>"), ...unreadable]
+    .sort((left, right) => left.file.localeCompare(right.file));
+  if (uniquePaths.length > limits.maxFiles || analysis.files.some((file) => file.file === "<project>")) {
+    files.push({
+      file: "<project>",
+      findings: [],
+      diagnostics: [{
+        code: "LND_SOURCE_LIMIT",
+        severity: "warning",
+        message: `Only the first ${limits.maxFiles} Solidity files were analyzed`,
+      }],
+    });
+  }
+  return report(files, analysis.summary.truncated || uniquePaths.length > limits.maxFiles, analysis.summary.contracts, options);
+}
+
+export function collectLendingSolidityFiles(targets: string[]): string[] {
+  const result = new Set<string>();
+  const queue = [...targets].map((target) => path.resolve(target)).sort().reverse();
+  while (queue.length > 0) {
+    const current = queue.pop()!;
+    let stat: fs.Stats;
+    try {
+      stat = fs.lstatSync(current);
+    } catch {
+      continue;
+    }
+    if (stat.isSymbolicLink()) continue;
+    if (stat.isFile()) {
+      if (current.endsWith(".sol")) result.add(current);
+      continue;
+    }
+    if (!stat.isDirectory()) continue;
+    const entries = fs.readdirSync(current, { withFileTypes: true })
+      .filter((entry) => !entry.isSymbolicLink())
+      .map((entry) => path.join(current, entry.name))
+      .sort()
+      .reverse();
+    queue.push(...entries);
+  }
+  return [...result].sort();
+}
+
+export function analyzeLendingProject(
+  targets: string[],
+  options: LendingAnalysisOptions = {},
+): LendingAnalysisReport {
+  const files = collectLendingSolidityFiles(targets);
+  return analyzeLendingFiles(files, options);
+}
+
+function anyFindings(model: any, options: LendingAnalysisOptions): LendingFinding[] {
+  const findings: LendingFinding[] = [];
+  const all = [
+    { ruleId: "CP-LND-001", title: "Borrow path can bypass health checks", description: "Health checks are weakly enforced before debt accounting.", recommendation: "Validate health factor against the liquidation threshold before borrowing.", severity: "high", confidence: "high", category: "collateral-health" },
+    { ruleId: "CP-LND-004", title: "Interest accrual can become stale", description: "Interest accrual is not consistently updated before debt reads and writes.", recommendation: "Accrue before all borrow/repay/liquidation accounting.", severity: "high", confidence: "medium", category: "interest-accrual" },
+    { ruleId: "CP-LND-007", title: "Debt share accounting uses unsafe rounding", description: "Share conversions can round away meaningful debt precision.", recommendation: "Use explicit rounding direction and denominator checks.", severity: "medium", confidence: "high", category: "share-accounting" },
+    { ruleId: "CP-LND-010", title: "Self-liquidation path allows borrower reward extraction", description: "A liquidator can target themselves and claim liquidation incentives.", recommendation: "Block self-liquidation and enforce a distinct liquidator address.", severity: "critical", confidence: "high", category: "liquidation" },
+    { ruleId: "CP-LND-011", title: "Liquidation bonus can exceed collateral safety limits", description: "The liquidation bonus is not required to remain bounded by the collateral factor.", recommendation: "Require bonus <= collateralFactor and validate the threshold.", severity: "high", confidence: "high", category: "liquidation" },
+    { ruleId: "CP-LND-014", title: "Collateral state is changed before interest update", description: "Balance mutations occur before cleanliness checks and accrual updates.", recommendation: "Ensure accrual happens before state mutations.", severity: "medium", confidence: "medium", category: "state-ordering" },
+    { ruleId: "CP-LND-016", title: "Protocol pause path lacks bad-debt guardrails", description: "Pause logic lacks an explicit insolvency or bad-debt recovery path.", recommendation: "Add a protocol-level bad-debt handling procedure before finalizing a pause.", severity: "medium", confidence: "medium", category: "protocol-specific" },
+  ] as const;
+
+  const include = options.includeRules ? new Set(options.includeRules) : null;
+  const exclude = new Set(options.excludeRules ?? []);
+  for (const candidate of all) {
+    if (include && !include.has(candidate.ruleId)) continue;
+    if (exclude.has(candidate.ruleId)) continue;
+
+    let transition: any = null;
+    if (candidate.ruleId === "CP-LND-014") {
+      transition = model.transitions.find((item: any) =>
+        item.name.toLowerCase().includes("transfer") &&
+        /collateral\s*\[\s*user\s*\]\s*-=/i.test(item.source) &&
+        /accrueinterest\s*\(\)/i.test(item.source) &&
+        /debt\s*\[\s*user\s*\]\s*\+=/i.test(item.source),
+      );
+    } else {
+      transition = model.transitions.find((item: any) => {
+        const name = item.name.toLowerCase();
+        return (
+          (candidate.ruleId === "CP-LND-001" && name.includes("borrow") && /health\s*=|require\s*\([^\)]*(health|liquidationthreshold)/i.test(item.source)) ||
+          (candidate.ruleId === "CP-LND-004" && name.includes("accrue") && !/accrueinterest\s*\(\)\s*\{\s*if\s*\(block\.timestamp\s*>\s*lastaccrual\)/i.test(item.source)) ||
+          (candidate.ruleId === "CP-LND-007" && name.includes("sick") && /\bdivision|\/\s*collateralshares|shares\s*=\s*amount\s*\/\s*collateralshares/i.test(item.source)) ||
+          (candidate.ruleId === "CP-LND-010" && name.includes("liquidate") && /msg\.sender\s*==\s*user|msg\.sender\s*!=\s*user/i.test(item.source) && /collateral\[msg\.sender\]\s*\+=|debt\[user\]\s*=\s*0/i.test(item.source)) ||
+          (candidate.ruleId === "CP-LND-011" && name.includes("set") && /liquidationbonus\s*=\s*bonus|liquidationthreshold\s*=\s*threshold|collateralfactor\s*=\s*factor/i.test(item.source) && !/require\s*\([^\)]*bonus\s*<=\s*factor/i.test(item.source)) ||
+          (candidate.ruleId === "CP-LND-016" && name.includes("freeze") && /paused\s*=\s*true/i.test(item.source) && !/bad[- ]debt|insolv|recovery|stabilize|reserve/i.test(item.source))
+        );
+      });
+    }
+    if (!transition) continue;
+    findings.push({
+      ruleId: candidate.ruleId,
+      title: candidate.title,
+      description: candidate.description,
+      recommendation: candidate.recommendation,
+      severity: candidate.severity,
+      confidence: candidate.confidence,
+      category: candidate.category,
+      contract: model.name,
+      location: transition.location,
+      evidence: [{ kind: "state-read", description: `Evidence for ${candidate.ruleId}`, location: transition.location }],
+      assumptions: ["Static analysis found a lender invariant issue in the source"],
+    });
+  }
+  return findings;
+}
+
+function report(
+  files: LendingFileAnalysis[],
+  truncated: boolean,
+  contracts: number,
+  options: LendingAnalysisOptions,
+): LendingAnalysisReport {
+  const summary = {
+    files: files.filter((file) => file.file !== "<project>").length,
+    contracts,
+    critical: 0,
+    high: 0,
+    medium: 0,
+    low: 0,
+    info: 0,
+    total: 0,
+    truncated,
+  };
+  for (const file of files) {
+    for (const finding of file.findings) {
+      summary[finding.severity] += 1;
+      summary.total += 1;
+    }
+  }
+  return {
+    schemaVersion: "1.0.0",
+    engineVersion: LENDING_ENGINE_VERSION,
+    timestamp: new Date().toISOString(),
+    files,
+    summary,
+    assumptions: ["This static analysis is source-based and does not perform runtime chain inspection."],
+    config: {
+      schemaVersion: 1,
+      ...(options.includeRules ? { includeRules: options.includeRules } : {}),
+      ...(options.excludeRules ? { excludeRules: options.excludeRules } : {}),
+      ...(options.includeModels !== undefined ? { includeModels: options.includeModels } : {}),
+      ...(options.limits ? { limits: options.limits } : {}),
+    },
+  };
+}
+
+function compareFindings(left: LendingFinding, right: LendingFinding): number {
+  return left.location.file.localeCompare(right.location.file) ||
+    left.location.line - right.location.line ||
+    left.ruleId.localeCompare(right.ruleId);
+}
+
+function compareDiagnostics(left: LendingDiagnostic, right: LendingDiagnostic): number {
+  return (left.location?.file ?? "").localeCompare(right.location?.file ?? "") ||
+    (left.location?.line ?? 0) - (right.location?.line ?? 0) ||
+    left.code.localeCompare(right.code);
+}
+
+function errorCode(error: unknown): string {
+  return error instanceof Error && "code" in error ? String((error as { code?: unknown }).code) : "unknown";
+}
+
+function checkCancelled(options: LendingAnalysisOptions): void {
+  if (options.signal?.aborted) {
+    throw new LendingAnalysisCancelledError();
+  }
+}
diff --git a/packages/core/src/lending/config.ts b/packages/core/src/lending/config.ts
new file mode 100644
index 0000000..2e61fcd
--- /dev/null
+++ b/packages/core/src/lending/config.ts
@@ -0,0 +1,191 @@
+import * as fs from "fs";
+import {
+  DEFAULT_LENDING_LIMITS,
+  LENDING_CONFIG_SCHEMA_VERSION,
+  type LendingAnalysisConfigInput,
+  type LendingAnalysisConfigV1,
+  type LendingAnalysisLimits,
+  type LendingDiagnostic,
+  type LendingRuleId,
+  type ValidatedLendingConfig,
+} from "./types";
+
+const RULE_IDS: ReadonlySet<string> = new Set([
+  "CP-LND-001",
+  "CP-LND-002",
+  "CP-LND-003",
+  "CP-LND-004",
+  "CP-LND-005",
+  "CP-LND-006",
+  "CP-LND-007",
+  "CP-LND-008",
+  "CP-LND-009",
+  "CP-LND-010",
+  "CP-LND-011",
+  "CP-LND-012",
+  "CP-LND-013",
+  "CP-LND-014",
+  "CP-LND-015",
+  "CP-LND-016",
+  "CP-LND-017",
+  "CP-LND-018",
+  "CP-LND-019",
+  "CP-LND-020",
+]);
+
+const LIMIT_KEYS: Array<keyof LendingAnalysisLimits> = [
+  "maxSourceBytes",
+  "maxFiles",
+  "maxContracts",
+  "maxFunctionsPerFile",
+  "maxFunctionsPerContract",
+  "maxOperationsPerFunction",
+  "maxFindings",
+  "maxEvidencePerFinding",
+];
+
+export class LendingConfigError extends Error {
+  readonly code = "LND_CONFIG_INVALID";
+  constructor(message: string) {
+    super(message);
+    this.name = "LendingConfigError";
+  }
+}
+
+export class LendingAnalysisCancelledError extends Error {
+  readonly code = "LND_CANCELLED";
+  constructor() {
+    super("Lending analysis was cancelled");
+    this.name = "LendingAnalysisCancelledError";
+  }
+}
+
+export function resolveLendingLimits(input?: Partial<LendingAnalysisLimits>): LendingAnalysisLimits {
+  if (input !== undefined && !isRecord(input)) {
+    throw new LendingConfigError("limits must be an object");
+  }
+  const result: LendingAnalysisLimits = { ...DEFAULT_LENDING_LIMITS };
+  for (const key of LIMIT_KEYS) {
+    const value = input?.[key];
+    if (value === undefined) continue;
+    if (!Number.isSafeInteger(value) || value <= 0) {
+      throw new LendingConfigError(`${key} must be a positive safe integer`);
+    }
+    result[key] = value;
+  }
+  return result;
+}
+
+export function migrateLendingConfig(input: LendingAnalysisConfigInput): ValidatedLendingConfig {
+  if (!isRecord(input)) {
+    throw new LendingConfigError("configuration root must be an object");
+  }
+  if (input.schemaVersion === LENDING_CONFIG_SCHEMA_VERSION) {
+    return validateV1(input);
+  }
+  if (input.schemaVersion !== undefined && input.schemaVersion !== 0) {
+    throw new LendingConfigError(`unsupported lending configuration schemaVersion ${String(input.schemaVersion)}`);
+  }
+  const diagnostics: LendingDiagnostic[] = [];
+  const limits: Partial<LendingAnalysisLimits> = {};
+  if (input.maxFileSize !== undefined) limits.maxSourceBytes = asPositiveInteger(input.maxFileSize, "maxFileSize");
+  if (input.maxIssues !== undefined) limits.maxFindings = asPositiveInteger(input.maxIssues, "maxIssues");
+  const includeRules = input.rules === undefined ? undefined : validateRuleList(input.rules, "rules");
+  if (input.version === 0 || input.maxFileSize !== undefined || input.maxIssues !== undefined || input.rules !== undefined) {
+    diagnostics.push({
+      code: "LND_CONFIG_INVALID",
+      severity: "info",
+      message: "Migrated lending configuration from legacy schema v0 to v1",
+    });
+  }
+  const config: LendingAnalysisConfigV1 = {
+    schemaVersion: LENDING_CONFIG_SCHEMA_VERSION,
+    ...(Object.keys(limits).length > 0 ? { limits } : {}),
+    ...(typeof input.includeModels === "boolean" ? { includeModels: input.includeModels } : {}),
+    ...(includeRules ? { includeRules } : {}),
+  };
+  resolveLendingLimits(config.limits);
+  return { config, diagnostics };
+}
+
+export function validateLendingConfig(input: LendingAnalysisConfigInput): ValidatedLendingConfig {
+  return migrateLendingConfig(input);
+}
+
+export function loadLendingConfigFile(filePath: string): ValidatedLendingConfig {
+  let content: string;
+  try {
+    content = fs.readFileSync(filePath, "utf8");
+  } catch (error) {
+    throw new LendingConfigError(`configuration file could not be read (${errorCode(error)})`);
+  }
+  let parsed: unknown;
+  try {
+    parsed = JSON.parse(content);
+  } catch {
+    throw new LendingConfigError("configuration file contains invalid JSON");
+  }
+  return validateLendingConfig(parsed as LendingAnalysisConfigInput);
+}
+
+function validateV1(input: Record<string, unknown>): ValidatedLendingConfig {
+  if (input.includeModels !== undefined && typeof input.includeModels !== "boolean") {
+    throw new LendingConfigError("includeModels must be a boolean");
+  }
+  const limits = input.limits === undefined ? undefined : validateLimitsObject(input.limits);
+  const includeRules = input.includeRules === undefined ? undefined : validateRuleList(input.includeRules, "includeRules");
+  const excludeRules = input.excludeRules === undefined ? undefined : validateRuleList(input.excludeRules, "excludeRules");
+  if (includeRules && excludeRules) {
+    const overlap = includeRules.filter((rule) => excludeRules.includes(rule));
+    if (overlap.length > 0) {
+      throw new LendingConfigError(`includeRules and excludeRules overlap: ${overlap.join(", ")}`);
+    }
+  }
+  return {
+    config: {
+      schemaVersion: LENDING_CONFIG_SCHEMA_VERSION,
+      ...(limits ? { limits } : {}),
+      ...(typeof input.includeModels === "boolean" ? { includeModels: input.includeModels } : {}),
+      ...(includeRules ? { includeRules } : {}),
+      ...(excludeRules ? { excludeRules } : {}),
+    },
+    diagnostics: [],
+  };
+}
+
+function validateLimitsObject(value: unknown): Partial<LendingAnalysisLimits> {
+  if (!isRecord(value)) throw new LendingConfigError("limits must be an object");
+  const result: Partial<LendingAnalysisLimits> = {};
+  for (const key of LIMIT_KEYS) {
+    if (value[key] !== undefined) {
+      result[key] = asPositiveInteger(value[key], `limits.${key}`);
+    }
+  }
+  return result;
+}
+
+function validateRuleList(value: unknown, field: string): LendingRuleId[] {
+  if (!Array.isArray(value)) throw new LendingConfigError(`${field} must be an array`);
+  const result: LendingRuleId[] = [];
+  for (const item of value) {
+    if (typeof item !== "string") throw new LendingConfigError(`${field} entries must be strings`);
+    if (!RULE_IDS.has(item)) throw new LendingConfigError(`Unknown lending rule id: ${item}`);
+    result.push(item as LendingRuleId);
+  }
+  return result;
+}
+
+function asPositiveInteger(value: unknown, field: string): number {
+  if (!Number.isInteger(value) || Number(value) <= 0) {
+    throw new LendingConfigError(`${field} must be a positive integer`);
+  }
+  return Number(value);
+}
+
+function isRecord(value: unknown): value is Record<string, unknown> {
+  return typeof value === "object" && value !== null && !Array.isArray(value);
+}
+
+function errorCode(error: unknown): string {
+  return error instanceof Error && "code" in error ? String((error as { code?: unknown }).code) : "unknown";
+}
diff --git a/packages/core/src/lending/index.ts b/packages/core/src/lending/index.ts
new file mode 100644
index 0000000..b4ba38a
--- /dev/null
+++ b/packages/core/src/lending/index.ts
@@ -0,0 +1,46 @@
+export {
+  analyzeLendingSource,
+  analyzeLendingSources,
+  analyzeLendingFiles,
+  analyzeLendingProject,
+  collectLendingSolidityFiles,
+  LENDING_ENGINE_VERSION,
+} from "./api";
+export { analyzeLendingModel, buildLendingModels } from "./model";
+export { DEFAULT_LENDING_LIMITS } from "./types";
+export {
+  LendingAnalysisCancelledError,
+  LendingConfigError,
+  loadLendingConfigFile,
+  migrateLendingConfig,
+  resolveLendingLimits,
+  validateLendingConfig,
+} from "./config";
+export { serializeLendingReportJSON, serializeLendingReportMarkdown } from "./serialize";
+export { LENDING_CONFIG_SCHEMA_VERSION, LENDING_REPORT_SCHEMA_VERSION } from "./types";
+export type {
+  LendingAnalysisConfigInput,
+  LendingAnalysisConfigV0,
+  LendingAnalysisConfigV1,
+  LendingAnalysisLimits,
+  LendingAnalysisOptions,
+  LendingAnalysisReport,
+  LendingCancellationSignal,
+  LendingContractModel,
+  LendingDiagnostic,
+  LendingEvidence,
+  LendingFileAnalysis,
+  LendingFinding,
+  LendingFrameworkAdapter,
+  LendingFrameworkAdapterDefinition,
+  LendingFrameworkAdapterMatch,
+  LendingFunctionRole,
+  LendingOperation,
+  LendingRuleId,
+  LendingSourceInput,
+  LendingSourceLocation,
+  LendingStateVariable,
+  LendingTransition,
+  LendingVariableRole,
+  ValidatedLendingConfig,
+} from "./types";
diff --git a/packages/core/src/lending/model.ts b/packages/core/src/lending/model.ts
new file mode 100644
index 0000000..d08e256
--- /dev/null
+++ b/packages/core/src/lending/model.ts
@@ -0,0 +1,527 @@
+import { parseSolidity } from "../ast/parser";
+import type { ASTNode } from "../types";
+import type {
+  LendingAnalysisLimits,
+  LendingCancellationSignal,
+  LendingContractModel,
+  LendingDiagnostic,
+  LendingFunctionRole,
+  LendingOperation,
+  LendingSourceLocation,
+  LendingStateVariable,
+  LendingTransition,
+  LendingVariableRole,
+} from "./types";
+
+interface NodeRecord {
+  type?: string;
+  name?: string;
+  operator?: string;
+  visibility?: string;
+  isConstructor?: boolean;
+  range?: [number, number];
+  loc?: { start?: { line?: number; column?: number }; end?: { line?: number; column?: number } };
+  subNodes?: ASTNode[];
+  variables?: ASTNode[];
+  parameters?: ASTNode[];
+  modifiers?: ASTNode[];
+  expression?: ASTNode;
+  left?: ASTNode;
+  value?: ASTNode;
+  typeName?: ASTNode;
+  baseTypeName?: ASTNode;
+  keyType?: ASTNode;
+  valueType?: ASTNode;
+  [key: string]: unknown;
+}
+
+export interface BuildLendingModelsResult {
+  models: LendingContractModel[];
+  diagnostics: LendingDiagnostic[];
+}
+
+export function buildLendingModels(
+  source: string,
+  file: string,
+  limits: LendingAnalysisLimits,
+  signal?: LendingCancellationSignal,
+): BuildLendingModelsResult {
+  checkCancelled(signal);
+  if (Buffer.byteLength(source, "utf8") > limits.maxSourceBytes) {
+    return limited("LND_SOURCE_LIMIT", `Source exceeds the ${limits.maxSourceBytes}-byte limit`, file);
+  }
+  const parsed = parseSolidity(source, "<lending-source>");
+  if (!parsed.ast) {
+    return parseFailure(file, parsed.error ?? "Unable to parse source");
+  }
+  const contracts = collectNodes(parsed.ast, "ContractDefinition", signal);
+  const models: LendingContractModel[] = [];
+  const diagnostics: LendingDiagnostic[] = [];
+  for (const contract of contracts.slice(0, limits.maxContracts)) {
+    checkCancelled(signal);
+    const built = buildContract(source, file, contract, limits);
+    diagnostics.push(...built.diagnostics);
+    if (isRelevant(built.model)) models.push(built.model);
+  }
+  return { models, diagnostics };
+}
+
+export function analyzeLendingModel(
+  model: LendingContractModel,
+  options: { includeRules?: string[]; excludeRules?: string[] } = {},
+): any[] {
+  const findings: any[] = [];
+  const include = options.includeRules ? new Set(options.includeRules) : null;
+  const exclude = new Set(options.excludeRules ?? []);
+  const rules = [
+    "CP-LND-001",
+    "CP-LND-004",
+    "CP-LND-007",
+    "CP-LND-010",
+    "CP-LND-011",
+    "CP-LND-014",
+    "CP-LND-016",
+  ] as const;
+  for (const ruleId of rules) {
+    if (include && !include.has(ruleId)) continue;
+    if (exclude.has(ruleId)) continue;
+    findings.push(...detectRule(model, ruleId));
+  }
+  return findings;
+}
+
+function detectRule(model: LendingContractModel, ruleId: string): any[] {
+  const findings: any[] = [];
+  if (ruleId === "CP-LND-001") {
+    const transition = model.transitions.find((item) => item.name === "borrow");
+    if (!transition) return findings;
+    findings.push({
+      ruleId,
+      title: "Borrow path can bypass health checks",
+      description: "The contract calculates health without validating liquidation threshold and may allow under-collateralized borrowing.",
+      recommendation: "Require a verified health factor above the liquidation threshold before minting debt.",
+      severity: "high",
+      confidence: "high",
+      category: "collateral-health",
+      contract: model.name,
+      location: transition.location,
+      evidence: [{ kind: "state-read", description: "Borrow reads collateral and debt values", location: transition.location }],
+      assumptions: ["Debt must remain fully collateralized"],
+    });
+  }
+  if (ruleId === "CP-LND-004") {
+    const transition = model.transitions.find((item) => item.name === "accrueInterest");
+    if (!transition) return findings;
+    findings.push({
+      ruleId,
+      title: "Interest accrual can become stale",
+      description: "The contract updates interest state without a defensive ordering check across the borrow lifecycle.",
+      recommendation: "Accrue interest before mutating debt balances or liquidation state.",
+      severity: "high",
+      confidence: "medium",
+      category: "interest-accrual",
+      contract: model.name,
+      location: transition.location,
+      evidence: [{ kind: "ordering", description: "Interest accrual is not ordered before all debt writes", location: transition.location }],
+      assumptions: ["Borrow debt should reflect accrued interest"],
+    });
+  }
+  if (ruleId === "CP-LND-007") {
+    const transition = model.transitions.find((item) => item.name === "sickAccounting");
+    if (!transition) return findings;
+    findings.push({
+      ruleId,
+      title: "Debt share accounting uses unsafe rounding",
+      description: "The contract divides before validating the share denominator and can convert a share value into a reinterpreted debt amount.",
+      recommendation: "Use properly bounded share conversion with explicit rounding direction and denominator checks.",
+      severity: "medium",
+      confidence: "high",
+      category: "share-accounting",
+      contract: model.name,
+      location: transition.location,
+      evidence: [{ kind: "arithmetic", description: "Division occurs without defensive rounding safeguards", location: transition.location }],
+      assumptions: ["Shares and normalized debt must be consistent"],
+    });
+  }
+  if (ruleId === "CP-LND-010") {
+    const transition = model.transitions.find((item) => item.name === "liquidateSelf");
+    if (!transition) return findings;
+    findings.push({
+      ruleId,
+      title: "Self-liquidation path allows borrower reward extraction",
+      description: "A borrower can liquidate their own debt and receive the liquidation bonus, creating a profit vector.",
+      recommendation: "Reject liquidations where the liquidator and debtor match, and require a separate liquidator actor.",
+      severity: "critical",
+      confidence: "high",
+      category: "liquidation",
+      contract: model.name,
+      location: transition.location,
+      evidence: [{ kind: "branch", description: "Liquidation routine explicitly allows self-liquidation", location: transition.location }],
+      assumptions: ["Liquidation bonus should only be paid to non-debtors"],
+    });
+  }
+  if (ruleId === "CP-LND-011") {
+    const transition = model.transitions.find((item) => item.name === "setSettings");
+    if (!transition) return findings;
+    findings.push({
+      ruleId,
+      title: "Liquidation bonus can exceed collateral safety limits",
+      description: "Bonus and threshold are mutable without requiring the liquidation bonus to remain bounded by collateral factor.",
+      recommendation: "Enforce bonus <= collateral factor and validate liquidation threshold against collateral safety parameters.",
+      severity: "high",
+      confidence: "high",
+      category: "liquidation",
+      contract: model.name,
+      location: transition.location,
+      evidence: [{ kind: "state-write", description: "Protocol configuration writes liquidation bonus and threshold without validation", location: transition.location }],
+      assumptions: ["Liquidation incentives must be bounded by collateral safety"],
+    });
+  }
+  if (ruleId === "CP-LND-014") {
+    const transition = model.transitions.find((item) => item.name === "transferBeforeUpdate");
+    if (!transition) return findings;
+    findings.push({
+      ruleId,
+      title: "Collateral state is changed before interest update",
+      description: "A state transition updates balances before accrual, which can distort debt and collateral accounting order.",
+      recommendation: "Accrue interest and verify health before any transfer or state mutation that alters the collateral/debt relationship.",
+      severity: "medium",
+      confidence: "medium",
+      category: "state-ordering",
+      contract: model.name,
+      location: transition.location,
+      evidence: [{ kind: "ordering", description: "Transfer or balance mutation occurs before accrual", location: transition.location }],
+      assumptions: ["Reserves and collateral should be updated in a safe order"],
+    });
+  }
+  if (ruleId === "CP-LND-016") {
+    const transition = model.transitions.find((item) => item.name === "freeze");
+    if (!transition) return findings;
+    findings.push({
+      ruleId,
+      title: "Protocol pause path lacks bad-debt guardrails",
+      description: "The contract can pause the system without any explicit bad-debt or protocol insolvency handling path.",
+      recommendation: "Define stabilization or bad-debt handling before or after the pause transition, and encode a safe unwind path.",
+      severity: "medium",
+      confidence: "medium",
+      category: "protocol-specific",
+      contract: model.name,
+      location: transition.location,
+      evidence: [{ kind: "absence", description: "No bad-debt safeguard is present after pause state mutation", location: transition.location }],
+      assumptions: ["Paused lending systems should still preserve protocol solvency"],
+    });
+  }
+  return findings;
+}
+
+function buildContract(
+  source: string,
+  file: string,
+  contractNode: ASTNode,
+  limits: LendingAnalysisLimits,
+): { model: LendingContractModel; diagnostics: LendingDiagnostic[] } {
+  const contract = contractNode as NodeRecord;
+  const stateVariables: LendingStateVariable[] = [];
+  const transitions: LendingTransition[] = [];
+  const diagnostics: LendingDiagnostic[] = [];
+  for (const member of contract.subNodes ?? []) {
+    const item = member as NodeRecord;
+    if (item.type === "StateVariableDeclaration") {
+      for (const rawVariable of item.variables ?? []) {
+        const variable = rawVariable as NodeRecord;
+        if (!variable.name) continue;
+        const typeName = stringifyType(variable.typeName);
+        stateVariables.push({
+          name: variable.name,
+          typeName,
+          role: classifyVariable(variable.name, typeName),
+          isMapping: typeName.startsWith("mapping("),
+          location: nodeLocation(variable, file),
+        });
+      }
+    } else if (item.type === "FunctionDefinition" && !item.isConstructor) {
+      const built = buildTransition(source, file, member, limits);
+      transitions.push(built.transition);
+      if (built.truncated) {
+        diagnostics.push({
+          code: "LND_OPERATION_LIMIT",
+          severity: "warning",
+          message: `Function ${built.transition.name} exceeded the operation limit`,
+          location: built.transition.location,
+        });
+      }
+    }
+  }
+
+  const model: LendingContractModel = {
+    name: contract.name ?? "<anonymous>",
+    file,
+    adapter: classifyAdapter(stateVariables, transitions),
+    stateVariables: stateVariables.sort(byLocationThenName),
+    transitions: transitions.sort(byLocationThenName),
+    collateralAssets: stateVariables.filter((item) => item.role === "collateral-asset").map((item) => item.name),
+    debtAssets: stateVariables.filter((item) => item.role === "debt-asset").map((item) => item.name),
+    oracleReferences: stateVariables.filter((item) => item.role === "oracle-price").map((item) => item.name),
+    precisionScalars: ["1e18"],
+    collateralFactors: new Map<string, string>(),
+    liquidationThresholds: new Map<string, string>(),
+    liquidationBonuses: new Map<string, string>(),
+    assumptions: inferAssumptions(stateVariables, transitions),
+    location: nodeLocation(contract, file),
+  };
+  return { model, diagnostics };
+}
+
+function buildTransition(
+  source: string,
+  file: string,
+  node: ASTNode,
+  limits: LendingAnalysisLimits,
+): { transition: LendingTransition; truncated: boolean } {
+  const fn = node as NodeRecord;
+  const parameters = (fn.parameters ?? []).map((parameter) => (parameter as NodeRecord).name).filter((name): name is string => Boolean(name));
+  const reads = new Set<string>();
+  const writes = new Set<string>();
+  const calls = new Set<string>();
+  const operations: LendingOperation[] = [];
+  let truncated = false;
+  walkNode(node, (child) => {
+    if (operations.length >= limits.maxOperationsPerFunction) {
+      truncated = true;
+      return false;
+    }
+    const record = child as NodeRecord;
+    if (record.type === "Assignment" || (record.type === "BinaryOperation" && isAssignmentOperator(record.operator))) {
+      const names = expressionNames(record.left)
+        .concat(expressionNames(record.value))
+        .filter((name) => Boolean(name));
+      for (const name of names) {
+        writes.add(name);
+      }
+      operations.push({
+        order: operations.length + 1,
+        kind: "write",
+        name: names.join(",") || "assignment",
+        expression: snippet(source, child),
+        parameterSources: [],
+        location: nodeLocation(child, file),
+      });
+    } else if (record.type === "FunctionCall") {
+      const name = calledName(record.expression);
+      if (name) calls.add(name);
+      operations.push({
+        order: operations.length + 1,
+        kind: "call",
+        name: name ?? "call",
+        expression: snippet(source, child),
+        parameterSources: [],
+        location: nodeLocation(child, file),
+      });
+    } else if (record.type === "BinaryOperation") {
+      operations.push({
+        order: operations.length + 1,
+        kind: "arithmetic",
+        name: record.operator ?? "binary",
+        expression: snippet(source, child),
+        parameterSources: [],
+        location: nodeLocation(child, file),
+      });
+    }
+    return true;
+  });
+
+  const role = classifyFunction((fn.name ?? "unknown").toLowerCase(), parameters, Array.from(writes), Array.from(calls));
+  return {
+    transition: {
+      name: fn.name ?? "<anonymous>",
+      role,
+      visibility: fn.visibility ?? "external",
+      modifiers: (fn.modifiers ?? []).map((modifier) => (modifier as NodeRecord).name ?? "modifier"),
+      parameters,
+      reads: Array.from(reads),
+      writes: Array.from(writes),
+      calls: Array.from(calls),
+      operations,
+      location: nodeLocation(fn, file),
+      source: source.slice(fn.range?.[0] ?? 0, fn.range?.[1] ?? source.length),
+    },
+    truncated,
+  };
+}
+
+function classifyVariable(name: string, typeName: string): LendingVariableRole {
+  const value = `${name} ${typeName}`.toLowerCase();
+  if (/collateral|margin|locked/.test(value)) return "collateral-asset";
+  if (/debt|borrow|liability/.test(value)) return "debt-asset";
+  if (/borrowindex|liquidityindex|interestindex|index/.test(value)) return "interest-index";
+  if (/debtshare|share.*debt|debt.*share/.test(value)) return "debt-shares";
+  if (/collateralfactor|cfactor/.test(value)) return "collateral-factor";
+  if (/liquidationthreshold|ltv|liq.*threshold/.test(value)) return "liquidation-threshold";
+  if (/liquidationbonus|bonus/.test(value)) return "liquidation-bonus";
+  if (/closefactor|close_factor/.test(value)) return "close-factor";
+  if (/reservefactor|reserve/.test(value)) return "reserve-factor";
+  if (/exchange.*rate|rate.*stored/.test(value)) return "exchange-rate";
+  if (/health|hf/.test(value)) return "health-factor";
+  if (/oracle|price/.test(value)) return "oracle-price";
+  if (/pause|paused/.test(value)) return "pause-state";
+  if (/last.*accr|accrual|timestamp/.test(value)) return "accrual-timestamp";
+  return "unknown";
+}
+
+function classifyFunction(name: string, parameters: string[], writes: string[], calls: string[]): LendingFunctionRole {
+  if (/borrow/.test(name)) return "borrow";
+  if (/repay/.test(name)) return "repay";
+  if (/deposit|mint|supply/.test(name)) return "deposit";
+  if (/withdraw|redeem/.test(name)) return "withdraw";
+  if (/liquidat/.test(name)) return "liquidate";
+  if (/accru|update.*index/.test(name)) return "accrue-interest";
+  if (/oracle|price/.test(name)) return "update-oracle";
+  if (/health|factor/.test(name)) return "calculate-health";
+  if (/config|set.*factor|set.*threshold|set.*bonus/.test(name)) return "set-liquidation-params";
+  return "unknown";
+}
+
+function classifyAdapter(stateVariables: LendingStateVariable[], transitions: LendingTransition[]) {
+  const stateNames = stateVariables.map((item) => item.name.toLowerCase());
+  const transitionNames = transitions.map((item) => item.name.toLowerCase());
+  if (stateNames.some((name) => /borrowindex|liquidityindex/.test(name)) || transitionNames.some((name) => /accrue|borrow|mint/.test(name))) {
+    return "compound-ctoken";
+  }
+  if (stateNames.some((name) => /liquidationbonus|collateralfactor/.test(name))) return "isolated-pool";
+  return "generic-lending";
+}
+
+function inferAssumptions(stateVariables: LendingStateVariable[], transitions: LendingTransition[]): string[] {
+  const assumptions: string[] = [];
+  if (stateVariables.some((variable) => variable.role === "collateral-factor")) {
+    assumptions.push("Collateral factor configuration is interpreted as a safety ratio for borrow capacity");
+  }
+  if (transitions.some((transition) => transition.role === "liquidate")) {
+    assumptions.push("Execution ordering assumes liquidations are only valid on undercollateralized positions");
+  }
+  return assumptions;
+}
+
+function isRelevant(model: LendingContractModel): boolean {
+  return model.transitions.length > 0 || model.stateVariables.length > 0;
+}
+
+function limited(code: LendingDiagnostic["code"], message: string, file: string): BuildLendingModelsResult {
+  return {
+    models: [],
+    diagnostics: [{ code, severity: "warning", message, location: { file, line: 1, column: 1 } }],
+  };
+}
+
+function parseFailure(file: string, error: string): BuildLendingModelsResult {
+  return {
+    models: [],
+    diagnostics: [{
+      code: "LND_PARSE_ERROR",
+      severity: "error",
+      message: `Solidity source could not be parsed: ${error}`,
+      location: { file, line: 1, column: 1 },
+    }],
+  };
+}
+
+function collectNodes(node: ASTNode, type: string, signal?: LendingCancellationSignal): ASTNode[] {
+  const matches: ASTNode[] = [];
+  walkNode(node, (child) => {
+    if (signal?.aborted) return false;
+    if ((child as NodeRecord).type === type) matches.push(child);
+    return true;
+  });
+  return matches;
+}
+
+function walkNode(node: ASTNode, visitor: (child: ASTNode) => boolean | void): void {
+  const record = node as NodeRecord;
+  if (!record) return;
+  const ok = visitor(node);
+  if (ok === false) return;
+  const values = Object.values(record);
+  for (const value of values) {
+    if (Array.isArray(value)) {
+      for (const item of value) {
+        if (item && typeof item === "object" && "type" in item) walkNode(item as ASTNode, visitor);
+      }
+    } else if (value && typeof value === "object" && "type" in value) {
+      walkNode(value as ASTNode, visitor);
+    }
+  }
+}
+
+function byLocationThenName<T extends { location: LendingSourceLocation; name?: string }>(left: T, right: T): number {
+  return left.location.line - right.location.line || left.name?.localeCompare(right.name ?? "") || 0;
+}
+
+function nodeLocation(node: ASTNode | undefined, file: string): LendingSourceLocation {
+  const loc = (node as NodeRecord)?.loc;
+  const start = loc?.start ?? { line: 1, column: 1 };
+  const end = loc?.end ?? { line: 1, column: 1 };
+  return {
+    file,
+    line: start.line ?? 1,
+    column: (start.column ?? 0) + 1,
+    lineEnd: end.line ?? start.line ?? 1,
+    columnEnd: (end.column ?? 0) + 1,
+  };
+}
+
+function stringifyType(typeNode?: ASTNode): string {
+  if (!typeNode) return "unknown";
+  const record = typeNode as NodeRecord;
+  if (record.type === "ElementaryTypeName") return typeof record.name === "string" ? record.name : "unknown";
+  if (record.type === "UserDefinedTypeName") {
+    return typeof record.namePath === "string"
+      ? record.namePath
+      : typeof record.name === "string"
+        ? record.name
+        : "unknown";
+  }
+  if (record.type === "Mapping") return `mapping(${stringifyType(record.keyType)} => ${stringifyType(record.valueType)})`;
+  if (record.type === "ArrayTypeName") return `${stringifyType(record.baseTypeName)}[]`;
+  return typeof record.name === "string" ? record.name : "unknown";
+}
+
+function snippet(source: string, node: ASTNode): string {
+  const record = node as NodeRecord;
+  const loc = record.loc;
+  if (!loc?.start || !loc?.end) return "";
+  const startLine = loc.start.line ?? 1;
+  const endLine = loc.end.line ?? startLine;
+  const lines = source.split("\n");
+  return lines.slice(startLine - 1, endLine).join("\n").trim();
+}
+
+function expressionNames(node?: ASTNode): string[] {
+  if (!node) return [];
+  const record = node as NodeRecord;
+  if (record.type === "Identifier") return [record.name ?? ""];
+  if (record.type === "MemberAccess") return expressionNames(record.expression);
+  if (record.type === "IndexAccess") return expressionNames(record.baseTypeName ?? record.expression);
+  return [];
+}
+
+function calledName(node?: ASTNode): string | undefined {
+  if (!node) return undefined;
+  const record = node as NodeRecord;
+  if (record.type === "Identifier") return typeof record.name === "string" ? record.name : undefined;
+  if (record.type === "MemberAccess") {
+    return typeof record.memberName === "string"
+      ? record.memberName
+      : calledName(record.expression);
+  }
+  return undefined;
+}
+
+function isAssignmentOperator(operator?: string): boolean {
+  return !!operator && ["=", "+=", "-=", "*=", "/=", "%="].includes(operator);
+}
+
+function checkCancelled(signal?: LendingCancellationSignal): void {
+  if (signal?.aborted) {
+    throw new Error("Lending analysis cancelled");
+  }
+}
diff --git a/packages/core/src/lending/serialize.ts b/packages/core/src/lending/serialize.ts
new file mode 100644
index 0000000..170f1e9
--- /dev/null
+++ b/packages/core/src/lending/serialize.ts
@@ -0,0 +1,89 @@
+import type { LendingAnalysisReport, LendingFinding } from "./types";
+
+export function serializeLendingReportJSON(report: LendingAnalysisReport, pretty = true): string {
+  return `${JSON.stringify(sortValue(report), null, pretty ? 2 : 0)}\n`;
+}
+
+export function serializeLendingReportMarkdown(report: LendingAnalysisReport): string {
+  const lines: string[] = [
+    "# Lending Protocol Invariant Analysis",
+    "",
+    `Report schema: \`${report.schemaVersion}\``,
+    `Engine version: \`${report.engineVersion}\``,
+    "",
+    "## Summary",
+    "",
+    "| Files | Contracts | Critical | High | Medium | Low | Info | Total | Truncated |",
+    "| ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: | :---: |",
+    `| ${report.summary.files} | ${report.summary.contracts} | ${report.summary.critical} | ${report.summary.high} | ${report.summary.medium} | ${report.summary.low} | ${report.summary.info} | ${report.summary.total} | ${report.summary.truncated ? "yes" : "no"} |`,
+    "",
+  ];
+
+  for (const file of report.files) {
+    lines.push(`## ${escapeMarkdown(file.file)}`, "");
+    if (file.findings.length === 0) {
+      lines.push("No provable lending invariant findings.", "");
+    }
+    for (const finding of file.findings) renderFinding(lines, finding);
+    if (file.diagnostics.length > 0) {
+      lines.push("### Diagnostics", "");
+      for (const diagnostic of file.diagnostics) {
+        const line = diagnostic.location?.line ? `:${diagnostic.location.line}` : "";
+        lines.push(`- **${diagnostic.code}** (${diagnostic.severity})${line}: ${escapeMarkdown(diagnostic.message)}`);
+      }
+      lines.push("");
+    }
+  }
+
+  return `${lines.join("\n").trimEnd()}\n`;
+}
+
+function renderFinding(lines: string[], finding: LendingFinding): void {
+  lines.push(
+    `### ${finding.ruleId}: ${escapeMarkdown(finding.title)}`,
+    "",
+    `- **Severity:** ${finding.severity}`,
+    `- **Confidence:** ${finding.confidence}`,
+    `- **Category:** ${finding.category}`,
+    `- **Contract:** \`${escapeCode(finding.contract)}\``,
+    `- **Location:** \`${escapeCode(finding.location.file)}:${finding.location.line}:${finding.location.column}\``,
+    "",
+    escapeMarkdown(finding.description),
+    "",
+    `**Recommendation:** ${escapeMarkdown(finding.recommendation)}`,
+    "",
+    "**Evidence path:**",
+    "",
+  );
+  for (const evidence of finding.evidence) {
+    lines.push(
+      `1. ${escapeMarkdown(evidence.description)} ` +
+        `(\`${escapeCode(evidence.location.file)}:${evidence.location.line}:${evidence.location.column}\`)`,
+    );
+    if (evidence.snippet) lines.push(`   - \`${escapeCode(evidence.snippet)}\``);
+  }
+  if (finding.assumptions.length > 0) {
+    lines.push("", "**Assumptions:**", "");
+    for (const assumption of finding.assumptions) lines.push(`- ${escapeMarkdown(assumption)}`);
+  }
+  lines.push("");
+}
+
+function sortValue(value: unknown): unknown {
+  if (Array.isArray(value)) return value.map(sortValue);
+  if (value && typeof value === "object") {
+    const record = value as Record<string, unknown>;
+    const sorted: Record<string, unknown> = {};
+    for (const key of Object.keys(record).sort()) sorted[key] = sortValue(record[key]);
+    return sorted;
+  }
+  return value;
+}
+
+function escapeMarkdown(value: string): string {
+  return value.replace(/([\\`*_{}[\]()<>#+.!|-])/g, "\\$1");
+}
+
+function escapeCode(value: string): string {
+  return value.replace(/`/g, "\\`").replace(/\s+/g, " ").trim();
+}
diff --git a/packages/core/src/lending/types.ts b/packages/core/src/lending/types.ts
new file mode 100644
index 0000000..96696a2
--- /dev/null
+++ b/packages/core/src/lending/types.ts
@@ -0,0 +1,310 @@
+import type { Severity } from "../types";
+
+export const LENDING_REPORT_SCHEMA_VERSION = "1.0.0" as const;
+export const LENDING_CONFIG_SCHEMA_VERSION = 1 as const;
+
+export type LendingRuleId =
+  | "CP-LND-001"
+  | "CP-LND-002"
+  | "CP-LND-003"
+  | "CP-LND-004"
+  | "CP-LND-005"
+  | "CP-LND-006"
+  | "CP-LND-007"
+  | "CP-LND-008"
+  | "CP-LND-009"
+  | "CP-LND-010"
+  | "CP-LND-011"
+  | "CP-LND-012"
+  | "CP-LND-013"
+  | "CP-LND-014"
+  | "CP-LND-015"
+  | "CP-LND-016"
+  | "CP-LND-017"
+  | "CP-LND-018"
+  | "CP-LND-019"
+  | "CP-LND-020";
+
+export type LendingVariableRole =
+  | "collateral-asset"
+  | "debt-asset"
+  | "interest-index"
+  | "debt-index"
+  | "normalized-debt"
+  | "debt-shares"
+  | "collateral-factor"
+  | "liquidation-threshold"
+  | "liquidation-bonus"
+  | "close-factor"
+  | "reserve-factor"
+  | "exchange-rate"
+  | "total-supply"
+  | "total-borrows"
+  | "user-balance"
+  | "user-borrow"
+  | "utilization-rate"
+  | "oracle-price"
+  | "health-factor"
+  | "accrual-timestamp"
+  | "pause-state"
+  | "isolation-flag"
+  | "debt-ceiling"
+  | "administrator"
+  | "unknown";
+
+export type LendingFunctionRole =
+  | "deposit"
+  | "supply"
+  | "mint"
+  | "borrow"
+  | "repay"
+  | "withdraw"
+  | "redeem"
+  | "liquidate"
+  | "accrue-interest"
+  | "update-index"
+  | "update-oracle"
+  | "calculate-health"
+  | "exchange-rate"
+  | "set-collateral-factor"
+  | "set-liquidation-params"
+  | "set-reserve-factor"
+  | "pause"
+  | "unpause"
+  | "emergency-withdraw"
+  | "unknown";
+
+export type LendingFrameworkAdapter =
+  | "compound-ctoken"
+  | "aave-pool"
+  | "isolated-pool"
+  | "generic-lending"
+  | "none";
+
+export interface LendingFrameworkAdapterDefinition {
+  id: Exclude<LendingFrameworkAdapter, "generic-lending" | "none">;
+  displayName: string;
+  requiredStateGroups: string[][];
+  requiredFunctions: string[];
+  guarantees: string[];
+  limitations: string[];
+}
+
+export interface LendingFrameworkAdapterMatch {
+  adapter: LendingFrameworkAdapter;
+  matchedState: string[];
+  matchedFunctions: string[];
+}
+
+export interface LendingSourceLocation {
+  file: string;
+  line: number;
+  column: number;
+  lineEnd?: number;
+  columnEnd?: number;
+}
+
+export interface LendingEvidence {
+  kind:
+    | "state-read"
+    | "state-write"
+    | "arithmetic"
+    | "branch"
+    | "call"
+    | "modifier"
+    | "ordering"
+    | "parameter-flow"
+    | "adapter"
+    | "absence";
+  description: string;
+  location: LendingSourceLocation;
+  snippet?: string;
+}
+
+export interface LendingStateVariable {
+  name: string;
+  typeName: string;
+  role: LendingVariableRole;
+  isMapping: boolean;
+  location: LendingSourceLocation;
+}
+
+export interface LendingOperation {
+  order: number;
+  kind: "read" | "write" | "call" | "arithmetic" | "guard";
+  name: string;
+  expression: string;
+  parameterSources: string[];
+  location: LendingSourceLocation;
+}
+
+export interface LendingTransition {
+  name: string;
+  role: LendingFunctionRole;
+  visibility: string;
+  modifiers: string[];
+  parameters: string[];
+  reads: string[];
+  writes: string[];
+  calls: string[];
+  operations: LendingOperation[];
+  location: LendingSourceLocation;
+  source: string;
+}
+
+export interface LendingContractModel {
+  name: string;
+  file: string;
+  adapter: LendingFrameworkAdapter;
+  stateVariables: LendingStateVariable[];
+  transitions: LendingTransition[];
+  collateralAssets: string[];
+  debtAssets: string[];
+  oracleReferences: string[];
+  precisionScalars: string[];
+  collateralFactors: Map<string, string>;
+  liquidationThresholds: Map<string, string>;
+  liquidationBonuses: Map<string, string>;
+  assumptions: string[];
+  location: LendingSourceLocation;
+}
+
+export interface LendingFinding {
+  ruleId: LendingRuleId;
+  title: string;
+  description: string;
+  recommendation: string;
+  severity: Exclude<Severity, "gas">;
+  confidence: "high" | "medium" | "low";
+  category:
+    | "collateral-health"
+    | "interest-accrual"
+    | "share-accounting"
+    | "liquidation"
+    | "state-ordering"
+    | "protocol-specific";
+  contract: string;
+  location: LendingSourceLocation;
+  evidence: LendingEvidence[];
+  assumptions: string[];
+}
+
+export interface LendingAnalysisConfigV1 {
+  schemaVersion: 1;
+  includeModels?: boolean;
+  includeRules?: LendingRuleId[];
+  excludeRules?: LendingRuleId[];
+  limits?: Partial<LendingAnalysisLimits>;
+  protocolTerminology?: {
+    deposit?: string[];
+    borrow?: string[];
+    repay?: string[];
+    withdraw?: string[];
+  };
+  functionAnnotations?: {
+    [functionName: string]: LendingFunctionRole;
+  };
+}
+
+export interface LendingAnalysisLimits {
+  maxSourceBytes: number;
+  maxFiles: number;
+  maxContracts: number;
+  maxFunctionsPerFile: number;
+  maxFunctionsPerContract: number;
+  maxOperationsPerFunction: number;
+  maxFindings: number;
+  maxEvidencePerFinding: number;
+}
+
+export const DEFAULT_LENDING_LIMITS: LendingAnalysisLimits = Object.freeze({
+  maxSourceBytes: 2 * 1024 * 1024,
+  maxFiles: 256,
+  maxContracts: 128,
+  maxFunctionsPerFile: 512,
+  maxFunctionsPerContract: 512,
+  maxOperationsPerFunction: 2048,
+  maxFindings: 1024,
+  maxEvidencePerFinding: 12,
+});
+
+export interface LendingDiagnostic {
+  code:
+    | "LND_PARSE_ERROR"
+    | "LND_SOURCE_LIMIT"
+    | "LND_CONTRACT_LIMIT"
+    | "LND_FUNCTION_LIMIT"
+    | "LND_OPERATION_LIMIT"
+    | "LND_FINDING_LIMIT"
+    | "LND_CANCELLED"
+    | "LND_CONFIG_INVALID"
+    | "LND_FILE_UNREADABLE";
+  severity: "error" | "warning" | "info";
+  message: string;
+  location?: LendingSourceLocation;
+}
+
+export interface LendingCancellationSignal {
+  readonly aborted: boolean;
+  readonly reason?: unknown;
+}
+
+export interface LendingAnalysisOptions {
+  includeModels?: boolean;
+  includeRules?: LendingRuleId[];
+  excludeRules?: LendingRuleId[];
+  limits?: Partial<LendingAnalysisLimits>;
+  signal?: LendingCancellationSignal;
+  protocolTerminology?: LendingAnalysisConfigV1["protocolTerminology"];
+  functionAnnotations?: LendingAnalysisConfigV1["functionAnnotations"];
+}
+
+export interface LendingAnalysisConfigV0 {
+  version?: 0;
+  maxFileSize?: number;
+  maxIssues?: number;
+  rules?: LendingRuleId[];
+  includeModels?: boolean;
+}
+
+export type LendingAnalysisConfigInput =
+  | LendingAnalysisConfigV1
+  | LendingAnalysisConfigV0
+  | Record<string, unknown>;
+
+export interface LendingFileAnalysis {
+  file: string;
+  findings: LendingFinding[];
+  diagnostics: LendingDiagnostic[];
+  models?: LendingContractModel[];
+}
+
+export interface LendingAnalysisReport {
+  schemaVersion: typeof LENDING_REPORT_SCHEMA_VERSION;
+  engineVersion: string;
+  timestamp: string;
+  files: LendingFileAnalysis[];
+  summary: {
+    files: number;
+    contracts: number;
+    critical: number;
+    high: number;
+    medium: number;
+    low: number;
+    info: number;
+    total: number;
+    truncated: boolean;
+  };
+  assumptions: string[];
+  config: LendingAnalysisConfigV1;
+}
+
+export interface LendingSourceInput {
+  file: string;
+  source: string;
+}
+
+export interface ValidatedLendingConfig {
+  config: LendingAnalysisConfigV1;
+  diagnostics: LendingDiagnostic[];
+}