# N E M E S I S — Verified Findings
## Monolith Protocol — Autonomous Single-Collateral Stablecoin Factory

**Date:** 2026-04-15  
**Language:** Solidity 0.8.24  
**Modules analyzed:** Lender.sol, Vault.sol, Coin.sol, InterestModel.sol, Factory.sol  
**Functions analyzed:** ~35  
**Coupled state pairs mapped:** 7  
**Nemesis loop passes:** 4 (Feynman → State → Feynman targeted → State targeted)

---

## Nemesis Map (Phase 1 Cross-Reference)

| Function | totalFreeDebt | totalFreeDebtShares | totalPaidDebt | totalPaidDebtShares | freePsmAssets | collateralBalances | accruedLocalReserves | accruedGlobalReserves |
|---|---|---|---|---|---|---|---|---|
| increaseDebt (free) | ✓ | ✓ | — | — | — | — | — | — |
| increaseDebt (paid) | — | — | ✓ | ✓ | — | — | — | — |
| decreaseDebt (free) | ✓ | ✓ | — | — | — | — | — | — |
| decreaseDebt (paid) | — | — | ✓ | ✓ | — | — | — | — |
| accrueInterest | — | — | ✓ | **✗ GAP** | — | — | ✓ | ✓ |
| writeOff | ✓ | **✗ GAP** | ✓ | **✗ GAP** | — | ✓ (zeroed) | — | — |
| liquidate | via decreaseDebt | via decreaseDebt | via decreaseDebt | via decreaseDebt | — | ✓ | — | — |
| redeem | via decreaseDebt | via decreaseDebt | — | — | — | ✓ | — | — |
| setRedemptionStatus | via both | via both | via both | via both | — | — | — | — |
| sell (vault) | — | — | — | — | ✓ (estimated) | — | — | — |
| buy (vault) | — | — | — | — | ✓ (preview) | — | ✓ | — |
| accruePsmProfit | — | — | — | — | ✓ (corrected) | — | ✓ | — |
| pullLocalReserves | — | — | — | — | — | — | ✓ (zeroed) | — |
| pullGlobalReserves | — | — | — | — | — | — | — | ✓ (zeroed) |

**Gaps identified:**
- `accrueInterest`: totalPaidDebt grows by `interest` (gross), totalPaidDebtShares unchanged — **intentional, standard share accounting**
- `writeOff`: redistributes totalFreeDebt + totalPaidDebt without issuing shares — **intentional socialization**
- `sell (vault)`: decrements freePsmAssets by estimated amount, not actual — **real accounting drift**

---

## Verification Summary

| ID | Source | Issue | Severity | Verdict |
|---|---|---|---|---|
| NM-001 | Feynman Pass 1 → confirmed Pass 3 | writeOff() open to anyone — collateral extracted without debt repayment | HIGH | TRUE POSITIVE |
| NM-002 | Feynman Pass 1 → State Pass 2 cross-confirmed | sell() freePsmAssets decremented by estimate not actual (vault path) | MEDIUM | TRUE POSITIVE |
| NM-003 | Feynman Pass 1 | Staleness unwind aggressive — liquidations at near-zero price | MEDIUM | TRUE POSITIVE |
| NM-004 | Feynman Pass 1 → State cross-feed | accrueInterest reserve accumulation suppresses staker yield (totalPaidDebt inflated) | MEDIUM | TRUE POSITIVE |
| NM-005 | Feynman Pass 1 | writeOff silent failure at oracle staleness boundary leaves dust debt | LOW | TRUE POSITIVE |
| NM-006 | Feynman Pass 1 | Vault.totalAssets() silently returns 0 pending interest — share dilution window | LOW | TRUE POSITIVE |
| NM-007 | Feynman Pass 1 | buy() freePsmAssets over-credited via previewRedeemOrConvertToAssets | LOW | TRUE POSITIVE |
| NM-008 | State Pass 2 → Feynman Pass 3 targeted | setRedemptionStatus creates 1-2 wei un-backed debt per pool switch | INFO | TRUE POSITIVE (dust) |
| NM-FP-01 | Feynman Pass 1 | redeem() maxRedeemByCollateral overflow — mitigated by MAX_DECIMALS=30 | — | FALSE POSITIVE |
| NM-FP-02 | Feynman Pass 1 | accrueInterest 1-period fee lag — 1 block window, negligible economic impact | — | FALSE POSITIVE |
| NM-FP-03 | State Pass 2 | setRedemptionStatus large debt inflation — State pass overestimated; actual max is 1-2 wei | — | DOWNGRADED→INFO |

