diff --git a/certora/certora.conf b/certora/certora.conf
index 72883d7..a7ca19c 100644
--- a/certora/certora.conf
+++ b/certora/certora.conf
@@ -1,8 +1,8 @@
 {
-  "files": ["src/Foo.sol"],
-  "msg": "Verifying Foo.sol",
+  "files": ["src/Rln.sol"],
+  "msg": "Verifying Rln.sol",
   "rule_sanity": "basic",
-  "verify": "Foo:certora/specs/Foo.spec",
+  "verify": "Rln:certora/specs/Rln.spec",
   "wait_for_results": "all",
 }
 
diff --git a/certora/specs/Foo.spec b/certora/specs/Foo.spec
deleted file mode 100644
index ed4bc13..0000000
--- a/certora/specs/Foo.spec
+++ /dev/null
@@ -1,9 +0,0 @@
-methods {
-  function id(uint256) external returns (uint256) envfree;
-}
-
-rule checkIdOutputIsAlwaysEqualToInput {
-  uint256 input;
-
-  assert id(input) == input;
-}
diff --git a/certora/specs/Rln.spec b/certora/specs/Rln.spec
new file mode 100644
index 0000000..5e7aa6d
--- /dev/null
+++ b/certora/specs/Rln.spec
@@ -0,0 +1,9 @@
+methods {
+  function root() external returns (uint256) envfree;
+}
+
+rule checkDefaultRootIsCorrect {
+  uint256 defaultRoot = 15019797232609675441998260052101280400536945603062888308240081994073687793470;
+
+  assert root() == input;
+}