Подтип строки, содержащей только шестнадцатеричные символы в Ada

Вы можете добавить динамический предикат и использовать динамическую семантику теста членства. Из RM 4.5.2 (29/4) :

Индивидуальный тест на членство дает результат «Истина», если:

• [...]
• Выбор членства — это метка_подтипа, тестируемый тип — скаляр, значение протестированного_простого_выражения принадлежит диапазону именованного подтипа, и это значение удовлетворяет предикатам именованного подтипа.

Например:

main.adb

procedure Main with SPARK_Mode is

   subtype Hex_Character is Character
     with Static_Predicate => Hex_Character in 
       'A' .. 'F' | 'a' .. 'f' | '0' .. '9';
      
   subtype Hex_String is String
     with Dynamic_Predicate =>
       (for all Char of Hex_String => Char in Hex_Character);
   
   S1 : Hex_String := "ABCDEF1234567890";       -- Line 11
   S2 : Hex_String := "Foo";                    -- Line 12
   
begin
   null;
end Main;

выход (GNATprove)

$ gnatprove -Pdefault.gpr -u main.adb --level=1 --report=all
Phase 1 of 3: generation of data representation information ...
Phase 2 of 3: generation of Global contracts ...
Phase 3 of 3: flow analysis and proof ...
main.adb:11:23: info: predicate check proved

main.adb:12:23: medium: predicate check might fail, cannot prove Char in Hex_Character
   12 |   S2 : Hex_String := "Foo";
      |                      ^~~~~
  in inlined predicate at main.adb:9
Summary logged in ./obj/gnatprove/gnatprove.out

Другой вариант — использовать частный тип:

Package Hexes is
   Subtype Upper_Hex is Character range 'A'..'F';
   Subtype Lower_Hex is Character range 'a'..'f';
   Subtype Digit_Hex is Character range '0'..'9';
   Subtype Hex_Character is Character
      with Static_Predicate => Hex_Character in Digit_Hex | Upper_Hex | Lower_Hex;

   Type Hex_String(<>) is private;
   Function "+"( Object : String     ) return Hex_String
     with Pre => (for all C in Object => C in Hex_Character);
   Function "+"( Object : Hex_String ) return String;
Private
   Type Hex_String is new String
     with Dynamic_Predicate => 
             (for all C in Hex_String => C in Hex_Character),
          Predicate_Failure => raise Constraint_Error with 
             "Invalid Hex-string: '" & String( Hex_String ) & "'.";
   Function "+"( Object : String     ) return Hex_String is
     ( Hex_String( Object ) );
   Function "+"( Object : Hex_String ) return String is
     ( String( Object ) );
End Hexes;

Вышеупомянутая конструкция вынуждает использовать функцию построения (перегруженный унарный плюс), если вам нужна эта устойчивость перед политикой утверждений off, затем переместите функцию построения в BODY и вручную поднимите Constraint_Error оттуда при обнаружении недействительного символы (через for all).