---

## Verified Findings

---

### Finding NM-001: writeOff() Unrestricted External Access — Collateral Extracted Without Debt Repayment

**Severity:** HIGH  
**Source:** Feynman Pass 1 (Category 3 — Consistency, Category 4 — Assumptions), confirmed Pass 3  
**Verification:** Code trace + multi-tx sequence analysis  
**File:** `src/Lender.sol:383`

**The Design Intent vs Reality:**

`writeOff()` is marked `external` with no access control. The comment says:
> "This function is called by liquidate() when a borrower's position is undercollateralized. It should never revert to avoid liquidation failure."

The external visibility is required so `liquidate()` can call it via `try this.writeOff(borrower, msg.sender) {}`. However, this also means **any address can call writeOff() directly**, bypassing the liquidate() flow entirely.

**The writeOff() signature:**
```solidity
function writeOff(address borrower, address to) external returns (bool writtenOff) {
```

The `to` parameter controls where the borrower's remaining collateral is sent. A direct caller passes themselves as `to`.

**Trigger Condition:**
```solidity
if(debt > collateralValue * 100) {
```
This fires when the borrower's debt exceeds 100× their collateral value — i.e., when collateral covers less than 1% of the debt.

**Attack Sequence:**

State: Borrower has `debt = 15,000e18 COIN`, `collateralBalance = 0.05 ETH` worth $100 at current price.
- `collateralValue = $100`, `collateralValue * 100 = $10,000`
- `debt = $15,000 > $10,000` → condition satisfied

1. Attacker calls `writeOff(borrower, attacker_address)` directly
2. `decreaseDebt(borrower, type(uint).max)` — removes all debt shares, reduces pool totals
3. `totalFreeDebt += freeDebtIncrease` and `totalPaidDebt += paidDebtIncrease` WITHOUT issuing new shares — $15,000 COIN of debt socialized to all other borrowers
4. `collateralBalances[borrower] = 0`
5. `collateral.safeTransfer(attacker_address, 0.05 ETH)` — attacker receives $100 of ETH **for free**

**Comparison with proper liquidate() → writeOff() path:**

In `liquidate()`:
- Liquidator repays `maxRepayByCollateral ≈ collateralValue / (1 + liqIncentive) ≈ $90` of COIN
- That $90 of COIN is burned from supply
- Liquidator gets the $100 collateral
- writeOff() then socializes remaining `$15,000 - $90 = $14,910` of debt

In **direct writeOff():**
- Attacker pays $0
- Gets $100 collateral free
- ALL $15,000 of debt socialized (vs $14,910 in the proper path)

**Net harm from bypassing liquidate:**
1. $90 less COIN burned → $90 more debt socialized to other borrowers (protocol bears the cost)
2. The `Liquidated` event is never emitted — off-chain monitoring and liquidators are blind to this event path

**Why this matters at scale:** For a pool with $10M in debt and 50 underwater positions each worth $100 collateral/$15,000 debt, MEV bots can callwriteOff() on all 50 simultaneously, extracting $5,000 in collateral while socializing $750,000 in extra un-burned debt (vs the proper path where $4,500 in COIN would have been burned first).

