source

cbor_ada

0.1.1

CBOR (RFC 8949) encoding/decoding library with SPARK formal verification

GitHub Community CIResults All crate versions Download JSON

0.1.1

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).

Authors: Baris Erdem
Maintainers: Baris Erdem <baris@erdem.dev>
Maintainer profiles: @b-erdem
Licenses: Apache-2.0
Website: https://github.com/b-erdem/cbor_ada
Repository: github.com/b-erdem/cbor_ada
Source revision: 4e578607a677
Tags: cbor, rfc8949, serialization, spark, embedded, iot, verified
Manifest: index/cb/cbor_ada/cbor_ada-0.1.1.toml