diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
new file mode 100644
index 0000000..d4c5c3f
--- /dev/null
+++ b/.github/workflows/certora.yml
@@ -0,0 +1,50 @@
+name: Certora
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    strategy:
+      fail-fast: false
+
+      matrix:
+        conf:
+          - Immutability
+          - Reentrancy
+
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Install python
+        uses: actions/setup-python@v5
+        with:
+          python-version: ">=3.11"
+
+      - name: Install certora
+        run: pip install certora-cli
+
+      - name: Install solc (0.8.19)
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc-0.8.19
+
+      - name: Install solc (0.8.27)
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.27/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc-0.8.27
+
+      - name: Verify ${{ matrix.conf }} specification
+        run: certoraRun certora/confs/${{ matrix.conf }}.conf
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
diff --git a/.gitignore b/.gitignore
index 85198aa..8c30259 100644
--- a/.gitignore
+++ b/.gitignore
@@ -12,3 +12,6 @@ docs/
 
 # Dotenv file
 .env
+
+# Certora
+.certora_internal
diff --git a/certora/README.md b/certora/README.md
new file mode 100644
index 0000000..a5ca080
--- /dev/null
+++ b/certora/README.md
@@ -0,0 +1,67 @@
+# Pre-liquidation Contract Formal Verification
+
+This folder contains the
+[CVL](https://docs.certora.com/en/latest/docs/cvl/index.html)
+specification and verification setup for the
+[pre-liquidation](../src/PreLiquidation.sol) contract using the
+[Certora Prover](https://www.certora.com/).
+
+## Getting Started
+
+This project depends on two different versions of
+[Solidity](https://soliditylang.org/) which are required for running
+the verification. The compiler binaries should be available under the
+following path names:
+
+  - `solc-0.8.19` for the solidity compiler version `0.8.19`, which is
+    used for `Morpho`;
+  - `solc-0.8.27` for the solidity compiler version `0.8.27`, which is
+    used for `PreLiquidation`.
+
+To verifying a specification, run the command `certoraRun Spec.conf`
+where `Spec.conf` is the configuration file of the matching CVL
+specification. Configuration files are available in
+[`certora/conf`](./confs). Please ensure that `CERTORAKEY` is set up
+in your environment.
+
+## Overview
+
+The PreLiquidation contract enables Morpho Blue borrowers to set up a
+safer liquidation plan on a given position, thus preventing undesired
+liquidations.
+
+### Reentrancy
+
+This is checked in [`Reentrancy.spec`](specs/Reentrancy.spec).
+
+### Immutability
+
+This is checked in [`Immutability.spec`](specs/Immutability.spec).
+
+## Verification architecture
+
+### Folders and file structure
+
+The [`certora/specs`](specs) folder contains the following files:
+
+- [`Reentrancy.spec`](specs/Reentrancy.spec) checks that
+  PreLiquidation is reentrancy safe by checking that the storage is never
+  used.
+
+- [`Immutability.spec`](specs/Immutability.spec) checks that
+  PreLiquidation contract is immutable because it doesn't perform any
+  delegate call.
+
+The [`certora/confs`](confs) folder contains a configuration file for
+each corresponding specification file.
+
+The [`certora/helpers`](helpers) folder contains helper contracts that
+enable the verification of PreLiquidation. Notably, this allows
+handling the fact that library functions should be called from a
+contract to be verified independently, and it allows defining needed
+getters.
+
+## TODO
+
+- [ ] Provide an overview of the specification.
+- [ ] Update the verification architecture.
diff --git a/certora/confs/Immutability.conf b/certora/confs/Immutability.conf
new file mode 100644
index 0000000..6fae19c
--- /dev/null
+++ b/certora/confs/Immutability.conf
@@ -0,0 +1,16 @@
+{
+    "files": [
+        "src/PreLiquidation.sol",
+    ],
+    "solc": "solc-0.8.27",
+    "solc_via_ir" : true,
+    "verify": "PreLiquidation:certora/specs/Immutability.spec",
+    "prover_args": [
+        "-depth 3",
+        "-mediumTimeout 20",
+        "-timeout 120",
+    ],
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "PreLiquidation Immutability",
+}
diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf
new file mode 100644
index 0000000..f217f93
--- /dev/null
+++ b/certora/confs/Reentrancy.conf
@@ -0,0 +1,17 @@
+{
+    "files": [
+        "src/PreLiquidation.sol",
+    ],
+    "solc": "solc-0.8.27",
+    "solc_via_ir" : true,
+    "verify": "PreLiquidation:certora/specs/Reentrancy.spec",
+    "prover_args": [
+        "-enableStorageSplitting false",
+        "-depth 3",
+        "-mediumTimeout 20",
+        "-timeout 120",
+    ],
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "PreLiquidation Reentrancy",
+}
diff --git a/certora/specs/Immutability.spec b/certora/specs/Immutability.spec
new file mode 100644
index 0000000..6c357af
--- /dev/null
+++ b/certora/specs/Immutability.spec
@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+persistent ghost bool delegateCall;
+
+hook DELEGATECALL(uint g, address addr, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {
+    delegateCall = true;
+}
+
+// Check that the contract is truly immutable.
+rule noDelegateCalls(method f, env e, calldataarg data) {
+    // Set up the initial state.
+    require !delegateCall;
+    f(e,data);
+    assert !delegateCall;
+}
diff --git a/certora/specs/Reentrancy.spec b/certora/specs/Reentrancy.spec
new file mode 100644
index 0000000..12c808d
--- /dev/null
+++ b/certora/specs/Reentrancy.spec
@@ -0,0 +1,22 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+
+
+// True when storage has been accessed with either a SSTORE or a SLOAD.
+persistent ghost bool hasAccessedStorage;
+
+hook ALL_SSTORE(uint loc, uint v) {
+    hasAccessedStorage = true;
+}
+
+hook ALL_SLOAD(uint loc) uint v {
+    hasAccessedStorage = true;
+}
+
+// Check that no function is accessing storage.
+rule reentrancySafe(method f, env e, calldataarg data) {
+    // Set up the initial state.
+    require !hasAccessedStorage;
+    f(e,data);
+    assert !hasAccessedStorage;
+}