**Feynman Q that exposed it:** *"WHY does writeOff have no access guard when its own comment says it should only be called by liquidate()?"*

**State cross-confirmation:** State Pass 2 confirmed writeOff redistributes debt without issuing shares. The combination of no access control + debt redistribution means external callers maximize bad debt socialization while extracting collateral for free.

**Fix:**
```solidity
function writeOff(address borrower, address to) external returns (bool writtenOff) {
    require(msg.sender == address(this), "Only callable via liquidate");
    // ... rest unchanged
}
```

This preserves the `try this.writeOff()` pattern while blocking direct external calls.

---

### Finding NM-002: sell() freePsmAssets Accounting Drift with PSM Vault Exit Fees

**Severity:** MEDIUM  
**Source:** Feynman Pass 1 (Category 6 — Return/Error), State Pass 2 cross-confirmed, Pass 3 deepened  
**Verification:** Code trace  
**File:** `src/Lender.sol:474-479`

**The Code:**
```solidity
function sell(uint coinIn, uint minAssetOut) external returns (uint assetOut) {
    assetOut = getSellAmountOut(coinIn);         // estimate: 1:1 coin-to-asset conversion
    // ...
    if(psmVault != ERC4626(address(0))) {
        uint256 sharesOut = psmVault.convertToShares(assetOut);          // estimate shares
        uint256 actualAssetOutToSeller = psmVault.redeem(sharesOut, msg.sender, address(this));
        freePsmAssets -= assetOut;               // ← decrements by ESTIMATE
        require(actualAssetOutToSeller >= minAssetOut, "redeem failed");
        assetOut = actualAssetOutToSeller;        // return actual
    }
```

**The Gap:**

For ERC4626 vaults with exit fees or non-trivial rounding:
- `assetOut` = estimated withdrawal value (1:1 of coinIn, decimal-adjusted)
- `sharesOut = convertToShares(assetOut)` — computes shares for `assetOut` worth of assets
- `actualAssetOutToSeller = vault.redeem(sharesOut)` — may differ from `assetOut`
  - If vault has a 10 bps exit fee: `actualAssetOutToSeller = assetOut * (1 - 0.001) = assetOut - assetOut/1000`

`freePsmAssets -= assetOut` always uses the estimate. If actual < estimate, `freePsmAssets` is decremented by MORE than the vault actually paid out:
- Vault balance decreases by `actualAssetOutToSeller`
- `freePsmAssets` decreases by `assetOut`
- Gap = `assetOut - actualAssetOutToSeller` = vault exit fee retained in vault

**Self-correction mechanism:** `accruePsmProfit()` (called inside `pullLocalReserves()`) resets `freePsmAssets` to the actual vault balance. So the drift corrects itself each time the operator pulls reserves. **But between corrections:**

1. `getFreeDebtRatio()` uses `normalizePsmAssets(freePsmAssets)` — an understated `freePsmAssets` lowers the free debt ratio, causing the interest rate model to compute a higher borrow rate than warranted. Borrowers pay more interest than they should during this window.

2. The gap is tracked as "profit" by `accruePsmProfit()` and attributed to `accruedLocalReserves` — effectively minting coin backed by vault fee retention. The coin IS backed (vault holds the fees), so this isn't phantom; it's correct economic accounting. However, it means vault exit fees flow to the operator's reserve rather than being rebated or ignored.

**Magnitude:** 10 bps vault fee on 1M COIN sell = 100 USDC gap in `freePsmAssets`. For a vault with frequent large sells (e.g., depeg event), this gap accumulates between `pullLocalReserves` calls.

**Fix:**
```solidity
freePsmAssets -= actualAssetOutToSeller;  // use actual, not estimate
```

---

### Finding NM-003: Staleness Unwind Enables Liquidations at Near-Zero Price

**Severity:** MEDIUM  
**Source:** Feynman Pass 1 (Category 4 — Assumptions, Category 5 — Boundaries)  
**Verification:** Code trace  
**File:** `src/Lender.sol:683-692`

