SPARK-proved HKDF (RFC 5869) for Ada 2022, built on hmac_ada. The HKDF-SHA-256 instantiation is fully proved at SPARK Level 2 (266 checks, zero pragma Assume). Uses System.Storage_Elements.Storage_Array for embedded and constrained-runtime (Light, ZFP) compatibility, no heap allocation, pragma Pure. A separate generic HKDF package provides an unproved convenience layer for other HMAC functions.