SPARK-proved CBOR encoder/decoder for Ada 2022. The encoder and decoder are 100% formally verified at SPARK Level 2 (517 proof obligations, 0 unproved). 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 UTF-8 validation (enabled by default).