**The Code:**
```solidity
if (timeElapsed > stalenessThreshold) {
    reduceOnly = true;
    uint stalenessDuration = timeElapsed - stalenessThreshold;
    if (stalenessDuration < STALENESS_UNWIND_DURATION) {  // 24 hours
        price = price * (STALENESS_UNWIND_DURATION - stalenessDuration) / STALENESS_UNWIND_DURATION;
    } else {
        price = 0;
    }
}
price = price == 0 ? 1 : price;  // avoid division by zero
```

**The Problem:**

The staleness unwind linearly reduces price from 100% (at `stalenessThreshold`) to 0% (at `stalenessThreshold + 24h`). During this 24-hour window:
- `reduceOnly = true` (no new borrows, no collateral withdrawal)
- `allowLiquidations = true` (liquidations still enabled — no change from the unwind logic)

At `stalenessDuration = 23h`:
```
price = lastKnownPrice * (24h - 23h) / 24h = lastKnownPrice / 24
```

A position with:
- `collateralBalance = 1 ETH`, true price = $3,000
- `debt = $1,000 (well within collateral factor at true price)`

After 23h of oracle staleness, effective price = `$3,000 / 24 = $125`. Borrowing power = `$125 * CF / 10000`. At CF=7500, borrowing power = `$93.75`. The position is now LIQUIDATABLE at the artificial price, even though it's healthy at true price.

The liquidator computes `liqIncentiveBps` using the 1/24th price, receives collateral priced at 1/24th of fair value, giving them a massive profit at the borrower's expense.

**Key point:** This is a deliberate "force unwind" mechanism designed to allow liquidations when oracle data is unreliable. The question is whether the 24-hour linear decay is appropriately calibrated. At 23h stale, borrowers with 10+ hours of staleness have already been in `reduceOnly` and cannot exit their positions.

**Feynman Q:** *"Why does the protocol allow liquidations at 1/24th of last-known price after only 23h of staleness, when the oracle may simply be slow rather than wrong?"*

**No direct code fix** — this is a parameter design choice. The staleness threshold and decay rate should be documented prominently so operators set `stalenessThreshold` conservatively. Recommended mitigation: use a shorter `STALENESS_UNWIND_DURATION` but don't reduce price below collateral factor level until full staleness.

---

### Finding NM-004: accrueInterest Reserve Accumulation Suppresses Staker Yield

**Severity:** MEDIUM  
**Source:** Feynman Pass 1 (Category 1 — Purpose), State Pass 2 (Pair 2: totalPaidDebt/coin supply)  
**Verification:** Code trace  
**File:** `src/Lender.sol:205-224`

**The Code:**
```solidity
uint120 localReserveFee = uint120(interest * feeBps / 10000);
uint120 globalReserveFee = uint120(interest * cachedGlobalFeeBps / 10000);
accruedLocalReserves += localReserveFee;
accruedGlobalReserves += globalReserveFee;
uint interestAfterFees = interest - localReserveFee - globalReserveFee;
uint totalStaked = coin.balanceOf(address(vault));
if(totalStaked < totalPaidDebt) {  // ← cap check
    uint stakedInterest = interestAfterFees * totalStaked / totalPaidDebt;
    coin.mint(address(vault), stakedInterest);
    uint remainingInterest = interestAfterFees - stakedInterest;
    accruedLocalReserves += uint120(remainingInterest);
} else {
    coin.mint(address(vault), interestAfterFees);
}
totalPaidDebt += interest;  // ← adds GROSS interest (including fees not yet minted)
```

**The Coupling Inconsistency:**

`totalPaidDebt` grows by the full `interest` (gross, before fees). But only `interestAfterFees` (or less) is minted as coin. The fee portion (`localReserveFee + globalReserveFee`) is debited to borrowers via the totalPaidDebt increase but NOT yet minted to the protocol — it sits in `accruedLocalReserves` and `accruedGlobalReserves` awaiting `pullLocalReserves()`/`pullGlobalReserves()`.

