Skip to content
Quantix Security Labs

Fenwick Lending

Formal Verification of Fenwick Lending, a lending protocol on Arbitrum covered by Quantix Protocol Research. Core accounting, interest accrual and liquidation engine, verified against 12 specified properties.
ResearchPublishedQX-TSA-2026-002 · v1.1
Download Report (PDF)Intelligence profile
Report cover · A4 PDF · 16 pages · 196 KB

Risk summary

State at remediation commit 4e9804ddfe0e

Findings
5
Critical and high
1
Open or partial
0
Remediation
100%

Findings by severity

  • Critical0
  • High1
  • Medium2
  • Low1
  • Informational1

Remediation statusAnalysis

  • Resolved3
  • Partially resolved0
  • Acknowledged2
  • Open0

Fenwick Lending

Lending

Document
QX-TSA-2026-002 · v1.1
Type
Formal Verification
Review
31 Aug 2026 – 18 Sept 2026
Published
30 Sept 2026
Ecosystems
Arbitrum
Languages
Solidity
Risk Index
AA86.9
Assessment contents · 12 sections

01

Assessment overview

Fenwick Lending is an isolated-market, over-collateralised lending protocol on Arbitrum. This engagement verified properties whose violation would create bad debt or move value between suppliers and borrowers without a corresponding action.

Twelve properties were specified with the protocol team and checked with an SMT-based prover. Eight were proved on the original commit. Three were violated, each with a concrete counterexample that became a finding (FL-01 to FL-03); all three were fixed and re-proved on the remediation commit. One property holds only for bounded executions and one is an explicit assumption about oracle freshness.

Results hold under the stated assumptions, most importantly that oracle prices are positive, fresh and not served during sequencer downtime. Those assumptions are part of the result and must be monitored in production.

02

Technical analysis: protocol architecture

Each market pairs one collateral asset with one debt asset. MarketCore tracks cash, total borrows, reserves and per-account balances; suppliers hold an exchange-rate-based claim on the pool, borrowers hold debt indexed by a global borrow index.

InterestRateModel returns borrow and supply rates from utilisation with a kink: rates rise slowly to the kink, then steeply. Interest accrues lazily on every state-changing call.

LiquidationEngine checks account health against the market’s liquidation threshold and lets anyone repay part of an unhealthy account’s debt in exchange for collateral plus an incentive, capped by a close factor. OracleRouter provides prices and rejects stale or sequencer-down rounds.

Trusted· 4

Assumed to behave as specified; compromise is out of the threat model.

  • MarketCoreBalances, exchange rate, borrow index, accrual
  • InterestRateModelKinked utilisation-based rates
  • LiquidationEngineHealth checks and partial liquidations
  • ReserveManagerReserve accounting and withdrawals
trust boundary

Semi-trusted· 2

Trusted for liveness or within bounds; misbehaviour is partly modelled.

  • OracleRouterPrice feeds with staleness and sequencer checks
  • Arbitrum sequencerTransaction ordering on L2
trust boundary

Untrusted· 1

May act adversarially; every input is validated.

  • LiquidatorsPermissionless liquidation callers
Components grouped by trust level. Calls that cross a trust boundary are where the review concentrated input validation and authorisation checks.

Trust assumptions

  • Oracle prices are positive, no older than the feed heartbeat, and not consumed while the L2 sequencer is down or within its grace period (P-12).
  • The reserve admin is a timelocked multisig; its key is not compromised.
  • Collateral and debt assets are standard ERC-20 tokens without fees on transfer or rebasing.

03

Scope

Core accounting, interest accrual and liquidation engine, verified against 12 specified properties.

Repository
github.com/example-org/fenwick-lending
Review effort
Two verification engineers, fifteen working days
Reviewed commit
0ce97e1de9ab9b08986888c883206cffe98ee76f
Remediation commit
4e9804ddfe0e800b1dc64b0b4f1f166e5b2d904c
Files and components in scope
PathDescriptionnSLOC
src/MarketCore.solSupply, borrow, repay and withdraw; exchange-rate accounting538
src/InterestRateModel.solUtilisation-based borrow and supply rates with a kink96
src/LiquidationEngine.solHealth checks, close factor, incentive and collateral seizure274
src/ReserveManager.solProtocol reserves and reserve withdrawals88
spec/Formal specification, harnesses and rule files (handed over to the protocol team)–
Total5 items996

