diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
new file mode 100644
index 000000000..07be11780
--- /dev/null
+++ b/.github/workflows/certora.yml
@@ -0,0 +1,32 @@
+name: certora
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        conf:
+          - Terms
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+      - name: Install certora
+        run: pip install certora-cli
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.28/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc-0.8.28
+      - name: Verify ${{ matrix.conf }}
+        run: certoraRun certora/${{ matrix.conf }}.conf
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
diff --git a/.github/workflows/forge.yml b/.github/workflows/forge.yml
new file mode 100644
index 000000000..487799b5a
--- /dev/null
+++ b/.github/workflows/forge.yml
@@ -0,0 +1,21 @@
+name: forge
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  foundry:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+      - name: Check formatting
+        run: forge fmt --check
+      - name: Run Forge tests
+        run: forge test
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 000000000..5280472af
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,3 @@
+cache
+out
+.certora_internal
diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 000000000..888d42dcd
--- /dev/null
+++ b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "lib/forge-std"]
+	path = lib/forge-std
+	url = https://github.com/foundry-rs/forge-std
diff --git a/certora/Terms.conf b/certora/Terms.conf
new file mode 100644
index 000000000..672d93437
--- /dev/null
+++ b/certora/Terms.conf
@@ -0,0 +1,16 @@
+{
+  "files": [
+    "certora/helpers/TermsHelpers.sol",
+    "certora/dispatch/ERC20Standard.sol"
+  ],
+  "solc": "solc-0.8.28",
+  "verify": "TermsHelpers:certora/Terms.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "optimistic_hashing": true,
+  "solc_via_ir": true,
+  "hashing_length_bound": "320",
+  "msg": "Terms" 
+}
diff --git a/certora/Terms.spec b/certora/Terms.spec
new file mode 100644
index 000000000..446a6ee20
--- /dev/null
+++ b/certora/Terms.spec
@@ -0,0 +1,56 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+/// METHODS ///
+
+methods {
+    function withdrawable(bytes32 id) external returns uint256 envfree;
+    function balanceOf(address, address) external returns uint256 envfree;
+    function id(Terms.Term) external returns bytes32 envfree;
+
+    // function _.transfer(address, uint256) external => DISPATCHER(true);
+    // function _.transferFrom(address, address, uint256) external => DISPATCHER(true);
+    // function _.balanceOf(address) external => DISPATCHER(true);
+}
+
+/// HOOKS ///
+
+persistent ghost mapping(bytes32 => mathint) sumBondSharesOf {
+    init_state axiom (forall bytes32 id. sumBondSharesOf[id] == 0);
+}
+hook Sload uint256 bondSharesOfOwner bondSharesOf[KEY address owner][KEY bytes32 id] {
+    require sumBondSharesOf[id] >= to_mathint(bondSharesOfOwner);
+}
+hook Sstore bondSharesOf[KEY address owner][KEY bytes32 id] uint256 newBondShares (uint256 oldBondShares) {
+    sumBondSharesOf[id] = sumBondSharesOf[id] - oldBondShares + newBondShares;
+}
+
+persistent ghost mapping(bytes32 => mathint) sumDebtOf {
+    init_state axiom (forall bytes32 id. sumDebtOf[id] == 0);
+}
+hook Sload uint256 debtOfOwner debtOf[KEY address owner][KEY bytes32 id] {
+    require sumDebtOf[id] >= to_mathint(debtOfOwner);
+}
+hook Sstore debtOf[KEY address owner][KEY bytes32 id] uint256 newDebt (uint256 oldDebt) {
+    sumDebtOf[id] = sumDebtOf[id] - oldDebt + newDebt;
+}
+
+/// SANITY ///
+
+invariant sanitySumBondShares(bytes32 id)
+    sumBondSharesOf[id] >= 0;
+    
+invariant sanitySumDebt(bytes32 id)
+    sumDebtOf[id] >= 0;
+
+rule satisfyMatch(env e, calldataarg args) {
+    MATCH(e, args);
+    satisfy true;
+}
+
+/// INVARIANTS ///
+
+// strong invariant sums(bytes32 id)
+//     sumBondOf[id] == sumDebtOf[id] + withdrawable(id);
+
+// invariant balances(TermsHelpers.Term term)
+//     balanceOf(term.loanToken, currentContract) >= withdrawable(id(term));
diff --git a/certora/dispatch/ERC20NoRevert.sol b/certora/dispatch/ERC20NoRevert.sol
new file mode 100644
index 000000000..b8dfccd1e
--- /dev/null
+++ b/certora/dispatch/ERC20NoRevert.sol
@@ -0,0 +1,48 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity ^0.8.0;
+
+contract ERC20NoRevert {
+    address public owner;
+    uint256 public totalSupply;
+    mapping(address => uint256) public balanceOf;
+    mapping(address => mapping(address => uint256)) public allowance;
+
+    constructor() {
+        owner = msg.sender;
+    }
+
+    modifier onlyOwner() {
+        require(msg.sender == owner);
+        _;
+    }
+
+    function _transfer(address _from, address _to, uint256 _amount) internal returns (bool) {
+        if (balanceOf[_from] < _amount) {
+            return false;
+        }
+        balanceOf[_from] -= _amount;
+        balanceOf[_to] += _amount;
+        return true;
+    }
+
+    function transfer(address _to, uint256 _amount) public returns (bool) {
+        return _transfer(msg.sender, _to, _amount);
+    }
+
+    function transferFrom(address _from, address _to, uint256 _amount) public returns (bool) {
+        if (allowance[_from][msg.sender] < _amount) {
+            return false;
+        }
+        allowance[_from][msg.sender] -= _amount;
+        return _transfer(_from, _to, _amount);
+    }
+
+    function approve(address _spender, uint256 _amount) public {
+        allowance[msg.sender][_spender] = _amount;
+    }
+
+    function mint(address _receiver, uint256 _amount) public onlyOwner {
+        balanceOf[_receiver] += _amount;
+        totalSupply += _amount;
+    }
+}
diff --git a/certora/dispatch/ERC20Standard.sol b/certora/dispatch/ERC20Standard.sol
new file mode 100644
index 000000000..71af6d9ca
--- /dev/null
+++ b/certora/dispatch/ERC20Standard.sol
@@ -0,0 +1,42 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity ^0.8.0;
+
+contract ERC20Standard {
+    address public owner;
+    uint256 public totalSupply;
+    mapping(address => uint256) public balanceOf;
+    mapping(address => mapping(address => uint256)) public allowance;
+
+    constructor() {
+        owner = msg.sender;
+    }
+
+    modifier onlyOwner() {
+        require(msg.sender == owner);
+        _;
+    }
+
+    function _transfer(address _from, address _to, uint256 _amount) internal returns (bool) {
+        balanceOf[_from] -= _amount;
+        balanceOf[_to] += _amount;
+        return true;
+    }
+
+    function transfer(address _to, uint256 _amount) public returns (bool) {
+        return _transfer(msg.sender, _to, _amount);
+    }
+
+    function transferFrom(address _from, address _to, uint256 _amount) public returns (bool) {
+        allowance[_from][msg.sender] -= _amount;
+        return _transfer(_from, _to, _amount);
+    }
+
+    function approve(address _spender, uint256 _amount) public {
+        allowance[msg.sender][_spender] = _amount;
+    }
+
+    function mint(address _receiver, uint256 _amount) public onlyOwner {
+        balanceOf[_receiver] += _amount;
+        totalSupply += _amount;
+    }
+}
diff --git a/certora/dispatch/ERC20USDT.sol b/certora/dispatch/ERC20USDT.sol
new file mode 100644
index 000000000..cce99353a
--- /dev/null
+++ b/certora/dispatch/ERC20USDT.sol
@@ -0,0 +1,45 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity ^0.8.0;
+
+contract ERC20USDT {
+    address public owner;
+    uint256 public totalSupply;
+    mapping(address => uint256) public balanceOf;
+    mapping(address => mapping(address => uint256)) public allowance;
+
+    constructor() {
+        owner = msg.sender;
+    }
+
+    modifier onlyOwner() {
+        require(msg.sender == owner);
+        _;
+    }
+
+    function _transfer(address _from, address _to, uint256 _amount) internal {
+        balanceOf[_from] -= _amount;
+        balanceOf[_to] += _amount;
+    }
+
+    function transfer(address _to, uint256 _amount) public {
+        _transfer(msg.sender, _to, _amount);
+    }
+
+    function transferFrom(address _from, address _to, uint256 _amount) public {
+        if (allowance[_from][msg.sender] < type(uint256).max) {
+            allowance[_from][msg.sender] -= _amount;
+        }
+        _transfer(_from, _to, _amount);
+    }
+
+    function approve(address _spender, uint256 _amount) public {
+        require(!((_amount != 0) && (allowance[msg.sender][_spender] != 0)));
+
+        allowance[msg.sender][_spender] = _amount;
+    }
+
+    function mint(address _receiver, uint256 _amount) public onlyOwner {
+        balanceOf[_receiver] += _amount;
+        totalSupply += _amount;
+    }
+}
diff --git a/certora/helpers/TermsHelpers.sol b/certora/helpers/TermsHelpers.sol
new file mode 100644
index 000000000..221b4287d
--- /dev/null
+++ b/certora/helpers/TermsHelpers.sol
@@ -0,0 +1,14 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.0;
+
+import {Terms, Term, IERC20} from "../../src/Terms.sol";
+
+contract TermsHelpers is Terms {
+    function balanceOf(address token, address account) external view returns (uint256) {
+        return IERC20(token).balanceOf(account);
+    }
+
+    function id(Term memory term) external pure returns (bytes32) {
+        return _id(term);
+    }
+}
diff --git a/foundry.toml b/foundry.toml
new file mode 100644
index 000000000..e9c314cdc
--- /dev/null
+++ b/foundry.toml
@@ -0,0 +1,2 @@
+[profile.default]
+via_ir = true
diff --git a/lib/forge-std b/lib/forge-std
new file mode 160000
index 000000000..b93cf4bc3
--- /dev/null
+++ b/lib/forge-std
@@ -0,0 +1 @@
+Subproject commit b93cf4bc34ff214c099dc970b153f85ade8c9f66
diff --git a/src/Terms.sol b/src/Terms.sol
new file mode 100644
index 000000000..d1affdbd6
--- /dev/null
+++ b/src/Terms.sol
@@ -0,0 +1,277 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity 0.8.28;
+
+import "./libraries/UtilsLib.sol";
+import {MathLib, WAD} from "./libraries/MathLib.sol";
+import {SharesMathLib} from "./libraries/SharesMathLib.sol";
+import "./interfaces/IERC20.sol";
+import "./interfaces/IOracle.sol";
+import "./interfaces/ITerms.sol";
+import "./interfaces/IMorphoLiquidationCallback.sol";
+
+contract Terms is ITerms {
+    using MathLib for uint256;
+    using SharesMathLib for uint256;
+
+    /// CONSTANTS ///
+
+    bytes32 public constant DOMAIN_TYPEHASH = keccak256("EIP712Domain(uint256 chainId,address verifyingContract)");
+    bytes32 public constant OFFER_TYPEHASH = keccak256(
+        "Offer(bool lend,address offering,uint256 assets,address loanToken,Collateral[] collaterals,uint256 maturity,uint256 price)"
+    );
+
+    uint256 public constant ORACLE_PRICE_SCALE = 1e36;
+
+    /// STORAGE ///
+
+    // Terms.
+    mapping(address => mapping(bytes32 => uint256)) public bondSharesOf;
+    mapping(address => mapping(bytes32 => uint256)) public debtOf;
+    mapping(bytes32 => uint256) public withdrawable;
+    mapping(bytes32 => uint256) public totalAssets;
+    mapping(bytes32 => uint256) public totalShares;
+    mapping(address => mapping(bytes32 => mapping(address => uint256))) public collateralOf;
+    // Offers.
+    mapping(bytes => uint256) public consumed;
+
+    /// ENTRY-POINTS ///
+
+    /// @dev This function is used for both primary and secondary markets.
+    function MATCH(Offer memory buyOffer, Signature memory buySig, Offer memory sellOffer, Signature memory sellSig)
+        public
+    {
+        _checkOffers(buyOffer, buySig, sellOffer, sellSig);
+
+        uint256 amount = UtilsLib.min(
+            buyOffer.assets - consumed[abi.encode(buyOffer)], sellOffer.assets - consumed[abi.encode(sellOffer)]
+        );
+        require(amount > 0, "No assets to match");
+        address buyer = buyOffer.offering;
+        address seller = sellOffer.offering;
+
+        consumed[abi.encode(buyOffer)] += amount;
+        consumed[abi.encode(sellOffer)] += amount;
+
+        Term memory term = Term(sellOffer.loanToken, sellOffer.collaterals, sellOffer.maturity);
+        bytes32 id = _id(term);
+
+        uint256 repaid = UtilsLib.min(debtOf[buyer][id], amount);
+        uint256 bought = amount - repaid;
+        uint256 boughtShares = bought.toSharesDown(totalAssets[id], totalShares[id]);
+        debtOf[buyer][id] -= repaid;
+        bondSharesOf[buyer][id] += boughtShares;
+
+        uint256 withdrawn;
+        uint256 withdrawnShares;
+
+        if (bondSharesOf[seller][id].toAssetsDown(totalAssets[id], totalShares[id]) < amount) {
+            withdrawn = bondSharesOf[seller][id].toAssetsDown(totalAssets[id], totalShares[id]);
+            withdrawnShares = bondSharesOf[seller][id];
+        } else {
+            withdrawn = amount;
+            withdrawnShares = amount.toSharesUp(totalAssets[id], totalShares[id]);
+        }
+
+        bondSharesOf[seller][id] -= withdrawnShares;
+        debtOf[seller][id] += amount - withdrawn;
+
+        totalShares[id] += boughtShares;
+        totalShares[id] -= withdrawnShares;
+        totalAssets[id] += bought;
+        totalAssets[id] -= withdrawn;
+
+        require(debtOf[buyer][id] == 0 || _isHealthy(term, buyer), "Buyer is unhealthy");
+        require(debtOf[seller][id] == 0 || _isHealthy(term, seller), "Seller is unhealthy");
+
+        uint256 sellerScaledPrice = sellOffer.price * amount / sellOffer.assets;
+        uint256 buyerScaledPrice = buyOffer.price * amount / buyOffer.assets;
+
+        IERC20(buyOffer.loanToken).transferFrom(buyer, seller, sellerScaledPrice);
+        IERC20(buyOffer.loanToken).transferFrom(buyer, msg.sender, buyerScaledPrice - sellerScaledPrice);
+    }
+
+    /// @dev Will revert if there is no withdrawable funds.
+    function withdrawBond(Term memory term, uint256 amount, uint256 shares, address onBehalf) external {
+        require(UtilsLib.exactlyOneZero(amount, shares), "INCONSISTENT_INPUT");
+        bytes32 id = _id(term);
+
+        if (amount > 0) shares = amount.toSharesUp(totalAssets[id], totalShares[id]);
+        else amount = shares.toAssetsDown(totalAssets[id], totalShares[id]);
+
+        bondSharesOf[onBehalf][id] -= shares;
+        withdrawable[id] -= amount;
+
+        totalShares[id] -= shares;
+        totalAssets[id] -= amount;
+
+        IERC20(term.loanToken).transfer(msg.sender, amount);
+    }
+
+    function repayDebt(Term memory term, uint256 amount, address onBehalf) external {
+        bytes32 id = _id(term);
+
+        debtOf[onBehalf][id] -= amount;
+        withdrawable[id] += amount;
+
+        IERC20(term.loanToken).transferFrom(msg.sender, address(this), amount);
+    }
+
+    function supplyCollateral(Term memory term, address collateral, uint256 amount, address onBehalf) external {
+        collateralOf[onBehalf][_id(term)][collateral] += amount;
+        IERC20(collateral).transferFrom(msg.sender, address(this), amount);
+    }
+
+    function withdrawCollateral(Term memory term, address collateral, uint256 amount, address onBehalf) external {
+        collateralOf[onBehalf][_id(term)][collateral] -= amount;
+
+        require(_isHealthy(term, onBehalf), "Unhealthy borrower");
+
+        IERC20(collateral).transfer(msg.sender, amount);
+    }
+
+    /// @notice Execute the given collection of `seizures` on the given `term` of the given `borrower`.
+    /// @dev On each seizure either `repaidAmounts` or `seizedAssets` should be equal to zero.
+    /// @param term The term of the bond.
+    /// @param seizures An array of amounts of debt to repay or assets to seize with the index of the collateral in the term's collateral assets.
+    /// @param borrower The debtor of the loan.
+    /// @param data Arbitrary data to pass to the callback. Pass empty data if not needed.
+    /// @return A collection of the actual amounts of debt repaid or asset seized with the collateral index.
+    function liquidate(Term memory term, Seizure[] memory seizures, address borrower, bytes calldata data)
+        external
+        returns (Seizure[] memory)
+    {
+        require(seizures.length == term.collaterals.length, "should have all collats");
+
+        bytes32 id = _id(term);
+        uint256 liquidationIncentiveFactor = 1.15e18;
+
+        uint256 maxDebt;
+        uint256 repayableDebt;
+
+        for (uint256 i = 0; i < term.collaterals.length; i++) {
+            uint256 price = IOracle(term.collaterals[i].oracle).price();
+            uint256 collateralQuoted =
+                collateralOf[borrower][id][term.collaterals[i].token].mulDivDown(price, ORACLE_PRICE_SCALE);
+            maxDebt += collateralQuoted.wMulDown(term.collaterals[i].lltv);
+            repayableDebt += collateralQuoted.wDivUp(liquidationIncentiveFactor);
+        }
+        require(debtOf[borrower][id] >= maxDebt, "position is healthy");
+
+        uint256 totalRepaid;
+
+        for (uint256 i = 0; i < term.collaterals.length; i++) {
+            if (seizures[i].repaidAmount + seizures[i].seizedAssets > 0) {
+                require(
+                    UtilsLib.exactlyOneZero(seizures[i].repaidAmount, seizures[i].seizedAssets), "INCONSISTENT_INPUT"
+                );
+
+                uint256 collateralPrice = IOracle(term.collaterals[i].oracle).price();
+
+                if (seizures[i].seizedAssets > 0) {
+                    seizures[i].repaidAmount = seizures[i].seizedAssets.mulDivDown(collateralPrice, ORACLE_PRICE_SCALE)
+                        .wDivUp(liquidationIncentiveFactor);
+                } else {
+                    seizures[i].seizedAssets = seizures[i].repaidAmount.wMulDown(liquidationIncentiveFactor).mulDivDown(
+                        ORACLE_PRICE_SCALE, collateralPrice
+                    );
+                }
+
+                totalRepaid += seizures[i].repaidAmount;
+                collateralOf[borrower][id][term.collaterals[i].token] -= seizures[i].seizedAssets;
+
+                IERC20(term.collaterals[i].token).transfer(msg.sender, seizures[i].seizedAssets);
+            }
+        }
+
+        uint256 originalDebt = debtOf[borrower][id];
+        debtOf[borrower][id] -= totalRepaid;
+
+        // Realize bad debt
+        if (repayableDebt < originalDebt) {
+            // Because roundings are not aligned the effective bad debt is either the remaining debt or the original debt minus the theoretical repayable debt.
+            uint256 badDebt = UtilsLib.min(debtOf[borrower][id], originalDebt - repayableDebt);
+            debtOf[borrower][id] -= badDebt;
+            totalAssets[id] -= badDebt;
+        }
+
+        withdrawable[id] += totalRepaid;
+
+        if (data.length > 0) IMorphoLiquidationCallback(msg.sender).onLiquidate(seizures, borrower, msg.sender, data);
+
+        IERC20(term.loanToken).transferFrom(msg.sender, address(this), totalRepaid);
+
+        return seizures;
+    }
+
+    function bondOf(address owner, bytes32 id) public view returns (uint256) {
+        return bondSharesOf[owner][id].toAssetsDown(totalAssets[id], totalShares[id]);
+    }
+
+    /// INTERNAL ///
+
+    function _id(Term memory term) public pure returns (bytes32) {
+        return keccak256(abi.encode(term));
+    }
+
+    function _checkOffers(
+        Offer memory buyOffer,
+        Signature memory buySig,
+        Offer memory sellOffer,
+        Signature memory sellSig
+    ) internal view {
+        // Check consistency.
+
+        require(buyOffer.buy && !sellOffer.buy, "Inconsistent lend flags");
+        require(buyOffer.maturity > block.timestamp, "Buy offer has expired");
+        _checkSignature(buyOffer, buySig);
+        _checkSignature(sellOffer, sellSig);
+
+        // Check compatibility.
+
+        require(buyOffer.offering != sellOffer.offering, "Same offering");
+        require(buyOffer.loanToken == sellOffer.loanToken, "Loan tokens do not match");
+        uint256 j = 0;
+        for (uint256 i = 0; i < sellOffer.collaterals.length; i++) {
+            // Relies on the fact that the collaterals are sorted.
+            // Note that we actually never check that.
+            // If they are not, the match could fail.
+            while (
+                bytes20(sellOffer.collaterals[i].token) < bytes20(buyOffer.collaterals[j].token)
+                    && j++ < buyOffer.collaterals.length
+            ) {}
+            require(sellOffer.collaterals[i].token == buyOffer.collaterals[j].token, "Collaterals tokens do not match");
+            require(sellOffer.collaterals[i].lltv <= buyOffer.collaterals[j].lltv, "LLTVs do not match");
+            require(sellOffer.collaterals[i].oracle == buyOffer.collaterals[j].oracle, "Oracles do not match");
+            j++;
+        }
+        require(buyOffer.maturity == sellOffer.maturity, "Maturities do not match");
+        require(buyOffer.price >= sellOffer.price, "Buy offer price is less than sell offer price");
+    }
+
+    function _checkSignature(Offer memory offer, Signature memory signature) internal view {
+        bytes32 hashStruct = keccak256(abi.encode(OFFER_TYPEHASH, offer));
+        bytes32 domainSeparator = keccak256(abi.encode(DOMAIN_TYPEHASH, block.chainid, address(this)));
+        bytes32 digest = keccak256(bytes.concat("\x19\x01", domainSeparator, hashStruct));
+        address signatory = ecrecover(digest, signature.v, signature.r, signature.s);
+
+        require(signatory != address(0) && offer.offering == signatory, "Invalid signature");
+    }
+
+    function _isHealthy(Term memory term, address borrower) internal view returns (bool) {
+        if (term.maturity < block.timestamp) {
+            return false;
+        } else {
+            bytes32 id = _id(term);
+
+            uint256 maxDebt;
+            for (uint256 i = 0; i < term.collaterals.length; i++) {
+                uint256 price = IOracle(term.collaterals[i].oracle).price();
+                uint256 collateralQuoted =
+                    collateralOf[borrower][id][term.collaterals[i].token].mulDivDown(price, ORACLE_PRICE_SCALE);
+                maxDebt += collateralQuoted.wMulDown(term.collaterals[i].lltv);
+            }
+
+            return debtOf[borrower][id] <= maxDebt;
+        }
+    }
+}
diff --git a/src/interfaces/IERC20.sol b/src/interfaces/IERC20.sol
new file mode 100644
index 000000000..444767548
--- /dev/null
+++ b/src/interfaces/IERC20.sol
@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.0;
+
+interface IERC20 {
+    function transfer(address recipient, uint256 amount) external returns (bool);
+    function transferFrom(address sender, address recipient, uint256 amount) external returns (bool);
+    function balanceOf(address account) external view returns (uint256);
+}
diff --git a/src/interfaces/IMorphoLiquidationCallback.sol b/src/interfaces/IMorphoLiquidationCallback.sol
new file mode 100644
index 000000000..b7a24bbda
--- /dev/null
+++ b/src/interfaces/IMorphoLiquidationCallback.sol
@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity 0.8.28;
+
+import {Seizure} from "./ITerms.sol";
+
+interface IMorphoLiquidationCallback {
+    function onLiquidate(Seizure[] memory seizures, address borrower, address liquidator, bytes memory data) external;
+}
diff --git a/src/interfaces/IOracle.sol b/src/interfaces/IOracle.sol
new file mode 100644
index 000000000..ffa31cff2
--- /dev/null
+++ b/src/interfaces/IOracle.sol
@@ -0,0 +1,6 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.0;
+
+interface IOracle {
+    function price() external view returns (uint256);
+}
diff --git a/src/interfaces/ITerms.sol b/src/interfaces/ITerms.sol
new file mode 100644
index 000000000..9b12845ca
--- /dev/null
+++ b/src/interfaces/ITerms.sol
@@ -0,0 +1,40 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.0;
+
+struct Term {
+    address loanToken;
+    // Must be sorted by address.
+    Collateral[] collaterals;
+    uint256 maturity;
+}
+
+struct Collateral {
+    address token;
+    uint256 lltv;
+    address oracle;
+}
+
+struct Offer {
+    bool buy;
+    address offering;
+    uint256 assets;
+    address loanToken;
+    Collateral[] collaterals;
+    uint256 maturity;
+    uint256 price;
+}
+
+struct Signature {
+    uint8 v;
+    bytes32 r;
+    bytes32 s;
+}
+
+struct Seizure {
+    // Amount of loan asset to repay.
+    uint256 repaidAmount;
+    // Amount of collater asset to seize.
+    uint256 seizedAssets;
+}
+
+interface ITerms {}
diff --git a/src/libraries/MathLib.sol b/src/libraries/MathLib.sol
new file mode 100644
index 000000000..0c9b99a66
--- /dev/null
+++ b/src/libraries/MathLib.sol
@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity ^0.8.0;
+
+uint256 constant WAD = 1e18;
+
+/// @title MathLib
+/// @author Morpho Labs
+/// @custom:contact security@morpho.org
+/// @notice Library to manage fixed-point arithmetic.
+library MathLib {
+    /// @dev Returns (`x` * `y`) / `WAD` rounded down.
+    function wMulDown(uint256 x, uint256 y) internal pure returns (uint256) {
+        return mulDivDown(x, y, WAD);
+    }
+
+    /// @dev Returns (`x` * `WAD`) / `y` rounded up.
+    function wDivUp(uint256 x, uint256 y) internal pure returns (uint256) {
+        return mulDivUp(x, WAD, y);
+    }
+
+    /// @dev Returns (`x` * `WAD`) / `y` rounded up.
+    function wDivDown(uint256 x, uint256 y) internal pure returns (uint256) {
+        return mulDivDown(x, WAD, y);
+    }
+
+    /// @dev Returns (`x` * `y`) / `d` rounded down.
+    function mulDivDown(uint256 x, uint256 y, uint256 d) internal pure returns (uint256) {
+        return (x * y) / d;
+    }
+
+    /// @dev Returns (`x` * `y`) / `d` rounded up.
+    function mulDivUp(uint256 x, uint256 y, uint256 d) internal pure returns (uint256) {
+        return (x * y + (d - 1)) / d;
+    }
+}
diff --git a/src/libraries/SharesMathLib.sol b/src/libraries/SharesMathLib.sol
new file mode 100644
index 000000000..7e252db2f
--- /dev/null
+++ b/src/libraries/SharesMathLib.sol
@@ -0,0 +1,40 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity ^0.8.0;
+
+import {MathLib} from "./MathLib.sol";
+
+/// @title SharesMathLib
+/// @author Morpho Labs
+/// @custom:contact security@morpho.org
+/// @notice Shares management library.
+/// @dev This implementation mitigates share price manipulations, using OpenZeppelin's method of virtual shares:
+/// https://docs.openzeppelin.com/contracts/4.x/erc4626#inflation-attack.
+library SharesMathLib {
+    using MathLib for uint256;
+
+    /// @dev The number of virtual shares has been chosen low enough to prevent overflows, and high enough to ensure
+    /// high precision computations.
+    /// @dev Virtual shares can never be redeemed for the assets they are entitled to, but it is assumed the share price
+    /// stays low enough not to inflate these assets to a significant value.
+    /// @dev Warning: The assets to which virtual borrow shares are entitled behave like unrealizable bad debt.
+    uint256 internal constant VIRTUAL_SHARES = 1e6;
+
+    /// @dev A number of virtual assets of 1 enforces a conversion rate between shares and assets when a market is
+    /// empty.
+    uint256 internal constant VIRTUAL_ASSETS = 1;
+
+    /// @dev Calculates the value of `assets` quoted in shares, rounding down.
+    function toSharesDown(uint256 assets, uint256 totalAssets, uint256 totalShares) internal pure returns (uint256) {
+        return assets.mulDivDown(totalShares + VIRTUAL_SHARES, totalAssets + VIRTUAL_ASSETS);
+    }
+
+    /// @dev Calculates the value of `shares` quoted in assets, rounding down.
+    function toAssetsDown(uint256 shares, uint256 totalAssets, uint256 totalShares) internal pure returns (uint256) {
+        return shares.mulDivDown(totalAssets + VIRTUAL_ASSETS, totalShares + VIRTUAL_SHARES);
+    }
+
+    /// @dev Calculates the value of `assets` quoted in shares, rounding up.
+    function toSharesUp(uint256 assets, uint256 totalAssets, uint256 totalShares) internal pure returns (uint256) {
+        return assets.mulDivUp(totalShares + VIRTUAL_SHARES, totalAssets + VIRTUAL_ASSETS);
+    }
+}
diff --git a/src/libraries/UtilsLib.sol b/src/libraries/UtilsLib.sol
new file mode 100644
index 000000000..57f43ae6d
--- /dev/null
+++ b/src/libraries/UtilsLib.sol
@@ -0,0 +1,23 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity ^0.8.0;
+
+/// @title UtilsLib
+/// @author Morpho Labs
+/// @custom:contact security@morpho.org
+/// @notice Library exposing helpers.
+/// @dev Inspired by https://github.com/morpho-org/morpho-utils.
+library UtilsLib {
+    /// @dev Returns true if there is exactly one zero among `x` and `y`.
+    function exactlyOneZero(uint256 x, uint256 y) internal pure returns (bool z) {
+        assembly {
+            z := xor(iszero(x), iszero(y))
+        }
+    }
+
+    /// @dev Returns the min of `x` and `y`.
+    function min(uint256 x, uint256 y) internal pure returns (uint256 z) {
+        assembly {
+            z := xor(x, mul(xor(x, y), lt(y, x)))
+        }
+    }
+}
diff --git a/test/BaseTest.sol b/test/BaseTest.sol
new file mode 100644
index 000000000..b9b886933
--- /dev/null
+++ b/test/BaseTest.sol
@@ -0,0 +1,41 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.0;
+
+import {Test} from "../lib/forge-std/src/Test.sol";
+import {ERC20} from "./helpers/ERC20.sol";
+import "../src/Terms.sol";
+
+abstract contract BaseTest is Test {
+    Terms internal terms;
+
+    function setUp() public virtual {
+        terms = new Terms();
+    }
+
+    function _signOffer(Offer memory offer, uint256 sk) internal view returns (Signature memory) {
+        bytes32 hashStruct = keccak256(abi.encode(terms.OFFER_TYPEHASH(), offer));
+        bytes32 domainSeparator = keccak256(abi.encode(terms.DOMAIN_TYPEHASH(), block.chainid, address(terms)));
+        bytes32 digest = keccak256(bytes.concat("\x19\x01", domainSeparator, hashStruct));
+
+        Signature memory sig;
+        (sig.v, sig.r, sig.s) = vm.sign(sk, digest);
+        return sig;
+    }
+
+    function sortTokens(ERC20[] memory arr) internal pure returns (ERC20[] memory) {
+        uint256 length = arr.length;
+        for (uint256 i = 1; i < length; i++) {
+            bytes20 key = bytes20((address(arr[i])));
+            uint256 j = i - 1;
+            while ((int256(j) >= 0) && (bytes20(address(arr[j])) > key)) {
+                arr[j + 1] = arr[j];
+                if (j == 0) {
+                    break;
+                }
+                j--;
+            }
+            arr[j + (bytes20(address(arr[j])) > key ? 0 : 1)] = ERC20(address(key));
+        }
+        return arr;
+    }
+}
diff --git a/test/LiquidationTest.sol b/test/LiquidationTest.sol
new file mode 100644
index 000000000..136bc5b18
--- /dev/null
+++ b/test/LiquidationTest.sol
@@ -0,0 +1,236 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.0;
+
+import "./BaseTest.sol";
+
+import {console} from "../lib/forge-std/src/Test.sol";
+
+import {Oracle} from "./helpers/Oracle.sol";
+
+contract LiquidationTest is BaseTest {
+    ERC20 private loanToken;
+    uint256 private borrowerSK;
+    address private borrower;
+    uint256 private lenderSK;
+    address private lender;
+    address private liquidator;
+    Term[] private liquidationTerms;
+    Seizure[][] private sN;
+    Seizure[][] private sK;
+
+    function genTerm(uint256 n) internal returns (Term memory) {
+        Collateral[] memory cs = new Collateral[](n);
+        ERC20[] memory tokens = new ERC20[](n);
+
+        for (uint256 i = 0; i < n; i++) {
+            tokens[i] = new ERC20("collat", "c", 1 ether);
+        }
+
+        tokens = sortTokens(tokens);
+
+        for (uint256 i = 0; i < n; i++) {
+            ERC20 c = tokens[i];
+            Oracle o = new Oracle();
+            c.transfer(borrower, 1 ether);
+            cs[i] = Collateral({token: address(tokens[i]), lltv: 0.75e18, oracle: address(o)});
+            vm.startPrank(borrower);
+            c.approve(address(terms), type(uint256).max);
+            vm.stopPrank();
+        }
+
+        Term memory t = Term(address(loanToken), cs, block.timestamp + 100);
+
+        loanToken.transfer(lender, 1000);
+
+        vm.startPrank(borrower);
+        uint256 remaining = 840;
+        uint256 dealt;
+        for (uint256 i = 1; i < n; i++) {
+            dealt += remaining / (n - 1);
+            terms.supplyCollateral(t, cs[i].token, remaining / (n - 1), borrower);
+        }
+        // The collateral in position 0 is used to make the position liquidatable.
+        terms.supplyCollateral(t, cs[0].token, remaining + 500, borrower);
+        vm.stopPrank();
+
+        return t;
+    }
+
+    function mintBond(Collateral[] memory cs) internal {
+        Offer memory lendOffer = Offer({
+            buy: true,
+            offering: lender,
+            assets: 1000,
+            loanToken: address(loanToken),
+            collaterals: cs,
+            maturity: block.timestamp + 100,
+            price: 990
+        });
+
+        Offer memory borrowOffer = Offer({
+            buy: false,
+            offering: borrower,
+            assets: 1000,
+            loanToken: address(loanToken),
+            collaterals: cs,
+            maturity: block.timestamp + 100,
+            price: 990
+        });
+
+        Signature memory lendSig = _signOffer(lendOffer, lenderSK);
+        Signature memory borrowSig = _signOffer(borrowOffer, borrowerSK);
+
+        terms.MATCH(lendOffer, lendSig, borrowOffer, borrowSig);
+    }
+
+    function setUp() public override {
+        super.setUp();
+        (borrower, borrowerSK) = makeAddrAndKey("borrower");
+        (lender, lenderSK) = makeAddrAndKey("lender");
+        liquidator = makeAddr("liquidator");
+
+        loanToken = new ERC20("loan", "loan", 1 ether);
+        loanToken.transfer(lender, 99);
+        loanToken.transfer(borrower, 1);
+
+        vm.prank(lender);
+        loanToken.approve(address(terms), type(uint256).max);
+        vm.prank(borrower);
+        loanToken.approve(address(terms), type(uint256).max);
+        vm.prank(liquidator);
+        loanToken.approve(address(terms), type(uint256).max);
+        vm.stopPrank();
+
+        liquidationTerms = new Term[](10);
+        sN = new Seizure[][](10);
+        sK = new Seizure[][](10);
+
+        for (uint256 i = 0; i < 10; i++) {
+            liquidationTerms[i] = genTerm(i + 1);
+            mintBond(liquidationTerms[i].collaterals);
+            sK[i] = new Seizure[](10);
+            sK[i][0] = Seizure({repaidAmount: 100, seizedAssets: 0});
+            for (uint256 k = 1; k < i + 1; k++) {
+                sK[i][k] = Seizure({repaidAmount: 0, seizedAssets: 93});
+            }
+        }
+
+        for (uint256 i = 0; i < 10; i++) {
+            liquidationTerms[i] = genTerm(i + 1);
+            mintBond(liquidationTerms[i].collaterals);
+            sN[i] = new Seizure[](i + 1);
+            sN[i][0] = Seizure({repaidAmount: 100, seizedAssets: 0});
+            for (uint256 k = 1; k < i + 1; k++) {
+                sN[i][k] = Seizure({repaidAmount: 0, seizedAssets: 0});
+            }
+        }
+
+        vm.warp(block.timestamp + 50);
+    }
+
+    function execLiquidation(uint256 k, uint256 n) public {
+        loanToken.transfer(liquidator, 1000);
+        Term memory t = liquidationTerms[n - 1];
+        Oracle(t.collaterals[0].oracle).setPrice(0.25e36);
+
+        vm.prank(liquidator);
+        uint256 gasBefore;
+        uint256 gasUsed;
+        if (n == 10) {
+            gasBefore = gasleft();
+            terms.liquidate(t, sK[k - 1], borrower, hex"");
+            gasUsed = gasBefore - gasleft();
+        } else {
+            gasBefore = gasleft();
+            terms.liquidate(t, sN[n - 1], borrower, hex"");
+            gasUsed = gasBefore - gasleft();
+        }
+
+        Oracle(t.collaterals[0].oracle).setPrice(1e36);
+        emit log_named_uint("Gas used", gasUsed);
+
+        assertEq(ERC20(t.collaterals[0].token).balanceOf(liquidator), 460);
+        vm.prank(borrower);
+        loanToken.transfer(address(0), loanToken.balanceOf(borrower));
+        vm.stopPrank();
+        vm.prank(liquidator);
+        loanToken.transfer(address(0), loanToken.balanceOf(liquidator));
+        vm.stopPrank();
+    }
+
+    function testLiquidationN1K1() public {
+        execLiquidation(1, 1);
+    }
+
+    function testLiquidationN2K1() public {
+        execLiquidation(1, 2);
+    }
+
+    function testLiquidationN3K1() public {
+        execLiquidation(1, 3);
+    }
+
+    function testLiquidationN4K1() public {
+        execLiquidation(1, 4);
+    }
+
+    function testLiquidationN5K1() public {
+        execLiquidation(1, 5);
+    }
+
+    function testLiquidationN6K1() public {
+        execLiquidation(1, 6);
+    }
+
+    function testLiquidationN7K1() public {
+        execLiquidation(1, 7);
+    }
+
+    function testLiquidationN8K1() public {
+        execLiquidation(1, 8);
+    }
+
+    function testLiquidationN9K1() public {
+        execLiquidation(1, 9);
+    }
+
+    function testLiquidationN10K1() public {
+        execLiquidation(1, 10);
+    }
+
+    function testLiquidationN10K2() public {
+        execLiquidation(2, 10);
+    }
+
+    function testLiquidationN10K3() public {
+        execLiquidation(3, 10);
+    }
+
+    function testLiquidationN10K4() public {
+        execLiquidation(4, 10);
+    }
+
+    function testLiquidationN10K5() public {
+        execLiquidation(5, 10);
+    }
+
+    function testLiquidationN10K6() public {
+        execLiquidation(6, 10);
+    }
+
+    function testLiquidationN10K7() public {
+        execLiquidation(7, 10);
+    }
+
+    function testLiquidationN10K8() public {
+        execLiquidation(8, 10);
+    }
+
+    function testLiquidationN10K9() public {
+        execLiquidation(9, 10);
+    }
+
+    function testLiquidationN10K10() public {
+        execLiquidation(10, 10);
+    }
+}
diff --git a/test/TermsTest.sol b/test/TermsTest.sol
new file mode 100644
index 000000000..d2f6d4c65
--- /dev/null
+++ b/test/TermsTest.sol
@@ -0,0 +1,140 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.0;
+
+import "./BaseTest.sol";
+
+import {Oracle} from "./helpers/Oracle.sol";
+
+contract TermsTest is BaseTest {
+    ERC20 private loanToken;
+    ERC20 private collateralToken;
+    Oracle private oracle;
+    uint256 private borrowerSK;
+    address private borrower;
+    uint256 private lenderSK;
+    address private lender;
+    address private liquidator;
+    Term private term;
+
+    bytes32 private id;
+    Collateral[] private collaterals;
+    Seizure[] private seizures;
+
+    function setUp() public override {
+        super.setUp();
+        (borrower, borrowerSK) = makeAddrAndKey("borrower");
+        (lender, lenderSK) = makeAddrAndKey("lender");
+        liquidator = makeAddr("liquidator");
+
+        loanToken = new ERC20("loan", "loan", 1 ether);
+        loanToken.transfer(lender, 99);
+        loanToken.transfer(borrower, 1);
+        collateralToken = new ERC20("collat", "collat", 1 ether);
+        oracle = new Oracle();
+
+        collaterals = new Collateral[](1);
+        collaterals[0] = Collateral({token: address(collateralToken), lltv: 0.75e18, oracle: address(oracle)});
+
+        seizures = new Seizure[](1);
+        seizures[0] = Seizure({repaidAmount: 0, seizedAssets: 134});
+
+        term = Term(address(loanToken), collaterals, block.timestamp + 100);
+        id = keccak256(abi.encode(term));
+
+        vm.prank(lender);
+        loanToken.approve(address(terms), type(uint256).max);
+        vm.prank(borrower);
+        loanToken.approve(address(terms), type(uint256).max);
+        collateralToken.approve(address(terms), type(uint256).max);
+        terms.supplyCollateral(term, address(collateralToken), 134, borrower);
+        vm.prank(liquidator);
+        loanToken.approve(address(terms), type(uint256).max);
+    }
+
+    function testMint() public {
+        Offer memory lendOffer = Offer({
+            buy: true,
+            offering: lender,
+            assets: 100,
+            loanToken: address(loanToken),
+            collaterals: collaterals,
+            maturity: block.timestamp + 100,
+            price: 99
+        });
+        Offer memory borrowOffer = Offer({
+            buy: false,
+            offering: borrower,
+            assets: 100,
+            loanToken: address(loanToken),
+            collaterals: collaterals,
+            maturity: block.timestamp + 100,
+            price: 99
+        });
+
+        Signature memory lendSig = _signOffer(lendOffer, lenderSK);
+        Signature memory borrowSig = _signOffer(borrowOffer, borrowerSK);
+
+        terms.MATCH(lendOffer, lendSig, borrowOffer, borrowSig);
+
+        assertEq(terms.bondOf(lender, id), 100);
+        assertEq(terms.debtOf(borrower, id), 100);
+
+        assertEq(loanToken.balanceOf(borrower), 100);
+        assertEq(loanToken.balanceOf(lender), 0);
+    }
+
+    function testRepay() public {
+        testMint();
+
+        vm.warp(block.timestamp + 99);
+
+        vm.prank(borrower);
+        terms.repayDebt(term, 100, borrower);
+
+        assertEq(terms.debtOf(borrower, id), 0);
+        assertEq(terms.withdrawable(id), 100);
+
+        assertEq(loanToken.balanceOf(address(terms)), 100);
+        assertEq(loanToken.balanceOf(borrower), 0);
+    }
+
+    function testWithdraw() public {
+        testRepay();
+
+        vm.prank(lender);
+        terms.withdrawBond(term, 100, 0, lender);
+
+        assertEq(terms.bondOf(lender, id), 0);
+        assertEq(terms.withdrawable(id), 0);
+
+        assertEq(loanToken.balanceOf(address(terms)), 0);
+        assertEq(loanToken.balanceOf(lender), 100);
+    }
+
+    function testWithdrawCollateral() public {
+        testRepay();
+
+        vm.prank(borrower);
+        terms.withdrawCollateral(term, address(collateralToken), 134, borrower);
+
+        assertEq(terms.collateralOf(borrower, id, address(collateralToken)), 0);
+
+        assertEq(collateralToken.balanceOf(address(terms)), 0);
+        assertEq(collateralToken.balanceOf(borrower), 134);
+    }
+
+    function testBadDebt() public {
+        testMint();
+
+        loanToken.transfer(liquidator, 1000);
+        Oracle(collaterals[0].oracle).setPrice(0.75e36);
+
+        vm.prank(liquidator);
+        Seizure[] memory ret = terms.liquidate(term, seizures, borrower, hex"");
+        assertEq(terms.debtOf(borrower, id), 0);
+        assertEq(ret[0].repaidAmount, 87);
+        assertEq(terms.withdrawable(id), 87);
+        assertEq(terms.bondOf(lender, id), 87);
+        assertEq(terms.totalAssets(id), 87);
+    }
+}
diff --git a/test/helpers/ERC20.sol b/test/helpers/ERC20.sol
new file mode 100644
index 000000000..72825edd2
--- /dev/null
+++ b/test/helpers/ERC20.sol
@@ -0,0 +1,42 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.0;
+
+contract ERC20 {
+    string public name;
+    string public symbol;
+    uint256 public totalSupply;
+    mapping(address => uint256) public balanceOf;
+    mapping(address => mapping(address => uint256)) public allowance;
+
+    constructor(string memory _name, string memory _symbol, uint256 _totalSupply) {
+        name = _name;
+        symbol = _symbol;
+        totalSupply = _totalSupply;
+        balanceOf[msg.sender] = _totalSupply;
+    }
+
+    function transfer(address recipient, uint256 amount) public returns (bool) {
+        require(amount <= balanceOf[msg.sender], "Insufficient balance");
+
+        balanceOf[msg.sender] -= amount;
+        balanceOf[recipient] += amount;
+
+        return true;
+    }
+
+    function transferFrom(address sender, address recipient, uint256 amount) public returns (bool) {
+        require(amount <= balanceOf[sender], "Insufficient balance");
+        require(amount <= allowance[sender][msg.sender], "Insufficient allowance");
+
+        balanceOf[sender] -= amount;
+        balanceOf[recipient] += amount;
+        allowance[sender][msg.sender] -= amount;
+
+        return true;
+    }
+
+    function approve(address spender, uint256 amount) public returns (bool) {
+        allowance[msg.sender][spender] = amount;
+        return true;
+    }
+}
diff --git a/test/helpers/Oracle.sol b/test/helpers/Oracle.sol
new file mode 100644
index 000000000..1db5ff986
--- /dev/null
+++ b/test/helpers/Oracle.sol
@@ -0,0 +1,10 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.0;
+
+contract Oracle {
+    uint256 public price = 1e36;
+
+    function setPrice(uint256 newPrice) external {
+        price = newPrice;
+    }
+}