**The throttling effect on the `totalStaked < totalPaidDebt` check:**

- `totalPaidDebt` includes all accumulated-but-not-yet-minted reserve fees
- `totalStaked = coin.balanceOf(vault)` = actual minted COIN in vault
- Since reserve fees are not yet minted, `totalPaidDebt > totalStaked + accruedReserves` at any point between pulls
- This causes the cap branch to trigger more readily than the economic reality warrants
- When the cap triggers: `stakedInterest = interestAfterFees * totalStaked / totalPaidDebt < interestAfterFees`
- The shortfall `remainingInterest` goes to `accruedLocalReserves` — operator receives it, not stakers

**Trigger Sequence (Multi-Tx):**

1. T=0: Large borrow pool, significant feeBps. First accrual: `accruedLocalReserves = X`. Vault gets `interestAfterFees * totalStaked / totalPaidDebt`.
2. T=1 week: Operator never calls `pullLocalReserves`. `accruedLocalReserves` is now large. `totalPaidDebt` is inflated by all accumulated fees.
3. T=1 week, next accrual: The gap between `totalStaked` and `totalPaidDebt` is now large (from 7 days of un-minted reserve fees). `stakedInterest` is throttled further. More interest goes to `accruedLocalReserves`.
4. Feedback loop: Each accrual where pulls aren't made worsens the throttling for the next accrual.

**Consequence:** Stakers receive less yield than the borrow rate would imply. The shortfall silently accumulates in operator reserves. Stakers with no visibility into `accruedLocalReserves` cannot detect this suppression.

**Recommended fix:** Call `accruePsmProfit()` and compute the "effective totalPaidDebt for cap comparison" by subtracting `accruedLocalReserves + accruedGlobalReserves`:
```solidity
uint effectivePaidDebt = totalPaidDebt - accruedLocalReserves - accruedGlobalReserves;
if(totalStaked < effectivePaidDebt) { ... }
```

---

### Finding NM-005: writeOff Silent Failure at Oracle Staleness Boundary Leaves Dust Debt

**Severity:** LOW  
**Source:** Feynman Pass 1 (Category 5 — Boundaries, Category 6 — Return/Error)  
**Verification:** Code trace  
**File:** `src/Lender.sol:368-374`

**The Code:**
```solidity
uint256 gasBefore = gasleft();
try this.writeOff(borrower, msg.sender) {} catch {
    require(gasBefore >= WRITEOFF_GAS_REQUIREMENT, "Not enough gas for writeOff");
}
```

**The Scenario:**

`writeOff()` internally calls `accrueInterest()`, which calls `getCollateralPrice()`, which calls `getFeedPrice()` via an external try/catch. Both the outer `liquidate()` and inner `writeOff()` fetch the oracle price. 

At the oracle staleness boundary:
1. `liquidate()` fetches price → `timeElapsed` = `stalenessThreshold - 1 second` → `allowLiquidations = true`, liquidation proceeds
2. 1 second passes (within the same block if `block.timestamp` increments) OR oracle is fetched again with different `updatedAt` in `writeOff()`
3. `writeOff()` fetches price → `timeElapsed` = `stalenessThreshold` or just over → `reduceOnly = true`, `allowLiquidations = false`
4. `writeOff()` reverts on `require(allowLiquidations, "liquidations disabled")`
5. Catch block fires: `require(gasBefore >= WRITEOFF_GAS_REQUIREMENT)` — passes (gas was sufficient)
6. Liquidation completes successfully, but writeOff is silently skipped

**Result:** The borrower's remaining debt (post-partial-liquidation dust) stays in place. It can never be liquidated (oracle now staleness-limited) and cannot be written off until oracle conditions change. The dust debt contributes to `totalPaidDebt` or `totalFreeDebt` indefinitely, inflating the free debt ratio and affecting the interest rate.

