hmac_ada

SPARK-proved HMAC (RFC 2104) with standalone SHA-256 (FIPS 180-4) for Ada 2022. 174 proof obligations fully discharged at Level 2 with zero pragma Assume. Constant-time digest comparison, secure wipe of key material, no heap allocation, pragma Pure. Suitable for embedded and safety-critical systems. Includes streaming and one-shot APIs, plus a generic HMAC package for other hash functions.