SPARK-proved CBOR encoder/decoder for Ada 2022. The entire library is formally verified at SPARK Level 2: 1082/1082 proof obligations discharged, 0 unproved, 0 pragma Assume. Beyond absence of run-time errors, the encode/decode round trip is machine-proved – Decode (Encode (x)) = x for every major-type head (integers, tags, array/map headers, simple values, booleans, null/undefined) and byte-exact float payload pass-through – via a shared ghost denotation of the wire format.

No heap allocation, pragma Pure, suitable for embedded and safety-critical systems. Full RFC 8949 well-formedness validation including shortest-form checking, configurable nesting depth, string length limits, and optional UTF-8 validation.