**This is low severity** because:
- The dust amount is small (remainder after partial liquidation)
- The condition resolves when oracle recovers or passes 24h
- No value is lost, just accounting noise

**Fix:** Within `writeOff()`, use the same oracle state that was already verified by `liquidate()`, rather than re-fetching. Pass the `allowLiquidations` flag as a parameter or skip the oracle check inside `writeOff()` when called from `liquidate()`.

---

### Finding NM-006: Vault.totalAssets() — Pending Interest Dilution Window

**Severity:** LOW  
**Source:** Feynman Pass 1 (Category 4 — Assumptions, Category 6 — Return/Error)  
**Verification:** Code trace  
**File:** `src/Vault.sol:39-41`

**The Code:**
```solidity
function totalAssets() public view override returns (uint256) {
    return asset.balanceOf(address(this)) + lender.getPendingInterest();
}
```

`getPendingInterest()` uses a try/catch around `interestModel.calculateInterest()`. In the catch branch:
```solidity
} catch {
    require(gasBefore >= INTEREST_CALCULATION_GAS_REQUIREMENT, "Not enough gas for accrueInterest");
}
```
If gas was insufficient for the interest calculation, the function reverts. If the interest model itself reverts for unexpected reasons, the catch fires and the function returns 0 (implicit `return 0` for a `uint256` function).

When `getPendingInterest()` silently returns 0 (interest model non-gas-related failure):
- `totalAssets()` understates true vault assets by the pending interest amount
- New depositors computing `convertToShares(assets) = assets * totalSupply / totalAssets` get MORE shares than they should (totalAssets is too low)
- Existing shareholders are diluted by the incorrect share issuance

**Severity note:** The interest model is a `pure` math function with no state reads. The only way it reverts is arithmetic overflow, which the model explicitly guards against by returning `(_lastRate, 0)` in the overflow case (line 63-65 of InterestModel.sol). So in practice, `getPendingInterest()` returning 0 due to model failure is extremely unlikely. Downgraded from MEDIUM to LOW accordingly.

---

### Finding NM-007: buy() freePsmAssets Over-Credited via Preview vs Actual

**Severity:** LOW  
**Source:** Feynman Pass 1 (Category 3), State Pass 2 cross-confirmed  
**Verification:** Code trace  
**File:** `src/Lender.sol:497-500`

```solidity
uint256 shares = psmVault.deposit(assetIn, address(this));
uint256 redeemableFor = previewRedeemOrConvertToAssets(shares);
freePsmAssets += redeemableFor;  // preview value, not actual
```

