diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
new file mode 100644
index 0000000..0dca91e
--- /dev/null
+++ b/.github/workflows/certora.yml
@@ -0,0 +1,45 @@
+name: Certora
+
+on: [push, pull_request]
+
+jobs:
+  certora:
+    name: Certora
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        arbitrum-farms:
+          - l1-farm-proxy
+          - l2-farm-proxy
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      
+      - uses: actions/setup-java@v2
+        with:
+          distribution: 'zulu'
+          java-version: '11'
+          java-package: jre
+
+      - name: Set up Python 3.8
+        uses: actions/setup-python@v3
+        with:
+          python-version: 3.8
+
+      - name: Install solc-select
+        run: pip3 install solc-select
+
+      - name: Solc Select 0.8.21
+        run: solc-select install 0.8.21
+
+      - name: Install Certora
+        run: pip3 install certora-cli-beta
+
+      - name: Verify ${{ matrix.arbitrum-farms }}
+        run: make certora-${{ matrix.arbitrum-farms }} results=1
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
diff --git a/.gitignore b/.gitignore
index 87132a9..94e0926 100644
--- a/.gitignore
+++ b/.gitignore
@@ -12,3 +12,6 @@ docs/
 .env
 
 deployed-[0-9]*.json
+
+# Certora
+.certora_internal
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..8e30c4e
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,3 @@
+PATH := ~/.solc-select/artifacts/:~/.solc-select/artifacts/solc-0.8.21:$(PATH)
+certora-l1-farm-proxy :; PATH=${PATH} certoraRun certora/L1FarmProxy.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,)
+certora-l2-farm-proxy :; PATH=${PATH} certoraRun certora/L2FarmProxy.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,)
diff --git a/certora/L1FarmProxy.conf b/certora/L1FarmProxy.conf
new file mode 100644
index 0000000..5bf1501
--- /dev/null
+++ b/certora/L1FarmProxy.conf
@@ -0,0 +1,30 @@
+{
+    "files": [
+        "src/L1FarmProxy.sol",
+        "certora/harness/Auxiliar.sol",
+        "test/mocks/L1TokenGatewayMock.sol",
+        "test/mocks/InboxMock.sol",
+        "test/mocks/GemMock.sol",
+    ],
+    "solc": "solc-0.8.21",
+    "solc_optimize_map": {
+        "L1FarmProxy": "200",
+        "Auxiliar": "0",
+        "L1TokenGatewayMock": "0",
+        "InboxMock": "0",
+        "GemMock": "0"
+    },
+    "link": [
+        "L1FarmProxy:l1Gateway=L1TokenGatewayMock",
+        "L1FarmProxy:inbox=InboxMock"
+    ],
+    "verify": "L1FarmProxy:certora/L1FarmProxy.spec",
+    "rule_sanity": "basic",
+    "multi_assert_check": true,
+    "parametric_contracts": ["L1FarmProxy"],
+    "build_cache": true,
+    "optimistic_hashing": true,
+    "optimistic_fallback": true,
+    "hashing_length_bound": "512",
+    "msg": "L1FarmProxy"
+}
diff --git a/certora/L1FarmProxy.spec b/certora/L1FarmProxy.spec
new file mode 100644
index 0000000..46d63d7
--- /dev/null
+++ b/certora/L1FarmProxy.spec
@@ -0,0 +1,332 @@
+// L1FarmProxy.spec
+
+using GemMock as gem;
+using Auxiliar as aux;
+using L1TokenGatewayMock as l1Gateway;
+
+methods {
+    // storage variables
+    function wards(address) external returns (uint256) envfree;
+    function maxGas() external returns (uint64) envfree;
+    function gasPriceBid() external returns (uint64) envfree;
+    function rewardThreshold() external returns (uint128) envfree;
+    // immutables
+    function rewardsToken() external returns (address) envfree;
+    function l2Proxy() external returns (address) envfree;
+    function feeRecipient() external returns (address) envfree;
+    function l1Gateway() external returns (address) envfree;
+    //
+    function aux.getDataHash(uint256) external returns (bytes32) envfree;
+    function gem.allowance(address,address) external returns (uint256) envfree;
+    function gem.totalSupply() external returns (uint256) envfree;
+    function gem.balanceOf(address) external returns (uint256) envfree;
+    function l1Gateway.escrow() external returns (address) envfree;
+    function l1Gateway.lastL1Token() external returns (address) envfree;
+    function l1Gateway.lastRefundTo() external returns (address) envfree;
+    function l1Gateway.lastTo() external returns (address) envfree;
+    function l1Gateway.lastAmount() external returns (uint256) envfree;
+    function l1Gateway.lastMaxGas() external returns (uint256) envfree;
+    function l1Gateway.lastGasPriceBid() external returns (uint256) envfree;
+    function l1Gateway.lastDataHash() external returns (bytes32) envfree;
+    function l1Gateway.lastValue() external returns (uint256) envfree;
+    //
+    function _.transfer(address,uint256) external => DISPATCHER(true);
+    function _.transferFrom(address,address,uint256) external => DISPATCHER(true);
+}
+
+persistent ghost bool success;
+hook CALL(uint256 g, address addr, uint256 value, uint256 argsOffset, uint256 argsLength, uint256 retOffset, uint256 retLength) uint256 rc {
+    success = rc != 0;
+}
+
+// Verify that each storage layout is only modified in the corresponding functions
+rule storageAffected(method f) {
+    env e;
+
+    address anyAddr;
+
+    mathint wardsBefore = wards(anyAddr);
+    mathint maxGasBefore = maxGas();
+    mathint gasPriceBidBefore = gasPriceBid();
+    mathint rewardThresholdBefore = rewardThreshold();
+
+    calldataarg args;
+    f(e, args);
+
+    mathint wardsAfter = wards(anyAddr);
+    mathint maxGasAfter = maxGas();
+    mathint gasPriceBidAfter = gasPriceBid();
+    mathint rewardThresholdAfter = rewardThreshold();
+
+    assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "Assert 1";
+    assert maxGasAfter != maxGasBefore => f.selector == sig:file(bytes32,uint256).selector, "Assert 2";
+    assert gasPriceBidAfter != gasPriceBidBefore => f.selector == sig:file(bytes32,uint256).selector, "Assert 3";
+    assert rewardThresholdAfter != rewardThresholdBefore => f.selector == sig:file(bytes32,uint256).selector, "Assert 4";
+}
+
+// Verify correct storage changes for non reverting rely
+rule rely(address usr) {
+    env e;
+
+    address other;
+    require other != usr;
+
+    mathint wardsOtherBefore = wards(other);
+
+    rely(e, usr);
+
+    mathint wardsUsrAfter = wards(usr);
+    mathint wardsOtherAfter = wards(other);
+
+    assert wardsUsrAfter == 1, "Assert 1";
+    assert wardsOtherAfter == wardsOtherBefore, "Assert 2";
+}
+
+// Verify revert rules on rely
+rule rely_revert(address usr) {
+    env e;
+
+    mathint wardsSender = wards(e.msg.sender);
+
+    rely@withrevert(e, usr);
+
+    bool revert1 = e.msg.value > 0;
+    bool revert2 = wardsSender != 1;
+
+    assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting deny
+rule deny(address usr) {
+    env e;
+
+    address other;
+    require other != usr;
+
+    mathint wardsOtherBefore = wards(other);
+
+    deny(e, usr);
+
+    mathint wardsUsrAfter = wards(usr);
+    mathint wardsOtherAfter = wards(other);
+
+    assert wardsUsrAfter == 0, "Assert 1";
+    assert wardsOtherAfter == wardsOtherBefore, "Assert 2";
+}
+
+// Verify revert rules on deny
+rule deny_revert(address usr) {
+    env e;
+
+    mathint wardsSender = wards(e.msg.sender);
+
+    deny@withrevert(e, usr);
+
+    bool revert1 = e.msg.value > 0;
+    bool revert2 = wardsSender != 1;
+
+    assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting file
+rule file(bytes32 what, uint256 data) {
+    env e;
+
+    mathint maxGasBefore = maxGas();
+    mathint gasPriceBidBefore = gasPriceBid();
+    mathint rewardThresholdBefore = rewardThreshold();
+
+    file(e, what, data);
+
+    mathint maxGasAfter = maxGas();
+    mathint gasPriceBidAfter = gasPriceBid();
+    mathint rewardThresholdAfter = rewardThreshold();
+
+    assert what == to_bytes32(0x6d61784761730000000000000000000000000000000000000000000000000000) => maxGasAfter == data % (max_uint64 + 1), "Assert 1";
+    assert what != to_bytes32(0x6d61784761730000000000000000000000000000000000000000000000000000) => maxGasAfter == maxGasBefore, "Assert 2";
+    assert what == to_bytes32(0x6761735072696365426964000000000000000000000000000000000000000000) => gasPriceBidAfter == data % (max_uint64 + 1), "Assert 3";
+    assert what != to_bytes32(0x6761735072696365426964000000000000000000000000000000000000000000) => gasPriceBidAfter == gasPriceBidBefore, "Assert 4";
+    assert what == to_bytes32(0x7265776172645468726573686f6c640000000000000000000000000000000000) => rewardThresholdAfter == data % (max_uint128 + 1), "Assert 5";
+    assert what != to_bytes32(0x7265776172645468726573686f6c640000000000000000000000000000000000) => rewardThresholdAfter == rewardThresholdBefore, "Assert 6";
+}
+
+// Verify revert rules on file
+rule file_revert(bytes32 what, uint256 data) {
+    env e;
+
+    mathint wardsSender = wards(e.msg.sender);
+
+    file@withrevert(e, what, data);
+
+    bool revert1 = e.msg.value > 0;
+    bool revert2 = wardsSender != 1;
+    bool revert3 = what != to_bytes32(0x6d61784761730000000000000000000000000000000000000000000000000000) &&
+                   what != to_bytes32(0x6761735072696365426964000000000000000000000000000000000000000000) &&
+                   what != to_bytes32(0x7265776172645468726573686f6c640000000000000000000000000000000000);
+
+    assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting reclaim
+rule reclaim(address receiver, uint256 amount) {
+    env e;
+
+    // require receiver == rec;
+
+    mathint balanceProxyBefore = nativeBalances[currentContract];
+    mathint balanceReceiverBefore = nativeBalances[receiver];
+    // ERC20 assumption
+    require gem.totalSupply() >= balanceProxyBefore + balanceReceiverBefore;
+
+    reclaim(e, receiver, amount);
+
+    mathint balanceProxyAfter = nativeBalances[currentContract];
+    mathint balanceReceiverAfter = nativeBalances[receiver];
+
+    assert currentContract != receiver => balanceProxyAfter == balanceProxyBefore - amount, "Assert 1";
+    assert currentContract != receiver => balanceReceiverAfter == balanceReceiverBefore + amount, "Assert 2";
+    assert currentContract == receiver => balanceProxyAfter == balanceProxyBefore, "Assert 3";
+}
+
+// Verify revert rules on reclaim
+rule reclaim_revert(address receiver, uint256 amount) {
+    env e;
+
+    mathint balanceProxy = nativeBalances[currentContract];
+    // Practical assumption
+    require nativeBalances[receiver] + amount <= max_uint256;
+
+    mathint wardsSender = wards(e.msg.sender);
+
+    reclaim@withrevert(e, receiver, amount);
+
+    bool revert1 = e.msg.value > 0;
+    bool revert2 = wardsSender != 1;
+    bool revert3 = balanceProxy < amount;
+    bool revert4 = !success;
+
+    assert lastReverted <=> revert1 || revert2 || revert3 ||
+                            revert4, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting recover
+rule recover(address token, address receiver, uint256 amount) {
+    env e;
+
+    require token == gem;
+
+    mathint tokenBalanceOfProxyBefore = gem.balanceOf(currentContract);
+    mathint tokenBalanceOfReceiverBefore = gem.balanceOf(receiver);
+    // ERC20 assumption
+    require gem.totalSupply() >= tokenBalanceOfProxyBefore + tokenBalanceOfReceiverBefore;
+
+    recover(e, token, receiver, amount);
+
+    mathint tokenBalanceOfProxyAfter = gem.balanceOf(currentContract);
+    mathint tokenBalanceOfReceiverAfter = gem.balanceOf(receiver);
+
+    assert currentContract != receiver => tokenBalanceOfProxyAfter == tokenBalanceOfProxyBefore - amount, "Assert 1";
+    assert currentContract != receiver => tokenBalanceOfReceiverAfter == tokenBalanceOfReceiverBefore + amount, "Assert 2";
+    assert currentContract == receiver => tokenBalanceOfProxyAfter == tokenBalanceOfProxyBefore, "Assert 3";
+}
+
+// Verify revert rules on recover
+rule recover_revert(address token, address receiver, uint256 amount) {
+    env e;
+
+    mathint tokenBalanceOfProxy = gem.balanceOf(currentContract);
+    // ERC20 assumption
+    require gem.totalSupply() >= tokenBalanceOfProxy + gem.balanceOf(receiver);
+
+    mathint wardsSender = wards(e.msg.sender);
+
+    recover@withrevert(e, token, receiver, amount);
+
+    bool revert1 = e.msg.value > 0;
+    bool revert2 = wardsSender != 1;
+    bool revert3 = tokenBalanceOfProxy < amount;
+
+    assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed";
+}
+
+// Verify correct estimateDepositCost getter behavior
+rule estimateDepositCost(uint256 l1BaseFee, uint256 _maxGas, uint256 _gasPriceBid) {
+    env e;
+
+    mathint maxSubmissionCost = (1400 + 6 * 324) * (l1BaseFee == 0 ? 30 * 10^9 : l1BaseFee);
+    mathint l1CallValue = maxSubmissionCost + (_maxGas > 0 ? _maxGas : maxGas()) * (_gasPriceBid > 0 ? _gasPriceBid : gasPriceBid());
+
+    mathint l1CallValueRet; mathint maxSubmissionCostRet;
+    l1CallValueRet, maxSubmissionCostRet = estimateDepositCost(e, l1BaseFee, _maxGas, _gasPriceBid);
+
+    assert l1CallValueRet == l1CallValue, "Assert 1";
+    assert maxSubmissionCostRet == maxSubmissionCost, "Assert 2";
+}
+
+// Verify correct storage changes for non reverting notifyRewardAmount
+rule notifyRewardAmount(uint256 reward) {
+    env e;
+
+    address rewardsToken = rewardsToken();
+    address l2Proxy = l2Proxy();
+    address feeRecipient = feeRecipient();
+    mathint maxGas = maxGas();
+    mathint gasPriceBid = gasPriceBid();
+    uint256 maxSubmissionCost = (1400 + 6 * 324) * 30*10^9;
+    bytes32 dataHash = aux.getDataHash(maxSubmissionCost);
+    mathint l1CallValue = maxSubmissionCost + maxGas * gasPriceBid;
+
+    notifyRewardAmount(e, reward);
+
+    address lastL1TokenAfter = l1Gateway.lastL1Token();
+    address lastRefundToAfter = l1Gateway.lastRefundTo();
+    address lastToAfter = l1Gateway.lastTo();
+    mathint lastAmountAfter = l1Gateway.lastAmount();
+    mathint lastMaxGasAfter = l1Gateway.lastMaxGas();
+    mathint lastGasPriceBidAfter = l1Gateway.lastGasPriceBid();
+    bytes32 lastDataHashAfter = l1Gateway.lastDataHash();
+    mathint lastValueAfter = l1Gateway.lastValue();
+
+    assert lastL1TokenAfter == rewardsToken, "Assert 1";
+    assert lastRefundToAfter == feeRecipient, "Assert 2";
+    assert lastToAfter == l2Proxy, "Assert 3";
+    assert lastAmountAfter == to_mathint(reward), "Assert 4";
+    assert lastMaxGasAfter == maxGas, "Assert 5";
+    assert lastGasPriceBidAfter == gasPriceBid, "Assert 6";
+    assert lastDataHashAfter == dataHash, "Assert 7";
+    assert lastValueAfter == l1CallValue, "Assert 8";
+}
+
+// Verify revert rules on notifyRewardAmount
+rule notifyRewardAmount_revert(uint256 reward) {
+    env e;
+
+    require rewardsToken() == gem;
+
+    mathint maxGas = maxGas();
+    mathint gasPriceBid = gasPriceBid();
+    mathint rewardThreshold = rewardThreshold();
+    mathint rewardsTokenBalanceOfProxy = gem.balanceOf(currentContract);
+    address escrow = l1Gateway.escrow();
+    mathint rewardsTokenBalanceOfEscrow = gem.balanceOf(escrow);
+    // ERC20 assumption
+    require gem.totalSupply() >= rewardsTokenBalanceOfProxy + rewardsTokenBalanceOfEscrow;
+    // Happening in constructor
+    require gem.allowance(currentContract, l1Gateway) == max_uint256;
+
+    mathint balanceProxy = nativeBalances[currentContract];
+    uint256 maxSubmissionCost = (1400 + 6 * 324) * 30*10^9;
+    mathint l1CallValue = maxSubmissionCost + maxGas * gasPriceBid;
+    // Practical assumption
+    require nativeBalances[l1Gateway] + l1CallValue <= max_uint256;
+
+    notifyRewardAmount@withrevert(e, reward);
+
+    bool revert1 = e.msg.value > 0;
+    bool revert2 = reward <= rewardThreshold;
+    bool revert3 = balanceProxy < l1CallValue;
+    bool revert4 = rewardsTokenBalanceOfProxy < reward;
+
+    assert lastReverted <=> revert1 || revert2 || revert3 ||
+                            revert4, "Revert rules failed";
+}
diff --git a/certora/L2FarmProxy.conf b/certora/L2FarmProxy.conf
new file mode 100644
index 0000000..e45537f
--- /dev/null
+++ b/certora/L2FarmProxy.conf
@@ -0,0 +1,22 @@
+{
+    "files": [
+        "src/L2FarmProxy.sol",
+        "test/mocks/GemMock.sol",
+        "test/mocks/FarmMock.sol"
+    ],
+    "solc": "solc-0.8.21",
+    "solc_optimize_map": {
+        "L2FarmProxy": "200",
+        "GemMock": "0",
+        "FarmMock": "0"
+    },
+    "link": [
+        "L2FarmProxy:farm=FarmMock"
+    ],
+    "verify": "L2FarmProxy:certora/L2FarmProxy.spec",
+    "rule_sanity": "basic",
+    "multi_assert_check": true,
+    "parametric_contracts": ["L2FarmProxy"],
+    "build_cache": true,
+    "msg": "L2FarmProxy"
+}
diff --git a/certora/L2FarmProxy.spec b/certora/L2FarmProxy.spec
new file mode 100644
index 0000000..dd062d1
--- /dev/null
+++ b/certora/L2FarmProxy.spec
@@ -0,0 +1,208 @@
+// L2FarmProxy.spec
+
+using GemMock as gem;
+using FarmMock as farm;
+
+methods {
+    // storage variables
+    function wards(address) external returns (uint256) envfree;
+    function rewardThreshold() external returns (uint256) envfree;
+    // immutables
+    function rewardsToken() external returns (address) envfree;
+    function farm() external returns (address) envfree;
+    //
+    function gem.totalSupply() external returns (uint256) envfree;
+    function gem.balanceOf(address) external returns (uint256) envfree;
+    function farm.lastReward() external returns (uint256) envfree;
+    //
+    function _.balanceOf(address) external => DISPATCHER(true);
+    function _.transfer(address,uint256) external => DISPATCHER(true);
+}
+
+// Verify that each storage layout is only modified in the corresponding functions
+rule storageAffected(method f) {
+    env e;
+
+    address anyAddr;
+
+    mathint wardsBefore = wards(anyAddr);
+    mathint rewardThresholdBefore = rewardThreshold();
+
+    calldataarg args;
+    f(e, args);
+
+    mathint wardsAfter = wards(anyAddr);
+    mathint rewardThresholdAfter = rewardThreshold();
+
+    assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "Assert 1";
+    assert rewardThresholdAfter != rewardThresholdBefore => f.selector == sig:file(bytes32,uint256).selector, "Assert 2";
+}
+
+// Verify correct storage changes for non reverting rely
+rule rely(address usr) {
+    env e;
+
+    address other;
+    require other != usr;
+
+    mathint wardsOtherBefore = wards(other);
+
+    rely(e, usr);
+
+    mathint wardsUsrAfter = wards(usr);
+    mathint wardsOtherAfter = wards(other);
+
+    assert wardsUsrAfter == 1, "Assert 1";
+    assert wardsOtherAfter == wardsOtherBefore, "Assert 2";
+}
+
+// Verify revert rules on rely
+rule rely_revert(address usr) {
+    env e;
+
+    mathint wardsSender = wards(e.msg.sender);
+
+    rely@withrevert(e, usr);
+
+    bool revert1 = e.msg.value > 0;
+    bool revert2 = wardsSender != 1;
+
+    assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting deny
+rule deny(address usr) {
+    env e;
+
+    address other;
+    require other != usr;
+
+    mathint wardsOtherBefore = wards(other);
+
+    deny(e, usr);
+
+    mathint wardsUsrAfter = wards(usr);
+    mathint wardsOtherAfter = wards(other);
+
+    assert wardsUsrAfter == 0, "Assert 1";
+    assert wardsOtherAfter == wardsOtherBefore, "Assert 2";
+}
+
+// Verify revert rules on deny
+rule deny_revert(address usr) {
+    env e;
+
+    mathint wardsSender = wards(e.msg.sender);
+
+    deny@withrevert(e, usr);
+
+    bool revert1 = e.msg.value > 0;
+    bool revert2 = wardsSender != 1;
+
+    assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting file
+rule file(bytes32 what, uint256 data) {
+    env e;
+
+    file(e, what, data);
+
+    mathint rewardThresholdAfter = rewardThreshold();
+
+    assert rewardThresholdAfter == data, "Assert 1";
+}
+
+// Verify revert rules on file
+rule file_revert(bytes32 what, uint256 data) {
+    env e;
+
+    mathint wardsSender = wards(e.msg.sender);
+
+    file@withrevert(e, what, data);
+
+    bool revert1 = e.msg.value > 0;
+    bool revert2 = wardsSender != 1;
+    bool revert3 = what != to_bytes32(0x7265776172645468726573686f6c640000000000000000000000000000000000);
+
+    assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting recover
+rule recover(address token, address receiver, uint256 amount) {
+    env e;
+
+    require token == gem;
+
+    mathint tokenBalanceOfProxyBefore = gem.balanceOf(currentContract);
+    mathint tokenBalanceOfReceiverBefore = gem.balanceOf(receiver);
+    // ERC20 assumption
+    require gem.totalSupply() >= tokenBalanceOfProxyBefore + tokenBalanceOfReceiverBefore;
+
+    recover(e, token, receiver, amount);
+
+    mathint tokenBalanceOfProxyAfter = gem.balanceOf(currentContract);
+    mathint tokenBalanceOfReceiverAfter = gem.balanceOf(receiver);
+
+    assert currentContract != receiver => tokenBalanceOfProxyAfter == tokenBalanceOfProxyBefore - amount, "Assert 1";
+    assert currentContract != receiver => tokenBalanceOfReceiverAfter == tokenBalanceOfReceiverBefore + amount, "Assert 2";
+    assert currentContract == receiver => tokenBalanceOfProxyAfter == tokenBalanceOfProxyBefore, "Assert 3";
+}
+
+// Verify revert rules on recover
+rule recover_revert(address token, address receiver, uint256 amount) {
+    env e;
+
+    mathint tokenBalanceOfProxy = gem.balanceOf(currentContract);
+    // ERC20 assumption
+    require gem.totalSupply() >= tokenBalanceOfProxy + gem.balanceOf(receiver);
+
+    mathint wardsSender = wards(e.msg.sender);
+
+    recover@withrevert(e, token, receiver, amount);
+
+    bool revert1 = e.msg.value > 0;
+    bool revert2 = wardsSender != 1;
+    bool revert3 = tokenBalanceOfProxy < amount;
+
+    assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting forwardReward
+rule forwardReward() {
+    env e;
+
+    require rewardsToken() == gem;
+
+    mathint rewardsTokenBalanceOfProxyBefore = gem.balanceOf(currentContract);
+    mathint rewardsTokenBalanceOfFarmBefore = gem.balanceOf(farm);
+    // ERC20 assumption
+    require gem.totalSupply() >= rewardsTokenBalanceOfProxyBefore + rewardsTokenBalanceOfFarmBefore;
+
+    forwardReward(e);
+
+    mathint rewardsTokenBalanceOfProxyAfter = gem.balanceOf(currentContract);
+    mathint rewardsTokenBalanceOfFarmAfter = gem.balanceOf(farm);
+    mathint farmLastRewardAfter = farm.lastReward();
+
+    assert rewardsTokenBalanceOfProxyAfter == 0, "Assert 1";
+    assert rewardsTokenBalanceOfFarmAfter == rewardsTokenBalanceOfFarmBefore + rewardsTokenBalanceOfProxyBefore, "Assert 2";
+    assert farmLastRewardAfter == rewardsTokenBalanceOfProxyBefore, "Assert 3";
+}
+
+// Verify revert rules on forwardReward
+rule forwardReward_revert() {
+    env e;
+
+    mathint rewardThreshold = rewardThreshold();
+    mathint rewardsTokenBalanceOfProxy = gem.balanceOf(currentContract);
+    // ERC20 assumption
+    require gem.totalSupply() >= gem.balanceOf(currentContract) + gem.balanceOf(farm);
+
+    forwardReward@withrevert(e);
+
+    bool revert1 = e.msg.value > 0;
+    bool revert2 = rewardsTokenBalanceOfProxy <= rewardThreshold;
+
+    assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
diff --git a/certora/harness/Auxiliar.sol b/certora/harness/Auxiliar.sol
new file mode 100644
index 0000000..b4ec010
--- /dev/null
+++ b/certora/harness/Auxiliar.sol
@@ -0,0 +1,28 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+
+// Copyright (C) 2024 Dai Foundation
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU Affero General Public License as published by
+// the Free Software Foundation, either version 3 of the License, or
+// (at your option) any later version.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU Affero General Public License for more details.
+//
+// You should have received a copy of the GNU Affero General Public License
+// along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+pragma solidity ^0.8.21;
+
+contract Auxiliar {
+    function getDataHash(uint256 maxSubmissionCost) public view returns (bytes32) {
+        return this.getDataHash(maxSubmissionCost, "");
+    }
+
+    function getDataHash(uint256 maxSubmissionCost, bytes calldata data) public pure returns (bytes32) {
+        return keccak256(abi.encode(maxSubmissionCost, data));
+    }
+}
diff --git a/script/BurnNonces.s.sol b/script/BurnNonces.s.sol
new file mode 100644
index 0000000..eec9f5d
--- /dev/null
+++ b/script/BurnNonces.s.sol
@@ -0,0 +1,66 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+
+// Copyright (C) 2024 Dai Foundation
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU Affero General Public License as published by
+// the Free Software Foundation, either version 3 of the License, or
+// (at your option) any later version.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU Affero General Public License for more details.
+//
+// You should have received a copy of the GNU Affero General Public License
+// along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+pragma solidity ^0.8.21;
+
+import "forge-std/Script.sol";
+
+import { ScriptTools } from "dss-test/ScriptTools.sol";
+import { Domain } from "dss-test/domains/Domain.sol";
+
+contract BurnNonces is Script {
+    uint256 l2PrivKey = vm.envUint("L2_PRIVATE_KEY");
+    address l2Deployer = vm.addr(l2PrivKey);
+
+    StdChains.Chain l1Chain;
+    StdChains.Chain l2Chain;
+    string config;
+    Domain l1Domain;
+    Domain l2Domain;
+    address deployer;
+    address l1GovRelay;
+    address l2GovRelay;
+    address l2Spell;
+    address etherForwarder;
+
+    function run() external {
+        l1Chain = getChain(string(vm.envOr("L1", string("mainnet"))));
+        l2Chain = getChain(string(vm.envOr("L2", string("arbitrum_one"))));
+        vm.setEnv("FOUNDRY_ROOT_CHAINID", vm.toString(l1Chain.chainId)); // used by ScriptTools to determine config path
+        config = ScriptTools.loadConfig("config");
+        l1Domain = new Domain(config, l1Chain);
+        l2Domain = new Domain(config, l2Chain);
+
+        // Check deployer's L2 nonce was burned on L1
+
+        l2Domain.selectFork();
+        uint256 l2Nonce = vm.getNonce(l2Deployer);
+        l1Domain.selectFork();
+        uint256 l1Nonce = vm.getNonce(l2Deployer);
+
+        if (l2Nonce >= l1Nonce) {
+            uint256 i = l2Nonce - l1Nonce + 1;
+            vm.startBroadcast(l2PrivKey);
+            while (i > 0) {
+                (bool success,) = l2Deployer.call{value: 0}("");
+                require(success, "l2Deployer burn nonce failed");
+                i--;
+            }
+            vm.stopBroadcast();
+        }
+    }
+}
diff --git a/test/mocks/FarmMock.sol b/test/mocks/FarmMock.sol
index 151c89e..d68fc4a 100644
--- a/test/mocks/FarmMock.sol
+++ b/test/mocks/FarmMock.sol
@@ -21,6 +21,8 @@ contract FarmMock {
     address public immutable rewardsToken;
     address public immutable stakingToken;
 
+    uint256 public lastReward;
+
     event OwnerNominated(address newOwner);
     event PauseChanged(bool isPaused);
     event RewardAdded(uint256 rewards);
@@ -42,6 +44,7 @@ contract FarmMock {
     }
 
     function notifyRewardAmount(uint256 reward) external {
+        lastReward = reward;
         emit RewardAdded(reward);
     }
 
diff --git a/test/mocks/L1TokenGatewayMock.sol b/test/mocks/L1TokenGatewayMock.sol
index 6181bdc..7d7a889 100644
--- a/test/mocks/L1TokenGatewayMock.sol
+++ b/test/mocks/L1TokenGatewayMock.sol
@@ -25,6 +25,15 @@ contract L1TokenGatewayMock {
     address public immutable inbox;
     address public immutable escrow;
 
+    address public lastL1Token;
+    address public lastRefundTo;
+    address public lastTo;
+    uint256 public lastAmount;
+    uint256 public lastMaxGas;
+    uint256 public lastGasPriceBid;
+    bytes32 public lastDataHash;
+    uint256 public lastValue;
+
     constructor(
         address _inbox,
         address _escrow
@@ -35,13 +44,22 @@ contract L1TokenGatewayMock {
 
     function outboundTransferCustomRefund(
         address l1Token,
-        address /* refundTo */,
-        address /* to */,
+        address refundTo,
+        address to,
         uint256 amount,
-        uint256 /* maxGas */,
-        uint256 /* gasPriceBid */,
-        bytes calldata /* data */
+        uint256 maxGas,
+        uint256 gasPriceBid,
+        bytes calldata data
     ) public payable returns (bytes memory res) {
+        lastL1Token = l1Token;
+        lastRefundTo = refundTo;
+        lastTo = to;
+        lastAmount = amount;
+        lastMaxGas = maxGas;
+        lastGasPriceBid = gasPriceBid;
+        lastDataHash = keccak256(data);
+        lastValue = msg.value;
+
         TokenLike(l1Token).transferFrom(msg.sender, escrow, amount);
         res = abi.encode(0);
     }