hello_world.adb

with Ada.Command_Line;
with Ada.Text_IO;

procedure Hello_World is
   You : constant String :=
--  Change to strict inequality below to prove
     (if Ada.Command_Line.Argument_Count >= 0 then
        Ada.Command_Line.Argument (1)
      else "世界");
begin
   Ada.Text_IO.Put ("Hello, ");
   Ada.Text_IO.Put_Line (You);
end Hello_World;

main.adc

pragma Profile(GNAT_Extended_Ravenscar);
pragma Partition_Elaboration_Policy(Sequential);
pragma SPARK_Mode (On);
pragma Warnings (Off, "no Global contract available");
pragma Warnings (Off, "subprogram * has no effect");

main.gpr

project Main is
   package Compiler is
      for Default_Switches ("Ada") use ("-gnatwa");
   end Compiler;

   package Prove is
      for Proof_Switches ("Ada") use ("--level=2", "-j0");
   end Prove;

   package Builder is
      for Global_Configuration_Pragmas use "main.adc";
   end Builder;
end Main;