Out of scope

  • OracleRouter (sequencer-uptime and staleness checks are an explicit assumption, P-12)
  • Governance and timelock contracts
  • Off-chain liquidation bots and keepers
  • Market listing and risk-parameter selection

04

Threat model

Each threat lists the actor, the vector and the mitigation, and links to the findings that realised it in the reviewed code.

Assets at risk

  • Supplier deposits and accrued interest
  • Borrower collateral
  • Protocol reserves
  • Market solvency (no unbacked debt)

Actors

  • BorrowerUntrustedSupplies collateral, borrows, repays
  • LiquidatorUntrustedLiquidates unhealthy accounts for an incentive
  • Reserve adminTrustedWithdraws protocol reserves
  • Oracle reportersSemi-trustedPublish prices consumed by the market
Threats, vectors, mitigations and related findings
ThreatActorVectorMitigationFindings
Unbacked debt inflates supplier exchange rateLiquidatorLiquidation that seizes all collateral but leaves debtWrite off residual debt in the same callFL-01
Reserve admin withdraws supplier fundsReserve adminWithdrawal bounded only by cashBound withdrawals by accumulated reservesFL-02
User funds stranded by over-repaymentBorrowerRepay on behalf with amount above debtCap transfer at outstanding debtFL-03
Solvency checks using stale pricesOracle reportersStale round or sequencer downtimeOracleRouter checks (assumed, out of scope)FL-05

05

Findings

Severity

5 findings

FL-01HighResolvedBusiness logic

Partial liquidation can leave debt with no collateral and no write-off

src/LiquidationEngine.sol:L118–L164

Likelihood
Medium
Impact
High
Weakness
CWE-682
Description

Property P-05 failed. When an account’s collateral value is close to its debt, the engine computes collateral to seize as repay × (1 + incentive) / price, rounds it up, and only afterwards applies the close-factor cap to the repay amount.

The prover produced a sequence in which the rounded seizure equals the account’s entire collateral while the capped repayment covers only part of the debt. The account ends with zero collateral and positive debt. Nothing marks the remainder as bad debt, so it stays in totalBorrows and keeps accruing interest.

Because the supplier exchange rate is computed from cash + totalBorrows − totalReserves, phantom debt inflates the rate that suppliers redeem at.

Preconditions
  • An account becomes undercollateralised close to the liquidation boundary
  • A liquidator repays the maximum allowed by the close factor
Exploit scenario
  1. 1.Collateral price drops so that an account’s collateral is worth slightly more than its debt.
  2. 2.A liquidator repays the close-factor maximum and seizes collateral including the incentive.
  3. 3.Rounding makes the seizure equal to all remaining collateral; residual debt remains.
  4. 4.Residual debt accrues interest; suppliers who withdraw early are paid from value that does not exist.
Impact

Unbacked debt inflates the exchange rate. Early withdrawers are overpaid and the shortfall falls on the last suppliers to exit. Each occurrence is small, but they accumulate in volatile markets.

Recommendation

When a liquidation reduces collateral to zero, write off the remaining debt against reserves (or socialise it explicitly) in the same call and emit an event. Compute the close-factor cap before the incentive.

Fix
src/LiquidationEngine.soldiff
       uint256 seize = _collateralToSeize(repayCapped);       _seize(borrower, liquidator, seize);+      if (collateralOf(borrower) == 0 && debtOf(borrower) > 0) {+          uint256 bad = debtOf(borrower);+          _writeOffAgainstReserves(borrower, bad);+          emit BadDebtRealised(borrower, bad);+      }
Resolution

Residual debt is written off against reserves in the same transaction and BadDebtRealised is emitted. P-05 re-proved.

References
FL-02MediumResolvedAccess control

Reserve withdrawal is bounded by cash, not by accumulated reserves

src/ReserveManager.sol:L57

Likelihood
Low
Impact
High
Weakness
CWE-284
Description

Property P-02 failed. withdrawReserves(amount) checks amount <= cash but not amount <= totalReserves. The prover produced a counterexample in which the reserve admin withdraws more than the protocol has accumulated, taking supplier cash and reducing the exchange rate.

