diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
new file mode 100644
index 0000000..0ca3fac
--- /dev/null
+++ b/.github/workflows/certora.yml
@@ -0,0 +1,45 @@
+name: Certora
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    strategy:
+      fail-fast: false
+
+      matrix:
+        conf:
+          - MerkleTree
+          - UniversalRewardsDistributor
+
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+
+      - name: Install python
+        uses: actions/setup-python@v4
+
+      - name: Install certora
+        run: pip install certora-cli
+
+      - name: Install solc
+        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: Verify ${{ matrix.conf }}
+        run: certoraRun certora/confs/${{ matrix.conf }}.conf
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
diff --git a/.gitignore b/.gitignore
index 9aa64ca..1818db5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -15,4 +15,8 @@ docs/
 
 # npm
 package-lock.json
-node_modules
\ No newline at end of file
+node_modules
+
+# certora
+.certora**
+emv-*-certora*
diff --git a/certora/README.md b/certora/README.md
new file mode 100644
index 0000000..d20271b
--- /dev/null
+++ b/certora/README.md
@@ -0,0 +1,56 @@
+This folder contains the verification of the universal rewards distribution mechanism using CVL, Certora's Verification Language.
+
+# Folder and file structure
+
+The [`certora/specs`](specs) folder contains the specification files.
+
+The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file.
+
+The [`certora/helpers`](helpers) folder contains files that enable the verification of Morpho Blue.
+
+# Overview of the verification
+
+This work aims at providing a formally verified rewards checker.
+The rewards checker is composed of the [Checker.sol](checker/Checker.sol) file, which takes a certificate as an input.
+The certificate is assumed to contain the submitted root to verify and a Merkle tree, and it is checked that the Merkle tree is well-formed.
+
+Those checks are done by only using "trusted" functions, namely `newLeaf` and `newInternalNode`, that have been formally verified to preserve those invariants:
+
+- it is checked in [MerkleTree.spec](specs/MerkleTree.spec) that those functions lead to creating well-formed trees.
+- it is checked in [UniversalRewardsDistributor.spec](specs/UniversalRewardsDistributor.spec) that the rewards distributor is correct, meaning that claimed rewards correspond exactly to the rewards contained in the corresponding Merkle tree.
+
+# Getting started
+
+## Verifying the rewards checker
+
+Install `certora-cli` package with `pip install certora-cli`.
+To verify specification files, pass to `certoraRun` the corresponding configuration file in the [`certora/confs`](confs) folder.
+It requires having set the `CERTORAKEY` environment variable to a valid Certora key.
+You can also pass additional arguments, notably to verify a specific rule.
+For example, at the root of the repository:
+
+```
+certoraRun certora/confs/MerkleTrees.conf --rule wellFormed
+```
+
+## Running the rewards checker
+
+To verify that a given list of proofs corresponds to a valid Merkle tree, you must generate a certificate from it.
+This assumes that the list of proofs is in the expected JSON format.
+For example, at the root of the repository, given a `proofs.json` file:
+
+```
+python certora/checker/create_certificate.py proofs.json
+```
+
+This requires installing the corresponding libraries first:
+
+```
+pip install web3 eth-tester py-evm
+```
+
+Then, check this certificate:
+
+```
+FOUNDRY_PROFILE=checker forge test
+```
diff --git a/certora/checker/Checker.sol b/certora/checker/Checker.sol
new file mode 100644
index 0000000..6259862
--- /dev/null
+++ b/certora/checker/Checker.sol
@@ -0,0 +1,38 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity ^0.8.0;
+
+import "../../lib/openzeppelin-contracts/contracts/utils/Strings.sol";
+import "../helpers/MerkleTree.sol";
+import "../../lib/forge-std/src/Test.sol";
+import "../../lib/forge-std/src/StdJson.sol";
+
+contract Checker is Test {
+    using stdJson for string;
+
+    MerkleTree tree = new MerkleTree();
+
+    function testVerifyCertificate() public {
+        string memory projectRoot = vm.projectRoot();
+        string memory path = string.concat(projectRoot, "/certificate.json");
+        string memory json = vm.readFile(path);
+
+        uint256 leafLength = abi.decode(json.parseRaw(".leafLength"), (uint256));
+        Leaf memory leaf;
+        for (uint256 i; i < leafLength; i++) {
+            leaf = abi.decode(json.parseRaw(string.concat(".leaf[", Strings.toString(i), "]")), (Leaf));
+            tree.newLeaf(leaf);
+        }
+
+        uint256 nodeLength = abi.decode(json.parseRaw(".nodeLength"), (uint256));
+        InternalNode memory node;
+        for (uint256 i; i < nodeLength; i++) {
+            node = abi.decode(json.parseRaw(string.concat(".node[", Strings.toString(i), "]")), (InternalNode));
+            tree.newInternalNode(node);
+        }
+
+        assertTrue(!tree.isEmpty(node.id), "empty root");
+
+        bytes32 root = abi.decode(json.parseRaw(".root"), (bytes32));
+        assertEq(tree.getHash(node.id), root, "mismatched roots");
+    }
+}
diff --git a/certora/checker/create_certificate.py b/certora/checker/create_certificate.py
new file mode 100644
index 0000000..eb0315b
--- /dev/null
+++ b/certora/checker/create_certificate.py
@@ -0,0 +1,109 @@
+import sys
+import json
+from eth_abi import encode
+from web3 import Web3, EthereumTesterProvider
+
+w3 = Web3(EthereumTesterProvider())
+
+
+# Returns the hash of a node given the hashes of its children.
+def hash_node(left_hash, right_hash):
+    return w3.to_hex(
+        w3.solidity_keccak(["bytes32", "bytes32"], [left_hash, right_hash])
+    )
+
+
+# Returns the hash of a leaf given the rewards details.
+def hash_leaf(address, reward, amount):
+    encoded_args = encode(["address", "address", "uint256"], [address, reward, amount])
+    first_hash = w3.solidity_keccak(
+        ["bytes"],
+        [encoded_args],
+    )
+    second_hash = w3.solidity_keccak(
+        ["bytes"],
+        [first_hash],
+    )
+    return w3.to_hex(second_hash)
+
+
+# Returns the identifier of a leaf.
+def hash_id(addr, reward):
+    encoded_args = encode(["address", "address"], [addr, reward])
+    return w3.to_hex(w3.solidity_keccak(["bytes"], [encoded_args]))
+
+
+certificate = {}
+hash_to_id = {}
+hash_to_address = {}
+hash_to_reward = {}
+hash_to_value = {}
+left = {}
+right = {}
+
+
+# Populates the fields of the tree along the path given by the proof.
+def populate(addr, reward, amount, proof):
+    computedHash = hash_leaf(addr, reward, amount)
+    hash_to_id[computedHash] = hash_id(addr, reward)
+    hash_to_address[computedHash] = addr
+    hash_to_reward[computedHash] = reward
+    hash_to_value[computedHash] = amount
+    for proofElement in proof:
+        [leftHash, rightHash] = (
+            [computedHash, proofElement]
+            if computedHash <= proofElement
+            else [proofElement, computedHash]
+        )
+        computedHash = hash_node(leftHash, rightHash)
+        hash_to_id[computedHash] = computedHash
+        left[computedHash] = leftHash
+        right[computedHash] = rightHash
+
+
+# Traverse the tree and generate corresponding instruction for each internal node and each leaf.
+def walk(node):
+    if node in left:
+        walk(left[node])
+        walk(right[node])
+        certificate["node"].append(
+            {
+                "id": node,
+                "left": hash_to_id[left[node]],
+                "right": hash_to_id[right[node]],
+            }
+        )
+    else:
+        certificate["leaf"].append(
+            {
+                "addr": hash_to_address[node],
+                "reward": hash_to_reward[node],
+                "value": hash_to_value[node],
+            }
+        )
+
+
+with open(sys.argv[1]) as input_file:
+    proofs = json.load(input_file)
+    rewards = proofs["rewards"]
+
+    certificate["root"] = proofs["root"]
+    certificate["leaf"] = []
+    certificate["node"] = []
+
+    for addr, data in rewards.items():
+        address = w3.to_checksum_address(addr)
+        for reward, data in data.items():
+            reward = w3.to_checksum_address(reward)
+            amount = int(data["amount"])
+            populate(addr, reward, amount, data["proof"])
+
+    walk(proofs["root"])
+
+    certificate["leafLength"] = len(certificate["leaf"])
+    certificate["nodeLength"] = len(certificate["node"])
+
+    json_output = json.dumps(certificate)
+
+with open("certificate.json", "w") as output_file:
+    output_file.write(json_output)
diff --git a/certora/confs/MerkleTree.conf b/certora/confs/MerkleTree.conf
new file mode 100644
index 0000000..73e698d
--- /dev/null
+++ b/certora/confs/MerkleTree.conf
@@ -0,0 +1,12 @@
+{
+    "files": [
+        "certora/helpers/MerkleTree.sol"
+    ],
+    "solc": "solc-0.8.19",
+    "verify": "MerkleTree:certora/specs/MerkleTree.spec",
+    "optimistic_loop": true,
+    "loop_iter": "4",
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "Merkle Tree",
+}
diff --git a/certora/confs/UniversalRewardsDistributor.conf b/certora/confs/UniversalRewardsDistributor.conf
new file mode 100644
index 0000000..4cc7bdc
--- /dev/null
+++ b/certora/confs/UniversalRewardsDistributor.conf
@@ -0,0 +1,15 @@
+{
+    "files": [
+        "src/UniversalRewardsDistributor.sol",
+        "lib/openzeppelin-contracts/contracts/token/ERC20/ERC20.sol",
+        "certora/helpers/MerkleTree.sol",
+        "certora/helpers/Util.sol",
+    ],
+    "solc": "solc-0.8.19",
+    "verify": "UniversalRewardsDistributor:certora/specs/UniversalRewardsDistributor.spec",
+    "optimistic_loop": true,
+    "loop_iter": "4",
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "Universal Rewards Distributor",
+}
diff --git a/certora/helpers/MerkleTree.sol b/certora/helpers/MerkleTree.sol
new file mode 100644
index 0000000..da051ff
--- /dev/null
+++ b/certora/helpers/MerkleTree.sol
@@ -0,0 +1,125 @@
+// SPDX-License-Identifier: AGPL-3.0-only
+pragma solidity ^0.8.0;
+
+struct Leaf {
+    address addr;
+    address reward;
+    uint256 value;
+}
+
+struct InternalNode {
+    bytes32 id;
+    bytes32 left;
+    bytes32 right;
+}
+
+struct Node {
+    bytes32 left;
+    bytes32 right;
+    address addr;
+    address reward;
+    uint256 value;
+    // hash of [addr, reward, value] for leaves, and [left.hash, right.hash] for internal nodes.
+    bytes32 hashNode;
+}
+
+contract MerkleTree {
+    /* STORAGE */
+
+    // The tree has no root because every node (and the nodes underneath) form a Merkle tree.
+    // We use bytes32 as keys of the mapping so that leaves can have an identifier that is the hash of the address and the reward token.
+    // This ensures that the same pair of address and reward token does not appear twice as a leaf in the tree.
+    // For internal nodes the key is left arbitrary, so that the certificate generation can choose freely any bytes32 value (that is not already used).
+    mapping(bytes32 => Node) internal tree;
+
+    /* MAIN FUNCTIONS */
+
+    function newLeaf(Leaf memory leaf) public {
+        bytes32 id = keccak256(abi.encode(leaf.addr, leaf.reward));
+        Node storage node = tree[id];
+        require(id != 0, "id is the zero bytes");
+        require(isEmpty(node), "leaf is not empty");
+        require(leaf.value != 0, "value is zero");
+
+        node.addr = leaf.addr;
+        node.reward = leaf.reward;
+        node.value = leaf.value;
+        node.hashNode = keccak256(bytes.concat(keccak256(abi.encode(leaf.addr, leaf.reward, leaf.value))));
+    }
+
+    function newInternalNode(InternalNode memory internalNode) public {
+        Node storage node = tree[internalNode.id];
+        Node storage leftNode = tree[internalNode.left];
+        Node storage rightNode = tree[internalNode.right];
+        require(internalNode.id != 0, "id is zero bytes");
+        require(isEmpty(node), "node is not empty");
+        require(!isEmpty(leftNode), "left is empty");
+        require(!isEmpty(rightNode), "right is empty");
+        require(leftNode.hashNode <= rightNode.hashNode, "children are not pair sorted");
+
+        node.left = internalNode.left;
+        node.right = internalNode.right;
+        node.hashNode = keccak256(abi.encode(leftNode.hashNode, rightNode.hashNode));
+    }
+
+    /* PURE AND VIEW FUNCTIONS */
+
+    function isEmpty(Node memory node) public pure returns (bool) {
+        return node.left == 0 && node.right == 0 && node.addr == address(0) && node.reward == address(0)
+            && node.value == 0 && node.hashNode == 0;
+    }
+
+    function isEmpty(bytes32 id) public view returns (bool) {
+        return isEmpty(tree[id]);
+    }
+
+    function getValue(address addr, address reward) public view returns (uint256) {
+        bytes32 id = keccak256(abi.encode(addr, reward));
+        return tree[id].value;
+    }
+
+    function getHash(bytes32 id) public view returns (bytes32) {
+        return tree[id].hashNode;
+    }
+
+    // The specification of a well-formed tree is the following:
+    //   - empty nodes are well-formed
+    //   - correct identifiers of leaves
+    //   - correct hashing of leaves and of internal nodes
+    //   - internal nodes have their children pair sorted and not empty
+    function isWellFormed(bytes32 id) public view returns (bool) {
+        Node storage node = tree[id];
+
+        if (isEmpty(node)) return true;
+
+        if (node.left == 0 && node.right == 0) {
+            bytes32 idLeaf = keccak256(abi.encode(node.addr, node.reward));
+            return id == idLeaf
+                && node.hashNode == keccak256(bytes.concat(keccak256(abi.encode(node.addr, node.reward, node.value))));
+        } else {
+            // Well-formed nodes have exactly 0 or 2 children.
+            if (node.left == 0 || node.right == 0) return false;
+            Node storage left = tree[node.left];
+            Node storage right = tree[node.right];
+            return !isEmpty(left) && !isEmpty(right) && left.hashNode <= right.hashNode
+                && node.hashNode == keccak256(abi.encode(left.hashNode, right.hashNode));
+        }
+    }
+
+    // Check that the nodes are well formed starting from `node` and going down the `tree`.
+    // The `proof` is used to choose the path downward.
+    function wellFormedPath(bytes32 id, bytes32[] memory proof) public view {
+        for (uint256 i = proof.length;;) {
+            require(isWellFormed(id));
+
+            if (i == 0) break;
+
+            bytes32 otherHash = proof[--i];
+
+            bytes32 left = tree[id].left;
+            bytes32 right = tree[id].right;
+
+            id = getHash(left) == otherHash ? right : left;
+        }
+    }
+}
diff --git a/certora/helpers/Util.sol b/certora/helpers/Util.sol
new file mode 100644
index 0000000..386a681
--- /dev/null
+++ b/certora/helpers/Util.sol
@@ -0,0 +1,10 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity ^0.8.0;
+
+import {IERC20} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/IERC20.sol";
+
+contract Util {
+    function balanceOf(address reward, address user) external view returns (uint256) {
+        return IERC20(reward).balanceOf(user);
+    }
+}
diff --git a/certora/specs/MerkleTree.spec b/certora/specs/MerkleTree.spec
new file mode 100644
index 0000000..0754f38
--- /dev/null
+++ b/certora/specs/MerkleTree.spec
@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+methods {
+    function getValue(address, address) external returns(uint256) envfree;
+    function isEmpty(bytes32) external returns(bool) envfree;
+    function isWellFormed(bytes32) external returns(bool) envfree;
+}
+
+invariant zeroIsEmpty()
+    isEmpty(to_bytes32(0));
+
+invariant wellFormed(bytes32 id)
+    isWellFormed(id)
+{ preserved {
+    requireInvariant zeroIsEmpty();
+  }
+}
diff --git a/certora/specs/UniversalRewardsDistributor.spec b/certora/specs/UniversalRewardsDistributor.spec
new file mode 100644
index 0000000..51037c4
--- /dev/null
+++ b/certora/specs/UniversalRewardsDistributor.spec
@@ -0,0 +1,85 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+using MerkleTree as MerkleTree;
+using Util as Util;
+
+methods {
+    function root() external returns bytes32 envfree;
+    function ipfsHash() external returns bytes32 envfree;
+    function claimed(address, address) external returns(uint256) envfree;
+    function claim(address, address, uint256, bytes32[]) external returns(uint256) envfree;
+    function pendingRoot() external returns(bytes32, bytes32, uint256) envfree;
+
+    function MerkleTree.getValue(address, address) external returns(uint256) envfree;
+    function MerkleTree.getHash(bytes32) external returns(bytes32) envfree;
+    function MerkleTree.wellFormedPath(bytes32, bytes32[]) external envfree;
+
+    function _.balanceOf(address) external => DISPATCHER(true);
+    function _.transfer(address, uint256) external => DISPATCHER(true);
+    function _.transferFrom(address, address, uint256) external => DISPATCHER(true);
+
+    function Util.balanceOf(address, address) external returns(uint256) envfree;
+}
+
+// Check how accept root changes the storage.
+rule acceptRootStorageChange(env e) {
+    bytes32 pendingRoot; bytes32 pendingIpfsHash;
+    pendingRoot, pendingIpfsHash, _ = pendingRoot();
+
+    acceptRoot(e);
+
+    assert root() == pendingRoot;
+    assert ipfsHash() == pendingIpfsHash;
+}
+
+// Check an account claimed amount is correctly updated.
+rule updatedClaimedAmount(address account, address reward, uint256 claimable, bytes32[] proof) {
+    claim(account, reward, claimable, proof);
+
+    assert claimable == claimed(account, reward);
+}
+
+// Check an account can only claim greater amounts each time.
+rule increasingClaimedAmounts(address account, address reward, uint256 claimable, bytes32[] proof) {
+    uint256 claimed = claimed(account, reward);
+
+    claim(account, reward, claimable, proof);
+
+    assert claimable > claimed;
+}
+
+// Check that the transferred amount is equal to the claimed amount minus the previous claimed amount.
+rule transferredTokens(address account, address reward, uint256 claimable, bytes32[] proof) {
+    // Assume that the rewards distributor itself is not receiving the tokens, to simplify this rule.
+    require account != currentContract;
+
+    uint256 balanceBefore = Util.balanceOf(reward, account);
+    uint256 claimedBefore = claimed(account, reward);
+
+    // Safe require because the sum is capped by the total supply.
+    require balanceBefore + Util.balanceOf(reward, currentContract) < 2^256;
+
+    claim(account, reward, claimable, proof);
+
+    uint256 balanceAfter = Util.balanceOf(reward, account);
+
+    assert balanceAfter - balanceBefore == claimable - claimedBefore;
+}
+
+// The main correctness result of the verification.
+// It ensures that if the root is setup according to a well-formed Merkle tree, then claiming will result in receiving the rewards stored in the tree for that particular pair of account and reward.
+rule claimCorrectness(address account, address reward, uint256 claimable, bytes32[] proof) {
+    bytes32 node;
+
+    // Assume that root is the hash of node in the tree.
+    require MerkleTree.getHash(node) == root();
+
+    // No need to make sure that node is equal to currRoot: one can pass an internal node instead.
+
+    // Assume that the tree is well-formed.
+    MerkleTree.wellFormedPath(node, proof);
+
+    claim(account, reward, claimable, proof);
+
+    assert claimable == MerkleTree.getValue(account, reward);
+}
diff --git a/foundry.toml b/foundry.toml
index 60c9b35..58ce97c 100644
--- a/foundry.toml
+++ b/foundry.toml
@@ -50,3 +50,8 @@ max_test_rejects = 65536
 [profile.test-fast.invariant]
 runs = 16
 depth = 256
+
+[profile.checker]
+test = 'certora/checker'
+fs_permissions = [{access = "read", path= "./"}]
+match_contract = 'Checker'