diff --git a/src/filo-fs-ext2.adb b/src/filo-fs-ext2.adb
index 3cdeca5..4dcde30 100644
--- a/src/filo-fs-ext2.adb
+++ b/src/filo-fs-ext2.adb
@@ -377,6 +377,7 @@
       subtype Extent_Off is Natural range 0 .. Extent_Header_Size;
       subtype Extent_Idx is Natural range 1 .. (Max_Block_Index'Last + 1) / Extent_Header_Size - 1;
       Dynamic_Max_Index : constant Extent_Idx := State.Block_Size / Extent_Header_Size - 1;
+      subtype Extent_Depth is Natural range 0 .. 32;
 
       function Extent_Byte_Offset (Idx : Extent_Idx; Off : Extent_Off) return Natural
       is
@@ -466,7 +467,7 @@
       procedure Next_Ref
         (Current     : in     FSBlock_Offset;
          Logical_Off : in     FSBlock_Logical;
-         Depth       : in     Natural;
+         Depth       : in     Extent_Depth;
          Next        :    out Extent_Idx;
          Cache_Start :    out Max_Block_Index;
          Cache_End   :    out Max_Block_Index;
@@ -474,6 +475,7 @@
       with
          Pre => Logical_Off <= Logical,
          Post => (if Success then
+                     Next <= Dynamic_Max_Index and then
                      Cache_End = Cache_Start + State.Block_Size - 1 and then
                      Extent_Logical (State.Block_Cache (Cache_Start .. Cache_End), Next) <= Logical)
       is
@@ -504,6 +506,7 @@
             Success := Success and then
                Hdr_Magic = Extent_Header_Magic and then
                Hdr_Depth = Depth and then
+               Hdr_Entries in Extent_Idx and then
                Hdr_Entries <= Dynamic_Max_Index and then
                First_Logical = Logical_Off;
             if not Success then
@@ -528,7 +531,8 @@
          Inode_Magic = Extent_Header_Magic and then
          Inode_Entries > 0 and then
          Inode_Entries < Inline_Extents'Length / Extent_Header_Size and then
-         First_Logical <= Logical;
+         First_Logical <= Logical and then
+         Depth in Extent_Depth;
       if not Success then
          Physical := 0;
          return;
@@ -543,6 +547,10 @@
          Physical := Index_Physical (Inline_Extents, Idx);
          Logical_Off := Index_Logical (Inline_Extents, Idx);
          loop
+            pragma Loop_Invariant
+              (Depth > 0 and then
+               Depth in Extent_Depth and then
+               Logical_Off <= Logical);
             Depth := Depth - 1;
             Next_Ref
               (Current     => Physical,