Designing DeFi Resilience: Inside Aave V4’s Security Blueprint
三句話摘要
Aave v4 採用「中心-輻條」新架構，並透過風險溢價與形式化驗證（Proof-Driven Development）大幅提升協議安全性與可擴展性。 Aave v4 最值得記住的是「把問題重新表述」的工程思維——無論是用加法取代除法消除舍入誤差，還是用形式化驗證取代事後審計，核心都是在設計階段就精確定義「正確」的數學含義，而非等到出問題才修補。 1. 模組化架構解決資產類別擴展問題
重點整理
重點- 1
1. 模組化架構解決資產類別擴展問題
- 2
v3 將流動性供應與借貸策略綁在同一合約，導致新資產類別（如 RWA、LP 代幣）難以接入。v4 將兩者拆開：Hub 只追蹤總供應、總借款與負債，任何符合介面的 Spoke 都可即插即用，從根本上降低了新市場冷啟動的門檻。
- 3
2. 風險溢價讓借貸成本反映真實風險
- 4
過去 v3 中，使用高風險抵押品（如 LP 代幣）與低風險抵押品（如 ETH）的借款人支付相同利率，實質上由低風險借款人補貼高風險方。v4 針對每個借款人設定個別風險係數，使利率精確對應抵押品風險，同時激勵借款人選擇低風險抵押品。
- 5
3. 用「溢價本金加法」取代加權平均除法
- 6
計算全系統加權平均風險溢價時，除法會累積舍入誤差，每次操作都使精度下降。v4 的解法是將風險百分比轉換為額外本金（溢價債務），用加法累加取代除法，使 Hub 狀態與單一用戶狀態完全一致、精確無誤差。
- 7
4. 形式化驗證（Proof-Driven Development）加速安全開發
- 8
開發初期就與 Certora 合作，以英語定義協議屬性，再用 CVL（Certora Verification Language）形式化為數學公式，讓 Prover 自動檢查。這個迭代流程能在設計階段即發現邏輯漏洞，而非等到審計時才修補。
實用技巧與重點
乾貨- 數字與計算
- 範例基準利率：5%；抵押品風險係數：40%；有效利率：5% × 1.4 = 7%
- Alice：債務 1,000，風險 10%，溢價債務 100
- Bob：債務 2,000，風險 30%，溢價債務 600
- 加權平均（舊方法）：(1000×10% + 2000×30%) ÷ 3000 = 23.33%（有舍入誤差）
- 加法總計（新方法）：100 + 600 = 700（精確，Alice 還款後剩 600 = Bob 的溢價債務，完全正確）
- 工具與平台
- Certora Prover（符號引擎，用於形式化驗證）
- CVL（Certora Verification Language）
- Z3（輕量級 SMT Solver，適合快速驗證較小程式碼片段）
- 架構元件
- Hub（中心）：追蹤總供應量、總借款量、總負債，極簡合約
- Spoke（輻條）：任意借貸策略或流動性使用邏輯，即插即用
- Share Rate = 總資產 ÷ 總份額（v4 使用份額率而非指數）
- 核心不變性（已形式化驗證）
- Share Rate 不可下降（任何操作後 share rate ≥ 操作前）
- 這等價於：協議永遠有償付能力，且任何人無法從協議中竊取資金
- 開發建議
- 儘早（設計階段）介入審計人員
- 兩個關鍵時間點定義屬性：「知道要做什麼」時 + 「知道怎麼做」時
- 先寫協議原型，快速迭代，再形式化驗證
- 使用 Z3 驗證舍入方向是否對協議有利
結論
結論“Aave v4 最值得記住的是「把問題重新表述」的工程思維——無論是用加法取代除法消除舍入誤差，還是用形式化驗證取代事後審計，核心都是在設計階段就精確定義「正確」的數學含義，而非等到出問題才修補。”
完整解析
詳細Aave v4 的核心問題意識起源於 v3 的架構限制。在 v3 中，每個市場都是獨立合約，流動性供應與借貸策略緊密耦合，導致每當需要支援新資產類別（如現實世界資產 RWA 或 Uniswap LP 代幣），都必須從零啟動一個全新市場並重新引導流動性。v4 的解法是引入「Hub-Spoke」架構：Hub 作為中央流動性池，只負責記錄總供應量、總借款量與總負債，保持極度簡潔；Spoke 則是各種借貸策略或流動性使用邏輯，任何符合 Hub 介面的 Spoke 都可以直接接入，不需要額外實作。這意味著未來的 LP 代幣抵押、期權市場保證金、甚至非傳統借貸場景，都可以作為新 Spoke 插入現有流動性池，大幅降低新市場的冷啟動成本。
在借貸定價上，v3 的一個隱性不公平問題被 v4 正式解決。過去所有借款人支付相同利率，但使用高風險抵押品（如 LP 代幣，具有智能合約風險與定價風險）的借款人實際上讓低風險借款人（如使用 ETH 者）替其承擔尾部風險。v4 引入「風險溢價」機制：風險管理人員為每種抵押品定義風險係數，借款人的實際利率依此係數調整，使成本與風險真正對應。這同時激勵借款人選擇低風險抵押品，並讓流動性供應商獲得與其承擔風險相稱的收益。
然而，要在 Hub 層面計算所有借款人的加權平均風險，直接使用除法會帶來精度問題。每次加減用戶時的除法運算都會引入舍入誤差，隨著用戶數量增加，誤差累積最終導致系統狀態不一致。v4 的數學創新在於「問題重新表述」：與其在利率百分比上做加權平均，不如將風險係數轉換為額外本金（溢價債務），整個系統只需對溢價債務做加減法，完全迴避除法。Alice 還款後，Hub 的狀態精確等於 Bob 的溢價債務，沒有任何舍入誤差——這個數學等價性是確保系統長期精確的關鍵。
在安全實踐層面，開發團隊 Sttor 採用了「Proof-Driven Development」範式。他們在設計初期即與 Certora 合作，將協議期望的安全屬性（如「Hub 永遠有償付能力」）先以英語描述，再用 CVL 形式化為數學公式，讓 Certora Prover 自動驗證。核心的已驗證不變性是：在任何操作後，share rate（總資產 ÷ 總份額）不可下降。這個屬性等價於沒有人能從協議中竊取資金；一旦有惡意函數嘗試抽走資金，Prover 立刻標記違反。這套流程的重要性在於，它讓模組化架構的安全驗證可以快速複用：每當設計新的 Spoke，只需遵循 Hub 的介面並跑一次 Prover，即可確認新設計是否破壞核心不變性，大幅縮短迭代週期。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
