diff --git a/cedar-lean/Cedar/Spec/Ext/IPAddr.lean b/cedar-lean/Cedar/Spec/Ext/IPAddr.lean
index 873c2bb18..61e18fcbf 100644
--- a/cedar-lean/Cedar/Spec/Ext/IPAddr.lean
+++ b/cedar-lean/Cedar/Spec/Ext/IPAddr.lean
@@ -148,7 +148,7 @@ def IPNet.isMulticast (ip : IPNet) : Bool :=
 
 def parseCIDR (str : String) (digits : Nat) (size : Nat) : Option (Fin (size + 1)) :=
   let len := str.length
-  if 0 < len && len ≤ digits
+  if 0 < len && len ≤ digits && (str.startsWith "0" → str = "0")
   then do
     let n ← str.toNat?
     if n ≤ size then .some (Fin.ofNat n) else .none
diff --git a/cedar-lean/UnitTest/IPAddr.lean b/cedar-lean/UnitTest/IPAddr.lean
index 8a747e160..e4697a3b1 100644
--- a/cedar-lean/UnitTest/IPAddr.lean
+++ b/cedar-lean/UnitTest/IPAddr.lean
@@ -64,7 +64,12 @@ def testsForInvalidStrings :=
     testInvalid "F:A" "too few groups",
     testInvalid "::ffff1" "group out of range",
     testInvalid "F:AE::F:5:F:F:0/129" "prefix out of range",
-    testInvalid "::ffff:127.0.0.1" "no IPv4 embedded in IPv6"
+    testInvalid "::ffff:127.0.0.1" "no IPv4 embedded in IPv6",
+    testInvalid "::/00" "no leading zeros",
+    testInvalid "::/01" "no leading zeros",
+    testInvalid "::/001" "no leading zeros",
+    testInvalid "127.0.0.1/01" "no leading zeros",
+    testInvalid "F:AE::F:5:F:F:0/01" "no leading zeros"
   ]
 
 deriving instance Inhabited for IPNet
@@ -163,4 +168,4 @@ def tests := [
 -- Uncomment for interactive debugging
 -- #eval TestSuite.runAll tests
 
-end UnitTest.IPAddr
\ No newline at end of file
+end UnitTest.IPAddr