diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
new file mode 100644
index 0000000..e231a4d
--- /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:
+        op-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.op-farms }}
+        run: make certora-${{ matrix.op-farms }} results=1
+        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/Makefile b/Makefile
new file mode 100644
index 0000000..71d2761
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,3 @@
+PATH := ~/.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..c1efa7f
--- /dev/null
+++ b/certora/L1FarmProxy.conf
@@ -0,0 +1,20 @@
+{
+    "files": [
+        "src/L1FarmProxy.sol",
+        "test/mocks/L1TokenBridgeMock.sol",
+        "test/mocks/GemMock.sol"
+    ],
+    "solc": "solc-0.8.21",
+    "solc_optimize": "200",
+    "link": [
+        "L1FarmProxy:l1Bridge=L1TokenBridgeMock"
+    ],
+    "verify": "L1FarmProxy:certora/L1FarmProxy.spec",
+    "rule_sanity": "basic",
+    "multi_assert_check": true,
+    "parametric_contracts": ["L1FarmProxy"],
+    "build_cache": true,
+    "optimistic_hashing": true,
+    "hashing_length_bound": "512",
+    "msg": "L1FarmProxy"
+}
diff --git a/certora/L1FarmProxy.spec b/certora/L1FarmProxy.spec
new file mode 100644
index 0000000..2b72b29
--- /dev/null
+++ b/certora/L1FarmProxy.spec
@@ -0,0 +1,238 @@
+// L1FarmProxy.spec
+
+using GemMock as gem;
+using L1TokenBridgeMock as l1Bridge;
+
+methods {
+    // storage variables
+    function wards(address) external returns (uint256) envfree;
+    function minGasLimit() external returns (uint32) envfree;
+    function rewardThreshold() external returns (uint224) envfree;
+    // immutables
+    function rewardsToken() external returns (address) envfree;
+    function remoteToken() external returns (address) envfree;
+    function l2Proxy() external returns (address) envfree;
+    function l1Bridge() external returns (address) 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 l1Bridge.escrow() external returns (address) envfree;
+    function l1Bridge.lastLocalToken() external returns (address) envfree;
+    function l1Bridge.lastRemoteToken() external returns (address) envfree;
+    function l1Bridge.lastTo() external returns (address) envfree;
+    function l1Bridge.lastAmount() external returns (uint256) envfree;
+    function l1Bridge.lastMinGasLimit() external returns (uint32) envfree;
+    function l1Bridge.lastExtraDataHash() external returns (bytes32) envfree;
+    function l1Bridge.getEmptyDataHash() external returns (bytes32) envfree;
+    //
+    function _.transfer(address,uint256) external => DISPATCHER(true);
+    function _.transferFrom(address,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 minGasLimitBefore = minGasLimit();
+    mathint rewardThresholdBefore = rewardThreshold();
+
+    calldataarg args;
+    f(e, args);
+
+    mathint wardsAfter = wards(anyAddr);
+    mathint minGasLimitAfter = minGasLimit();
+    mathint rewardThresholdAfter = rewardThreshold();
+
+    assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "Assert 1";
+    assert minGasLimitAfter != minGasLimitBefore => f.selector == sig:file(bytes32,uint256).selector, "Assert 2";
+    assert rewardThresholdAfter != rewardThresholdBefore => f.selector == sig:file(bytes32,uint256).selector, "Assert 3";
+}
+
+// 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 minGasLimitBefore = minGasLimit();
+    mathint rewardThresholdBefore = rewardThreshold();
+
+    file(e, what, data);
+
+    mathint minGasLimitAfter = minGasLimit();
+    mathint rewardThresholdAfter = rewardThreshold();
+
+    assert what == to_bytes32(0x6d696e4761734c696d6974000000000000000000000000000000000000000000) => minGasLimitAfter == data % (max_uint32 + 1), "Assert 1";
+    assert what != to_bytes32(0x6d696e4761734c696d6974000000000000000000000000000000000000000000) => minGasLimitAfter == minGasLimitBefore, "Assert 2";
+    assert what == to_bytes32(0x7265776172645468726573686f6c640000000000000000000000000000000000) => rewardThresholdAfter == data % (max_uint224 + 1), "Assert 3";
+    assert what != to_bytes32(0x7265776172645468726573686f6c640000000000000000000000000000000000) => rewardThresholdAfter == rewardThresholdBefore, "Assert 4";
+}
+
+// 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(0x6d696e4761734c696d6974000000000000000000000000000000000000000000) &&
+                   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 notifyRewardAmount
+rule notifyRewardAmount(uint256 reward) {
+    env e;
+
+    bytes32 emptyDataHash = l1Bridge.getEmptyDataHash();
+
+    notifyRewardAmount(e, reward);
+
+    address lastLocalTokenAfter = l1Bridge.lastLocalToken();
+    address lastRemoteTokenAfter = l1Bridge.lastRemoteToken();
+    address lastToAfter = l1Bridge.lastTo();
+    mathint lastAmountAfter = l1Bridge.lastAmount();
+    mathint lastMinGasLimitAfter = l1Bridge.lastMinGasLimit();
+    bytes32 lastExtraDataHashAfter = l1Bridge.lastExtraDataHash();
+
+    assert lastLocalTokenAfter == rewardsToken(), "Assert 1";
+    assert lastRemoteTokenAfter == remoteToken(), "Assert 2";
+    assert lastToAfter == l2Proxy(), "Assert 3";
+    assert lastAmountAfter == reward, "Assert 4";
+    assert lastMinGasLimitAfter == minGasLimit(), "Assert 5";
+    assert lastExtraDataHashAfter == emptyDataHash, "Assert 6";
+}
+
+// Verify revert rules on notifyRewardAmount
+rule notifyRewardAmount_revert(uint256 reward) {
+    env e;
+
+    require rewardsToken() == gem;
+
+    mathint rewardThreshold = rewardThreshold();
+    mathint rewardsTokenBalanceOfProxy = gem.balanceOf(currentContract);
+    address escrow = l1Bridge.escrow();
+    mathint rewardsTokenBalanceOfEscrow = gem.balanceOf(escrow);
+    // ERC20 assumption
+    require gem.totalSupply() >= rewardsTokenBalanceOfProxy + rewardsTokenBalanceOfEscrow;
+    // Happening in constructor
+    require gem.allowance(currentContract, l1Bridge) == max_uint256;
+
+    notifyRewardAmount@withrevert(e, reward);
+
+    bool revert1 = e.msg.value > 0;
+    bool revert2 = reward <= rewardThreshold;
+    bool revert3 = rewardsTokenBalanceOfProxy < reward;
+
+    assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed";
+}
diff --git a/certora/L2FarmProxy.conf b/certora/L2FarmProxy.conf
new file mode 100644
index 0000000..00db4ee
--- /dev/null
+++ b/certora/L2FarmProxy.conf
@@ -0,0 +1,20 @@
+{
+    "files": [
+        "src/L2FarmProxy.sol",
+        "test/mocks/GemMock.sol",
+        "test/mocks/FarmMock.sol"
+    ],
+    "solc": "solc-0.8.21",
+    "solc_optimize": "200",
+    "link": [
+        "L2FarmProxy:farm=FarmMock"
+    ],
+    "verify": "L2FarmProxy:certora/L2FarmProxy.spec",
+    "rule_sanity": "basic",
+    "multi_assert_check": true,
+    "parametric_contracts": ["L2FarmProxy"],
+    "build_cache": true,
+    "optimistic_hashing": true,
+    "hashing_length_bound": "512",
+    "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/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/L1TokenBridgeMock.sol b/test/mocks/L1TokenBridgeMock.sol
index 03b6ca5..8924030 100644
--- a/test/mocks/L1TokenBridgeMock.sol
+++ b/test/mocks/L1TokenBridgeMock.sol
@@ -24,18 +24,40 @@ interface TokenLike {
 contract L1TokenBridgeMock {
     address public immutable escrow;
 
+    address public lastLocalToken;
+    address public lastRemoteToken;
+    address public lastTo;
+    uint256 public lastAmount;
+    uint32  public lastMinGasLimit;
+    bytes32 public lastExtraDataHash;
+
     constructor(address _escrow) {
         escrow = _escrow;
     }
 
+    function getEmptyDataHash() public view returns (bytes32) {
+        return this.getDataHash("");
+    }
+
+    function getDataHash(bytes calldata data) public pure returns (bytes32) {
+        return keccak256(data);
+    }
+
     function bridgeERC20To(
         address        _localToken,
-        address        /* _remoteToken */,
-        address        /* _to */,
+        address        _remoteToken,
+        address        _to,
         uint256        _amount,
-        uint32         /* _minGasLimit */,
-        bytes calldata /* _extraData */
+        uint32         _minGasLimit,
+        bytes calldata _extraData
     ) public {
+        lastLocalToken = _localToken;
+        lastRemoteToken = _remoteToken;
+        lastTo = _to;
+        lastAmount = _amount;
+        lastMinGasLimit = _minGasLimit;
+        lastExtraDataHash = keccak256(_extraData);
+
         TokenLike(_localToken).transferFrom(msg.sender, escrow, _amount);
     }
 }