diff --git a/common/hw-gfx-framebuffer_filler.adb b/common/hw-gfx-framebuffer_filler.adb
index 250d903..29c7da6 100644
--- a/common/hw-gfx-framebuffer_filler.adb
+++ b/common/hw-gfx-framebuffer_filler.adb
@@ -17,6 +17,8 @@
 pragma Elaborate_All (HW.MMIO_Range);
 
 package body HW.GFX.Framebuffer_Filler
+with
+   Refined_State => (State => FB.State, Base_Address => FB.Base_Address)
 is
 
    type FB_Index is new Natural range
diff --git a/common/hw-gfx-framebuffer_filler.ads b/common/hw-gfx-framebuffer_filler.ads
index 228d43a..7ad3b79 100644
--- a/common/hw-gfx-framebuffer_filler.ads
+++ b/common/hw-gfx-framebuffer_filler.ads
@@ -19,6 +19,9 @@
 use type HW.Int32;
 
 package HW.GFX.Framebuffer_Filler
+with
+   Abstract_State => ((State with External), Base_Address),
+   Initializes => Base_Address
 is
 
    procedure Fill (Linear_FB : Word64; Framebuffer : Framebuffer_Type)
diff --git a/common/hw-gfx-gma.adb b/common/hw-gfx-gma.adb
index f135a5e..a443132 100644
--- a/common/hw-gfx-gma.adb
+++ b/common/hw-gfx-gma.adb
@@ -18,8 +18,6 @@
 with HW.PCI.Dev;
 pragma Elaborate_All (HW.PCI.Dev);
 
-with HW.GFX.Framebuffer_Filler;
-
 with HW.GFX.GMA.Config;
 with HW.GFX.GMA.Config_Helpers;
 with HW.GFX.GMA.Registers;
@@ -527,7 +525,15 @@
 
    ----------------------------------------------------------------------------
 
+   pragma Warnings
+     (GNATprove, Off, """Registers.Register_State"" * is not modified*",
+      Reason => "Power_Up_VGA is only effective on certain generations.");
    procedure Power_Up_VGA
+   with
+      Refined_Global =>
+        (Input => (Cur_Configs, Time.State),
+         In_Out => (Registers.Register_State),
+         Proof_In => (Initialized))
    is
       Fake_Config : constant Pipe_Configs :=
         (Primary =>
@@ -543,6 +549,14 @@
    begin
       Power_And_Clocks.Power_Up (Cur_Configs, Fake_Config);
    end Power_Up_VGA;
+   pragma Warnings
+     (GNATprove, Off, "no check message justified*", Reason => "see below");
+   pragma Annotate
+     (GNATprove, Intentional, "unused global",
+      "Power_Up_VGA is only effective on certain generations.");
+   pragma Warnings (GNATprove, On, "no check message justified*");
+   pragma Warnings
+     (GNATprove, On, """Registers.Register_State"" * is not modified*");
 
    ----------------------------------------------------------------------------
 
diff --git a/common/hw-gfx-gma.ads b/common/hw-gfx-gma.ads
index 1f81ece..7f44a0f 100644
--- a/common/hw-gfx-gma.ads
+++ b/common/hw-gfx-gma.ads
@@ -16,6 +16,7 @@
 with HW.Config;
 with HW.Time;
 with HW.Port_IO;
+with HW.GFX.Framebuffer_Filler;
 
 package HW.GFX.GMA
 with
@@ -107,44 +108,86 @@
       Global => (Input => Init_State);
    pragma Warnings (GNATprove, On, "unused variable ""Write_Delay""");
 
-   pragma Warnings (GNATprove, Off, "subprogram ""Power_Up_VGA"" has no effect",
-                    Reason => "Effect depends on the platform compiled for");
    procedure Power_Up_VGA
    with
+      Global =>
+        (Input => (State, Time.State),
+         In_Out => (Device_State),
+         Proof_In => (Init_State)),
       Pre => Is_Initialized;
 
-   procedure Update_Outputs (Configs : Pipe_Configs);
+   ----------------------------------------------------------------------------
 
-   procedure Update_Cursor (Pipe : Pipe_Index; Cursor : Cursor_Type);
+   procedure Update_Outputs (Configs : Pipe_Configs)
+   with
+      Global =>
+        (Input => (Config_State, Time.State),
+         In_Out => (State, Device_State, Port_IO.State),
+         Proof_In => (Init_State)),
+      Pre => Is_Initialized;
+
+   procedure Update_Cursor (Pipe : Pipe_Index; Cursor : Cursor_Type)
+   with
+      Global =>
+        (In_Out => (State, Device_State),
+         Proof_In => (Init_State)),
+      Pre => Is_Initialized;
+
    procedure Place_Cursor
      (Pipe : Pipe_Index;
       X : Cursor_Pos;
-      Y : Cursor_Pos);
+      Y : Cursor_Pos)
+   with
+      Global =>
+        (In_Out => (State, Device_State),
+         Proof_In => (Init_State)),
+      Pre => Is_Initialized;
+
    procedure Move_Cursor
      (Pipe : Pipe_Index;
       X : Cursor_Pos;
-      Y : Cursor_Pos);
+      Y : Cursor_Pos)
+   with
+      Global =>
+        (In_Out => (State, Device_State),
+         Proof_In => (Init_State)),
+      Pre => Is_Initialized;
 
-   pragma Warnings (GNATprove, Off, "subprogram ""Dump_Configs"" has no effect",
-                    Reason => "It's only used for debugging");
-   procedure Dump_Configs (Configs : Pipe_Configs);
+   ----------------------------------------------------------------------------
 
    procedure Write_GTT
      (GTT_Page       : GTT_Range;
       Device_Address : GTT_Address_Type;
-      Valid          : Boolean);
+      Valid          : Boolean)
+   with
+      Global => (In_Out => Device_State, Proof_In => Init_State),
+      Pre => Is_Initialized;
 
    procedure Setup_Default_FB
      (FB       : in     Framebuffer_Type;
       Clear    : in     Boolean := True;
       Success  :    out Boolean)
    with
+      Global =>
+        (In_Out =>
+           (State, Device_State,
+            Framebuffer_Filler.State, Framebuffer_Filler.Base_Address),
+         Proof_In => (Init_State)),
       Pre => Is_Initialized and HW.Config.Dynamic_MMIO;
 
    procedure Map_Linear_FB (Linear_FB : out Word64; FB : in Framebuffer_Type)
    with
+      Global =>
+        (In_Out => (State, Device_State),
+         Proof_In => (Init_State)),
       Pre => Is_Initialized and HW.Config.Dynamic_MMIO;
 
+   ----------------------------------------------------------------------------
+
+   pragma Warnings (GNATprove, Off, "subprogram ""Dump_Configs"" has no effect",
+                    Reason => "It's only used for debugging");
+   procedure Dump_Configs (Configs : Pipe_Configs);
+
 private
 
    -- For the default framebuffer setup (see below) with 90 degree rotations,