diff --git a/Makefile b/Makefile
index af591cea..9dbaf41e 100644
--- a/Makefile
+++ b/Makefile
@@ -1,10 +1,11 @@
-certora-buffer          		:; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorBuffer=solc-0.8.16,GemMock=solc-0.8.16 --solc_optimize_map AllocatorBuffer=200,GemMock=0 --rule_sanity basic src/AllocatorBuffer.sol test/mocks/GemMock.sol --verify AllocatorBuffer:certora/AllocatorBuffer.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results
-certora-vault           		:; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorVault=solc-0.8.16,AllocatorRoles=solc-0.8.16,VatMock=solc-0.8.16,JugMock=solc-0.8.16,NstJoinMock=solc-0.8.16,NstMock=solc-0.8.16 --solc_optimize_map AllocatorVault=200,AllocatorRoles=200,VatMock=0,JugMock=0,NstJoinMock=0,NstMock=0 --rule_sanity basic src/AllocatorVault.sol src/AllocatorRoles.sol test/mocks/VatMock.sol test/mocks/JugMock.sol test/mocks/NstJoinMock.sol test/mocks/NstMock.sol --link AllocatorVault:roles=AllocatorRoles AllocatorVault:vat=VatMock AllocatorVault:jug=JugMock AllocatorVault:nstJoin=NstJoinMock AllocatorVault:nst=NstMock JugMock:vat=VatMock NstJoinMock:vat=VatMock NstJoinMock:nst=NstMock --verify AllocatorVault:certora/AllocatorVault.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results --multi_assert_check
-certora-roles           		:; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorRoles=solc-0.8.16 --solc_optimize_map AllocatorRoles=200 --rule_sanity basic src/AllocatorRoles.sol --verify AllocatorRoles:certora/AllocatorRoles.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results
-certora-oracle          		:; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorOracle=solc-0.8.16 --solc_optimize_map AllocatorOracle=200 --rule_sanity basic src/AllocatorOracle.sol --verify AllocatorOracle:certora/AllocatorOracle.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results
-certora-registry        		:; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorRegistry=solc-0.8.16 --solc_optimize_map AllocatorRegistry=200 --rule_sanity basic src/AllocatorRegistry.sol --verify AllocatorRegistry:certora/AllocatorRegistry.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results
-certora-swapper         		:; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map Swapper=solc-0.8.16,AllocatorRoles=solc-0.8.16,Gem0Mock=solc-0.8.16,Gem1Mock=solc-0.8.16,CalleeMock=solc-0.8.16 --solc_optimize_map Swapper=200,AllocatorRoles=200,Gem0Mock=0,Gem1Mock=0,CalleeMock=0 --rule_sanity basic src/funnels/Swapper.sol src/AllocatorRoles.sol test/mocks/Gem0Mock.sol test/mocks/Gem1Mock.sol test/mocks/CalleeMock.sol --link Swapper:roles=AllocatorRoles --verify Swapper:certora/funnels/Swapper.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results
-certora-depositoruniv3  		:; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map DepositorUniV3=solc-0.8.16,AllocatorRoles=solc-0.8.16,PoolUniV3Mock=solc-0.8.16,Gem0Mock=solc-0.8.16,Gem1Mock=solc-0.8.16,Auxiliar=solc-0.8.16 --solc_optimize_map DepositorUniV3=200,AllocatorRoles=200,PoolUniV3Mock=0,Gem0Mock=0,Gem1Mock=0,Auxiliar=0 --rule_sanity basic src/funnels/DepositorUniV3.sol src/AllocatorRoles.sol test/mocks/PoolUniV3Mock.sol test/mocks/Gem0Mock.sol test/mocks/Gem1Mock.sol certora/funnels/Auxiliar.sol --link DepositorUniV3:roles=AllocatorRoles --verify DepositorUniV3:certora/funnels/DepositorUniV3.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results
-certora-stable-swapper  		:; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map StableSwapper=solc-0.8.16 --solc_optimize_map StableSwapper=200 --rule_sanity basic src/funnels/automation/StableSwapper.sol --verify StableSwapper:certora/funnels/automation/StableSwapper.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results
-certora-stable-depositoruniv3  	:; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map StableDepositorUniV3=solc-0.8.16 --solc_optimize_map StableDepositorUniV3=200 --rule_sanity basic src/funnels/automation/StableDepositorUniV3.sol --verify StableDepositorUniV3:certora/funnels/automation/StableDepositorUniV3.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results
-certora-conduit-mover		  	:; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map ConduitMover=solc-0.8.16 --solc_optimize_map ConduitMover=200 --rule_sanity basic src/funnels/automation/ConduitMover.sol --verify ConduitMover:certora/funnels/automation/ConduitMover.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results
+PATH := ~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:$(PATH)
+certora-buffer                :; PATH=${PATH} certoraRun certora/AllocatorBuffer.conf$(if $(rule), --rule $(rule),)
+certora-vault                 :; PATH=${PATH} certoraRun certora/AllocatorVault.conf$(if $(rule), --rule $(rule),)
+certora-roles                 :; PATH=${PATH} certoraRun certora/AllocatorRoles.conf$(if $(rule), --rule $(rule),)
+certora-oracle                :; PATH=${PATH} certoraRun certora/AllocatorOracle.conf$(if $(rule), --rule $(rule),)
+certora-registry              :; PATH=${PATH} certoraRun certora/AllocatorRegistry.conf$(if $(rule), --rule $(rule),)
+certora-swapper               :; PATH=${PATH} certoraRun certora/funnels/Swapper.conf$(if $(rule), --rule $(rule),)
+certora-depositoruniv3        :; PATH=${PATH} certoraRun certora/funnels/DepositorUniV3.conf$(if $(rule), --rule $(rule),)
+certora-stable-swapper        :; PATH=${PATH} certoraRun certora/funnels/automation/StableSwapper.conf$(if $(rule), --rule $(rule),)
+certora-stable-depositoruniv3 :; PATH=${PATH} certoraRun certora/funnels/automation/StableDepositorUniV3.conf$(if $(rule), --rule $(rule),)
+certora-conduit-mover         :; PATH=${PATH} certoraRun certora/funnels/automation/ConduitMover.conf$(if $(rule), --rule $(rule),)
diff --git a/certora/AllocatorBuffer.conf b/certora/AllocatorBuffer.conf
new file mode 100644
index 00000000..dab8c6b1
--- /dev/null
+++ b/certora/AllocatorBuffer.conf
@@ -0,0 +1,14 @@
+{
+    "files": [
+        "src/AllocatorBuffer.sol",
+        "test/mocks/GemMock.sol"
+    ],
+    "rule_sanity": "basic",
+    "solc": "solc-0.8.16",
+    "solc_optimize_map": {
+        "AllocatorBuffer": "200",
+        "GemMock": "0"
+    },
+    "verify": "AllocatorBuffer:certora/AllocatorBuffer.spec",
+    "wait_for_results": "all"
+}
diff --git a/certora/AllocatorOracle.conf b/certora/AllocatorOracle.conf
new file mode 100644
index 00000000..127e1c57
--- /dev/null
+++ b/certora/AllocatorOracle.conf
@@ -0,0 +1,10 @@
+{
+    "files": [
+        "src/AllocatorOracle.sol"
+    ],
+    "rule_sanity": "basic",
+    "solc": "solc-0.8.16",
+    "solc_optimize": "200",
+    "verify": "AllocatorOracle:certora/AllocatorOracle.spec",
+    "wait_for_results": "all"
+}
diff --git a/certora/AllocatorRegistry.conf b/certora/AllocatorRegistry.conf
new file mode 100644
index 00000000..7bb23ed5
--- /dev/null
+++ b/certora/AllocatorRegistry.conf
@@ -0,0 +1,10 @@
+{
+    "files": [
+        "src/AllocatorRegistry.sol"
+    ],
+    "rule_sanity": "basic",
+    "solc": "solc-0.8.16",
+    "solc_optimize": "200",
+    "verify": "AllocatorRegistry:certora/AllocatorRegistry.spec",
+    "wait_for_results": "all"
+}
diff --git a/certora/AllocatorRoles.conf b/certora/AllocatorRoles.conf
new file mode 100644
index 00000000..10376ef8
--- /dev/null
+++ b/certora/AllocatorRoles.conf
@@ -0,0 +1,10 @@
+{
+    "files": [
+        "src/AllocatorRoles.sol"
+    ],
+    "rule_sanity": "basic",
+    "solc": "solc-0.8.16",
+    "solc_optimize": "200",
+    "verify": "AllocatorRoles:certora/AllocatorRoles.spec",
+    "wait_for_results": "all"
+}
diff --git a/certora/AllocatorVault.conf b/certora/AllocatorVault.conf
new file mode 100644
index 00000000..316281ca
--- /dev/null
+++ b/certora/AllocatorVault.conf
@@ -0,0 +1,33 @@
+{
+    "files": [
+        "src/AllocatorVault.sol",
+        "src/AllocatorRoles.sol",
+        "test/mocks/VatMock.sol",
+        "test/mocks/JugMock.sol",
+        "test/mocks/NstJoinMock.sol",
+        "test/mocks/NstMock.sol"
+    ],
+    "link": [
+        "AllocatorVault:roles=AllocatorRoles",
+        "AllocatorVault:vat=VatMock",
+        "AllocatorVault:jug=JugMock",
+        "AllocatorVault:nstJoin=NstJoinMock",
+        "AllocatorVault:nst=NstMock",
+        "JugMock:vat=VatMock",
+        "NstJoinMock:vat=VatMock",
+        "NstJoinMock:nst=NstMock"
+    ],
+    "rule_sanity": "basic",
+    "solc": "solc-0.8.16",
+    "solc_optimize_map": {
+        "AllocatorVault": "200",
+        "AllocatorRoles": "200",
+        "VatMock": "0",
+        "JugMock": "0",
+        "NstJoinMock": "0",
+        "NstMock": "0"
+    },
+    "verify": "AllocatorVault:certora/AllocatorVault.spec",
+    "multi_assert_check": true,
+    "wait_for_results": "all"
+}
diff --git a/certora/funnels/DepositorUniV3.conf b/certora/funnels/DepositorUniV3.conf
new file mode 100644
index 00000000..e8aa2cdd
--- /dev/null
+++ b/certora/funnels/DepositorUniV3.conf
@@ -0,0 +1,25 @@
+{
+    "files": [
+        "src/funnels/DepositorUniV3.sol",
+        "src/AllocatorRoles.sol",
+        "test/mocks/PoolUniV3Mock.sol",
+        "test/mocks/Gem0Mock.sol",
+        "test/mocks/Gem1Mock.sol",
+        "certora/funnels/Auxiliar.sol"
+    ],
+    "link": [
+        "DepositorUniV3:roles=AllocatorRoles"
+    ],
+    "rule_sanity": "basic",
+    "solc": "solc-0.8.16",
+    "solc_optimize_map": {
+        "DepositorUniV3": "200",
+        "AllocatorRoles": "200",
+        "PoolUniV3Mock": "0",
+        "Gem0Mock": "0",
+        "Gem1Mock": "0",
+        "Auxiliar": "0"
+    },
+    "verify": "DepositorUniV3:certora/funnels/DepositorUniV3.spec",
+    "wait_for_results": "all"
+}
diff --git a/certora/funnels/Swapper.conf b/certora/funnels/Swapper.conf
new file mode 100644
index 00000000..9cadff2f
--- /dev/null
+++ b/certora/funnels/Swapper.conf
@@ -0,0 +1,23 @@
+{
+    "files": [
+        "src/funnels/Swapper.sol",
+        "src/AllocatorRoles.sol",
+        "test/mocks/Gem0Mock.sol",
+        "test/mocks/Gem1Mock.sol",
+        "test/mocks/CalleeMock.sol"
+    ],
+    "link": [
+        "Swapper:roles=AllocatorRoles"
+    ],
+    "rule_sanity": "basic",
+    "solc": "solc-0.8.16",
+    "solc_optimize_map": {
+        "Swapper": "200",
+        "AllocatorRoles": "200",
+        "Gem0Mock": "0",
+        "Gem1Mock": "0",
+        "CalleeMock": "0"
+    },
+    "verify": "Swapper:certora/funnels/Swapper.spec",
+    "wait_for_results": "all"
+}
diff --git a/certora/funnels/automation/ConduitMover.conf b/certora/funnels/automation/ConduitMover.conf
new file mode 100644
index 00000000..7456aece
--- /dev/null
+++ b/certora/funnels/automation/ConduitMover.conf
@@ -0,0 +1,10 @@
+{
+    "files": [
+        "src/funnels/automation/ConduitMover.sol"
+    ],
+    "rule_sanity": "basic",
+    "solc": "solc-0.8.16",
+    "solc_optimize": "200",
+    "verify": "ConduitMover:certora/funnels/automation/ConduitMover.spec",
+    "wait_for_results": "all"
+}
diff --git a/certora/funnels/automation/StableDepositorUniV3.conf b/certora/funnels/automation/StableDepositorUniV3.conf
new file mode 100644
index 00000000..0a60d833
--- /dev/null
+++ b/certora/funnels/automation/StableDepositorUniV3.conf
@@ -0,0 +1,10 @@
+{
+    "files": [
+        "src/funnels/automation/StableDepositorUniV3.sol",
+    ],
+    "rule_sanity": "basic",
+    "solc": "solc-0.8.16",
+    "solc_optimize": "200",
+    "verify": "StableDepositorUniV3:certora/funnels/automation/StableDepositorUniV3.spec",
+    "wait_for_results": "all"
+}
diff --git a/certora/funnels/automation/StableSwapper.conf b/certora/funnels/automation/StableSwapper.conf
new file mode 100644
index 00000000..6977f741
--- /dev/null
+++ b/certora/funnels/automation/StableSwapper.conf
@@ -0,0 +1,10 @@
+{
+    "files": [
+        "src/funnels/automation/StableSwapper.sol",
+    ],
+    "rule_sanity": "basic",
+    "solc": "solc-0.8.16",
+    "solc_optimize": "200",
+    "verify": "StableSwapper:certora/funnels/automation/StableSwapper.spec",
+    "wait_for_results": "all"
+}