The function is restricted to the reserve admin (P-08 proved), so this is not exploitable by arbitrary users. It does mean that the reserve role is effectively able to withdraw all market liquidity, which is a larger privilege than documented.

Preconditions
  • The reserve admin key is compromised or makes an error
Exploit scenario
  1. 1.Reserve admin calls withdrawReserves(cash).
  2. 2.Cash is transferred out; totalReserves becomes negative in effect; the exchange rate drops.
Impact

A compromised or mistaken reserve admin can transfer supplier funds out of the market.

Recommendation

Require amount <= totalReserves and decrement reserves before transferring.

Fix
src/ReserveManager.soldiff
   function withdrawReserves(uint256 amount) external onlyReserveAdmin {-      require(amount <= cash(), "cash");+      if (amount > totalReserves) revert ExceedsReserves(amount, totalReserves);+      totalReserves -= amount;       asset.safeTransfer(reserveAdmin, amount);   }
Resolution

Bound added and reserves decremented before transfer. P-02 re-proved.

References
FL-03MediumResolvedBusiness logic

Repaying on behalf of another account can strand surplus tokens

src/MarketCore.sol:L301–L327

Likelihood
Medium
Impact
Medium
Weakness
CWE-682
Description

Property P-06 failed. repayBorrowBehalf(borrower, amount) transfers amount from the caller in full but reduces the borrower’s debt by at most the outstanding balance. Any surplus stays in the contract as unaccounted cash.

Integrations commonly pass a slightly larger amount than the quoted debt to cover interest that accrues before execution, so the surplus case is routine rather than exotic.

Preconditions
  • Caller passes an amount above the outstanding debt
Exploit scenario
  1. 1.A repayment helper sends debt + 1% buffer.
  2. 2.The buffer is transferred in but not credited; the caller loses it.
Impact

Users who over-repay lose the surplus. Unaccounted cash also breaks P-01 until it is swept.

Recommendation

Cap the transferred amount at the outstanding debt and support type(uint256).max as "repay all".

Fix
src/MarketCore.soldiff
   function repayBorrowBehalf(address borrower, uint256 amount) external {       _accrue();-      asset.safeTransferFrom(msg.sender, address(this), amount);-      _reduceDebt(borrower, Math.min(amount, debtOf(borrower)));+      uint256 owed = debtOf(borrower);+      uint256 pay = amount == type(uint256).max ? owed : Math.min(amount, owed);+      asset.safeTransferFrom(msg.sender, address(this), pay);+      _reduceDebt(borrower, pay);   }
Resolution

Amount capped before transfer. P-06 re-proved.

References
FL-04LowAcknowledgedPrecision and rounding

Borrow rate decreases by one unit at the kink due to integer division

src/InterestRateModel.sol:L44–L61

Likelihood
Low
Impact
Low
Weakness
CWE-682
Description

P-07 was provable only after excluding a one-unit discontinuity at the kink. The two branches of the rate formula divide in a different order, so the rate immediately above the kink can be one unit lower than immediately below it.

The effect on interest paid is negligible, but it contradicts the documented monotonicity of the model, which integrators may rely on when computing rate bounds.

Preconditions
  • Utilisation exactly at the kink boundary
Exploit scenario
  1. 1.Utilisation moves across the kink; the rate drops by one unit instead of rising.
Impact

Negligible economic effect. Recorded because it contradicts the documented model.

Recommendation

Compute both branches with the same operation order, or document the tolerance in the specification.

Resolution

Acknowledged. The tolerance is documented in the specification and P-07 is stated with it.

References
FL-05InformationalAcknowledgedConfiguration

Verification relies on fresh prices and sequencer availability

spec/assumptions.md

Likelihood
Low
Impact
Medium
Description

Solvency properties are proved under assumption P-12: oracle prices are positive, updated within the heartbeat, and not consumed while the Arbitrum sequencer is down or inside the grace period after it restarts. MarketCore does not enforce these conditions itself; it relies on OracleRouter, which was out of scope.

During sequencer downtime, prices on L2 can lag L1 markets significantly, and liquidations or borrows executed immediately after restart may use stale values.

