This is the smoking gun for me:

    procedure Overflow_This_Buffer
       with SPARK_Mode => On
    is
       type Integer_Array is array (Positive range <>) of Integer;
       Int_Array : Integer_Array (1 .. 10) := [others => 1];
       Index_To_Clear : Integer;
    begin
       Ada.Text_IO.Put ("What array index should be cleared? ");
       --  Read the new array size from stdin.
       Ada.Integer_Text_IO.Get (Index_To_Clear);

       Int_Array (Index_To_Clear) := 0;
    end Overflow_This_Buffer;

What I am asking is what exactly is formally proving from 1st principles? Because to me this looks no different than a simple assertion statement or runtime bounds check which can be performed in any language with if statements & exceptions.

How did you prove that no one could just put in an arbitrary integer into that function? Does it fail to compile? Then you're just making a custom type which enforces valid state which, again can be done in any language with a rich type system and if statements.

If I might be more blunt: formal proofs in the field of programming appear to be nothing more than mathematicians trying to strong-arm their way into the industry where they aren't necessarily needed. Formal proofs make sense when you're trying to come up with new formulas or studying the cosmos, but they make no sense when you're trying to predict how bits will behave on a computer, because for the most part that is a solved problem by languages themselves.