diff --git a/src/filo-fs-ext2.adb b/src/filo-fs-ext2.adb
index 3276cdd..96328dd 100644
--- a/src/filo-fs-ext2.adb
+++ b/src/filo-fs-ext2.adb
@@ -71,7 +71,7 @@
             return;
          end if;
       end;
-      pragma Assert_And_Cut (Success);
+      pragma Assert_And_Cut (Success and not Is_Mounted (State));
 
       declare
          S_Inodes_Per_Group : constant Unsigned_32 := Read_LE32 (Super_Block, 10 * 4);
@@ -83,7 +83,6 @@
             return;
          end if;
       end;
-      pragma Assert_And_Cut (Success);
 
       declare
          S_Rev_Level : constant Unsigned_32 := Read_LE32 (Super_Block, 19 * 4);
@@ -107,7 +106,7 @@
          end if;
          Static.Inodes_Per_Block := Inode_In_Block_Count (Static.Block_Size / Static.Inode_Size);
       end;
-      pragma Assert_And_Cut (Success);
+      pragma Assert_And_Cut (Success and not Is_Mounted (State));
 
       declare
          S_Feature_Incompat : constant Unsigned_32 := Read_LE32 (Super_Block, 24 * 4);
@@ -135,7 +134,6 @@
          end if;
          Static.Group_Desc_Per_Block := Group_In_Block_Count (Static.Block_Size / Static.Group_Desc_Size);
       end;
-      pragma Assert_And_Cut (Success);
 
       State.S := Mounted;
    end Mount;
@@ -224,6 +222,8 @@
       Logical     : in     FSBlock_Logical;
       Physical    :    out FSBlock_Offset;
       Success     :    out Boolean)
+   with
+      Post => State.Static = State.Static'Old and State.S = State.S'Old
    is
       Static : constant Mount_State := State.Static;
 
@@ -254,7 +254,8 @@
       with
          Pre =>
             Addr_Per_Block = FSBlock_Logical (Static.Block_Size / 4) and
-            FSBlock_Logical (Addr_In_Block) < Addr_Per_Block
+            FSBlock_Logical (Addr_In_Block) < Addr_Per_Block,
+         Post => State.Static = State.Static'Old and State.S = State.S'Old
       is
          Cache_Start, Cache_End : Max_Block_Index;
       begin
@@ -361,6 +362,8 @@
       Logical     : in     FSBlock_Logical;
       Physical    :    out FSBlock_Offset;
       Success     :    out Boolean)
+   with
+      Post => State.Static = State.Static'Old and State.S = State.S'Old
    is
       Cache : Cache_Buffer renames State.Cache.Buffer;
 
@@ -495,7 +498,7 @@
             Logical_Off <= Logical and
             Dynamic_Max_Index = State.Static.Block_Size / Extent_Header_Size - 1,
          Post =>
-            State.Static = State.Static'Old and
+            State.Static = State.Static'Old and State.S = State.S'Old and
             (if Success then
                Next <= Dynamic_Max_Index and then
                Cache_End = Cache_Start + State.Static.Block_Size - 1 and then
@@ -570,6 +573,7 @@
          loop
             pragma Loop_Invariant
               (State.Static = State.Static'Loop_Entry and then
+               State.S = State.S'Loop_Entry and then
                Depth > 0 and then
                Depth in Extent_Depth and then
                Logical_Off <= Logical);
@@ -692,7 +696,7 @@
       Success  : out Boolean)
    with
       Pre => Is_Mounted (State),
-      Post => Success = Is_Open (State)
+      Post => Is_Mounted (State) and (Success = Is_Open (State))
    is
       Static : Mount_State renames State.Static;
       Cache : Cache_Buffer renames State.Cache.Buffer;
@@ -926,7 +930,7 @@
       Static : Mount_State renames State.Static;
       Cache : Cache_Buffer renames State.Cache.Buffer;
 