Preconditions
  • OracleRouter misconfigured or bypassed
  • Sequencer outage
Exploit scenario
  1. 1.Sequencer goes down while collateral prices fall on L1.
  2. 2.On restart, borrows execute against stale, higher prices before feeds update.
Impact

If the assumption fails in production, the solvency results do not apply.

Recommendation

Enforce staleness, positivity and sequencer-uptime checks at the market level as defence in depth, and monitor feed heartbeats and the sequencer uptime feed.

Resolution

Acknowledged. An on-chain staleness check in MarketCore is planned for the next release; monitoring is in place.

References

06

Severity

5findings
  • Critical0 · 0%
  • High1 · 20%
  • Medium2 · 40%
  • Low1 · 20%
  • Informational1 · 20%

By vulnerability class

  • Business logic2
  • Access control1
  • Configuration1
  • Precision and rounding1

Likelihood and impact

Each finding placed by the likelihood of its preconditions and the impact of exploitation.

Findings by likelihood (columns) and impact (rows)
Impact ↓ / Likelihood →LowMediumHigh
High
1
1
0
Medium
1
1
0
Low
1
0
0

07

Remediation

3 of 5 findings are resolved, 2 acknowledged, 0 partially resolved and 0 open at remediation commit 4e9804ddfe0e.

Remediation progress100%

Resolved and acknowledged findings count fully; partially resolved findings count half.

100%remediated
  • Resolved3 · 60%
  • Partially resolved0 · 0%
  • Acknowledged2 · 40%
  • Open0 · 0%
Findings by severity and remediation status
SeverityResolvedPartially resolvedAcknowledgedOpenTotal
Critical00000
High10001
Medium20002
Low00101
Informational00101
All findings30205

Residual items

  • FL-04LowAcknowledgedAcknowledged. The tolerance is documented in the specification and P-07 is stated with it.
  • FL-05InformationalAcknowledgedAcknowledged. An on-chain staleness check in MarketCore is planned for the next release; monitoring is in place.
  • ResolvedFixed and verified in the remediation review.
  • Partially resolvedMitigated; the residual risk is documented.
  • AcknowledgedAccepted by the protocol team with a stated rationale.
  • OpenNot yet addressed at the reviewed remediation commit.

08

Formal verification

Twelve properties were specified. Results below are final, on the remediation commit. Properties violated on the original commit are marked in their notes with the finding they produced.

Tool: SMT-based prover with bounded model checking fallback

  • P-01Provedcash + totalBorrows − totalReserves = Σ supplierAssets
  • P-02Proved¬badDebtEvent ⇒ exchangeRate′ ≥ exchangeRateViolated on the original commit (FL-02); re-proved after the fix.
  • P-03ProvedborrowIndex′ ≥ borrowIndex
  • P-04Provedhealth(a) ≥ 1 ⇒ liquidate(a) reverts
  • P-05Proveddebt(a) > 0 ∧ collateral(a) = 0 ⇒ isBadDebt(a)Violated on the original commit (FL-01); re-proved after the fix.
  • P-06ProvedtransferIn(repay) ≤ debt(a)Violated on the original commit (FL-03); re-proved after the fix.
  • P-07Provedu₁ ≤ u₂ ⇒ rate(u₁) ≤ rate(u₂), within one unit at the kinkProved with a documented one-unit tolerance (FL-04).
  • P-08ProvedwithdrawReserves ⇒ msg.sender = reserveAdmin
  • P-09Provedwithdraw(a, x) ⇒ x ≤ redeemable(a)
  • P-10Inconclusiveaccrue(t₀→t₂) ≈ accrue(t₀→t₁→t₂) within 1 wei per stepHolds for sequences up to 8 accruals; the prover timed out for unbounded sequences.
  • P-11Provedpaused ⇒ supply, borrow and withdraw revert
  • P-12Not in scopeprice > 0 ∧ now − updatedAt ≤ heartbeat ∧ sequencerUpAssumption about OracleRouter, not proved (FL-05).

A proved property holds for every execution of the model under its stated assumptions. Fuzzing and property-based results are evidence, not proofs, and are recorded as inconclusive.

09