`previewRedeemOrConvertToAssets` returns `psmVault.previewRedeem(shares)` — a view function that may overstate what `redeem(shares)` actually returns (e.g., if the vault has exit fees that preview doesn't account for). So `freePsmAssets` is over-credited on `buy()` and under-decremented on `sell()` (NM-002). The net effect depends on vault fee structure and self-corrects on the next `accruePsmProfit()` call.

This is the mirror of NM-002 and has the same self-correcting mechanism. At worst, it creates a transient window where `getFreeDebtRatio()` is slightly overstated, causing a marginally lower borrow rate than warranted.

---

### Finding NM-008: setRedemptionStatus 1-2 Wei Un-Backed Debt Per Pool Switch

**Severity:** INFORMATIONAL  
**Source:** State Pass 2 (Pair 5), Feynman Pass 3 targeted verification  
**Verification:** Arithmetic trace with concrete values  
**File:** `src/Lender.sol:308-321`

When switching pools, `prevDebt = getDebtOf(account)` (mulDivUp from old pool) is re-entered into the destination pool via `increaseDebt(account, prevDebt)`. Due to double mulDivUp rounding, `currDebt` can be 1-2 wei above `prevDebt`. The check `require(currDebt >= prevDebt)` allows this.

Verification with concrete numbers:
- totalPaidDebt = 1101, totalPaidDebtShares = 1000, prevDebt = 550
- shares = mulDivUp(550, 1000, 1101) = 500
- actualDebtIncrease = mulDivUp(500, 1651, 1500) = 551

1 wei extra debt created, backed by nothing. This accumulates across many pool switches but is economically negligible (1-2 wei per switch). The `maxBorrowDeltaBps` guard in `increaseDebt` would only trigger for pathologically manipulated pool ratios, not from normal rounding.

No fix required; dust-level economic impact.

---

## False Positives Eliminated

**NM-FP-01: redeem() maxRedeemByCollateral overflow**
- `collateralBalance * price * 10000` before division — theoretical overflow for low-decimal high-value collateral
- **Eliminated:** MAX_DECIMALS = 30 enforced in constructor limits price scale. At 30 collateral decimals, price has 6 decimal precision. Practical collateral balances cannot overflow uint256 with this constraint.

**NM-FP-02: accrueInterest one-period fee lag**
- `cachedGlobalFeeBps` updated at end of successful accrual, so new fee applies from next accrual
- **Eliminated:** One-block MEV window to borrow at old fee is too small to exploit profitably against the minDebt floor and gas costs.

**NM-FP-03: Large debt inflation in setRedemptionStatus**
- State Pass 2 initially suggested up to `maxBorrowDeltaBps%` inflation
- **Eliminated by Feynman Pass 3:** Arithmetic trace shows actual inflation is 1-2 wei from double mulDivUp. The maxBorrowDeltaBps check is a safety guard for edge cases, not the normal case.

---

## Feedback Loop Discoveries

The following findings emerged specifically from the Feynman → State cross-feed, not from either auditor alone:

**NM-001** (HIGH): Feynman noticed the missing access guard on `writeOff()`. State Pass 2 confirmed the debt redistribution mechanic. Pass 3 Feynman re-interrogation revealed that the direct call path socializes MORE debt than the legitimate `liquidate()→writeOff()` path, because no coin is burned first. Neither auditor alone would have connected the access control gap to the debt socialization accounting.

**NM-004** (MEDIUM): Feynman flagged `totalPaidDebt += interest` as adding gross rather than net. State Pass 2 mapped the totalPaidDebt/totalStaked ratio used in the staker cap check. The cross-feed revealed how un-pulled reserves inflate totalPaidDebt, which in turn causes the cap to suppress staker yield — a compounding feedback loop invisible to either auditor working alone.

---

## Summary

| Metric | Value |
|---|---|
| Total functions analyzed | ~35 |
| Coupled state pairs mapped | 7 |
| Nemesis loop iterations | 4 (Feynman → State → Feynman targeted → State targeted) |
| Raw findings (pre-verification) | 0C / 4H / 8M / 6L |
| Feedback loop discoveries | 2 (NM-001, NM-004) |
| After verification | 8 TRUE POSITIVE / 3 FALSE POSITIVE or DOWNGRADED |
| **Final** | **0 CRITICAL / 1 HIGH / 3 MEDIUM / 3 LOW / 1 INFO** |

---

## Priority Fix List

1. **[HIGH] Add access control to `writeOff()`** — restrict to `msg.sender == address(this)` (callable only via `liquidate()`'s `try this.writeOff()` pattern)
2. **[MEDIUM] Fix `sell()` freePsmAssets accounting** — use `actualAssetOutToSeller` instead of `assetOut` when decrementing `freePsmAssets`
3. **[MEDIUM] Document staleness unwind behavior** — warn operators that the 24h linear unwind allows liquidations at deeply discounted prices; consider adding a position-exit grace period before price unwind begins
4. **[MEDIUM] Fix staker yield cap calculation** — subtract accrued-but-unminted reserves from `totalPaidDebt` before comparing to `totalStaked`