-      Pos : Natural;
+      Pos : Natural range Buf'First .. Buf'Last + 1;
    begin
       if State.Inode.Mode = Fast_Link then
          if State.Inode.Size > Inode_Length (State.Inode.Inline'Length) or
@@ -944,22 +948,30 @@
 
       Len := 0;
       Pos := Buf'First;
-      while Pos <= Buf'Last and Inode_Length (File_Pos) < State.Inode.Size loop
+      while Pos <= Buf'Last and
+            File_Pos < File_Offset'Last and
+            Inode_Length (File_Pos) < State.Inode.Size
+      loop
+         pragma Loop_Invariant (Is_Open (State));
          declare
             In_Block : constant Max_Block_Index := Natural (File_Pos) mod Static.Block_Size;
-            Logical : constant FSBlock_Logical := FSBlock_Logical (File_Pos / File_Offset (Static.Block_Size));
-            In_Block_Space : constant Natural := Natural (Static.Block_Size) - In_Block;
+            Logical : constant FSBlock_Logical :=
+               FSBlock_Logical (File_Pos / File_Offset (Static.Block_Size));
+            In_Block_Space : constant Positive := Static.Block_Size - In_Block;
             In_File_Space : constant Inode_Length := State.Inode.Size - Inode_Length (File_Pos);
-            In_Buf_Space : constant Natural := Buf'Last - Pos + 1;
-            Len_Here : Natural;
+            In_Buf_Space : constant Positive := Buf'Last - Pos + 1;
+            Len_Here : Positive;
          begin
             Len_Here := In_Block_Space;
             if In_File_Space < Inode_Length (Len_Here) then
-               Len_Here := Natural (In_File_Space);
+               Len_Here := Positive (In_File_Space);
             end if;
             if In_Buf_Space < Len_Here then
                Len_Here := In_Buf_Space;
             end if;
+            if File_Offset'Last - File_Pos < File_Length (Len_Here) then
+               Len_Here := Positive (File_Offset'Last - File_Pos);
+            end if;
 
             declare
                Last : constant Index_Type := Pos + Len_Here - 1;
@@ -972,23 +984,24 @@
                else
                   Ext2_Block_Map (State, Logical, Physical, Success);
                end if;
-               if Success then
-                  Cache_FSBlock
-                    (Static      => Static,
-                     Cache       => State.Cache,
-                     Phys        => Physical,
-                     Level       => Block_Cache_Index'Last,
-                     Cache_Start => Cache_Start,
-                     Cache_End   => Cache_End,
-                     Success     => Success);
-               end if;
+               exit when not Success;
+
+               Cache_FSBlock
+                 (Static      => Static,
+                  Cache       => State.Cache,
+                  Phys        => Physical,
+                  Level       => Block_Cache_Index'Last,
+                  Cache_Start => Cache_Start,
+                  Cache_End   => Cache_End,
+                  Success     => Success);
+               pragma Assert (Cache_Start <= Cache_End - (In_Block + Len_Here - 1));
                exit when not Success;
 
                Buf (Pos .. Last) := Cache (
                   Cache_Start + In_Block .. Cache_Start + In_Block + Len_Here - 1);
                File_Pos := File_Pos + File_Length (Len_Here);
                Pos := Pos + Len_Here;
-               Len := Len + Len_Here;
+               Len := Pos - Buf'First;
             end;
          end;
       end loop;
diff --git a/src/filo-fs-ext2.ads b/src/filo-fs-ext2.ads
index c48ee93..1757da8 100644
--- a/src/filo-fs-ext2.ads
+++ b/src/filo-fs-ext2.ads
@@ -24,7 +24,7 @@
       Success     : out    Boolean)
    with
       Pre => Is_Mounted (State),
-      Post => Success = Is_Open (State);
+      Post => (if Success then Is_Open (State) else Is_Mounted (State));
 
    procedure Close (State : in out T)
    with
@@ -37,7 +37,7 @@
       Buf      :    out Buffer_Type;
       Len      :    out Natural)
    with
-      Pre => Is_Open (State),
+      Pre => Is_Open (State) and Buf'Length > 0,
       Post => Is_Open (State);
 
 private
diff --git a/src/filo-fs-vfs.adb b/src/filo-fs-vfs.adb
index a43edf6..02e4c52 100644
--- a/src/filo-fs-vfs.adb
+++ b/src/filo-fs-vfs.adb
@@ -107,7 +107,7 @@
         (Path        : in out Path_String;
          Rest_First  : in     Path_Index_Plus;
          Rest_Last   : in     Path_Index;
-         Link_Len    : in     Natural;
+         Link_Len    : in     Positive;
          Success     :    out Boolean)
       with
          Pre =>
@@ -127,11 +127,15 @@
             return;
          end if;
 
+         pragma Warnings
+           (GNATprove, Off, """File_Pos"" is set*but not used",
+            Reason => "We only read the link at once, during path walks.");
          Read
            (State    => State,
             File_Pos => File_Pos,
             Buf      => Path_Buf (1 .. Link_Len),
             Len      => Read_Len);
+         pragma Warnings (GNATprove, On, """File_Pos"" is set*but not used");
          Success := Read_Len = Link_Len;
 
          if Success then
@@ -209,14 +213,14 @@
                            return;
                         end if;
                      when Link =>
-                        if File_Len > Path_Max then
+                        if File_Len = 0 or File_Len > Path_Max then
                            Success := False;
                         else
                            Read_Link
                              (Path        => Path,
                               Rest_First  => Comp_Last + 1,
                               Rest_Last   => Path_Last,
-                              Link_Len    => Natural (File_Len),
+                              Link_Len    => Positive (File_Len),
                               Success     => Success);
                         end if;
                         Close (State);