Recommendations

  1. 01

    Run the specification in CI

    The rule files were handed over with the report. Re-running them on every change to MarketCore or LiquidationEngine keeps the proofs valid as the code evolves.

  2. 02

    Close the P-10 gap

    Path-independence of accrual was proved only for bounded sequences. Either restructure accrual to make it provable, or add a fuzzing campaign targeting long accrual chains.

  3. 03

    Verify OracleRouter next

    Solvency depends on P-12. Extending verification to OracleRouter turns the largest assumption into a result.

  4. 04

    Document the reserve admin’s power

    Even with FL-02 fixed, the reserve admin controls protocol revenue. Publish the role, its holder and its timelock.

10

Methodology and limitations

  1. 01Requirements workshop with the protocol team to agree properties in plain language before formalisation
  2. 02Formal specification of 12 properties covering solvency, conservation, monotonicity and access control
  3. 03Verification with an SMT-based prover over unbounded state; bounded model checking where the prover timed out
  4. 04Mutation testing of the specification: each rule was shown to fail against a deliberately broken implementation
  5. 05Counterexample analysis and minimisation for every violated property
  6. 06Re-verification of all properties against the remediation commit

Severity classification

Critical
Direct loss of funds or permanent loss of control is achievable with little or no precondition.
High
Material loss or protocol disruption is achievable under realistic conditions.
Medium
Limited loss, degraded functionality, or impact that depends on specific conditions.
Low
Minor impact, defence-in-depth gaps, or issues with unlikely preconditions.
Informational
Code quality, documentation or best-practice observations without direct security impact.

Limitations

  • Results are proofs about a model of the contracts listed in scope, under the stated assumptions. They are not proofs about the deployed system as a whole.
  • Properties not written in the specification were not verified. The absence of a property is not evidence of safety.
  • P-10 was verified only up to bounded sequences of accruals and is reported as inconclusive for unbounded executions.
  • OracleRouter, governance contracts and off-chain liquidation bots were out of scope.

No assessment can show that a system is free of vulnerabilities. This research assessment reflects the code at the commits listed. Quantix methodology

11

Technical appendix

Tools

  • SMT-based proverUnbounded verification of the 12 properties
  • Bounded model checkerP-10 within bounded accrual sequences
  • Specification mutation testingConfirming each rule can fail
  • FoundryReproducing counterexamples as concrete tests
Reviewed files (SHA-256) · 4 files
SHA-256 hashes of reviewed files
FileSHA-256
src/MarketCore.solc54cb07c0aba4a3ea6ba67b9633c0fd63a7724c3340b947b36acfa66197504e6
src/InterestRateModel.sol7f898e092957f93aef5ab1f1affe65c1543d40187ff7e52cf0f69f6ec595384d
src/LiquidationEngine.solf4751a07029d64694957c9b48d8a575d598b14d725ec7017e58a16b90e40c60e
src/ReserveManager.sola70d4065728b0143fd035ead5e47bf2da9e15cde6d01b63fa28bebe6fe254352

Notes

  • Every counterexample was replayed as a Foundry test that fails on the original commit and passes on the remediation commit.
  • The specification uses the notation: x′ for post-state, Σ for summation over all accounts.

Technical references

  1. 1.CWE-682: Incorrect Calculation (opens in a new tab)
  2. 2.CWE-284: Improper Access Control (opens in a new tab)
  3. 3.Solidity: integer division semantics (opens in a new tab)
  4. 4.Chainlink: L2 sequencer uptime feeds (opens in a new tab)

Quantix Technical Security Assessment QX-TSA-2026-002

Version 1.1, published 30 Sept 2026. A4 PDF generated from this assessment record.

Download Report

12

Report history

  1. 31 Aug 2026Review openedReviewed commit 0ce97e1de9ab in github.com/example-org/fenwick-lending
  2. 18 Sept 2026Review closedTwo verification engineers, fifteen working days
  3. After reviewRemediation reviewFixes checked at commit 4e9804ddfe0e
  4. 30 Sept 2026Version 1.1 publishedQX-TSA-2026-002, A4 PDF generated from this record
All security assessments

Commission an assessment written to be verified.

Share the repository and the commit you plan to deploy. We reply with scoping questions and an estimate.

Request an AuditSee the methodology