What we have proved

Ten properties a user of zlib relies on: compression and decompression are deterministic, decompression does not consume what follows the stream, a round trip gives back exactly the data, too little output space gives Z_BUF_ERROR and the start of the data, the compressed size and the memory of both directions stay within stated bounds, and decompression is memory-safe on any input. The gz* file API and infback.c are not covered.

Forty-five short specs and 17 longer ones from the first proof. crc32 is proved for its byte-at-a-time loop, not the braided loop of a default x86-64 build.

Nineteen short specs: the handshake’s keys agree and its secrets are erased, stale, replayed and failed messages change nothing, the replay window accepts each nonce once, and the AEADs give back what they encrypted.

Nineteen longer specs from the first proof: the handshake in noise.c and cookie.c does what a model of WireGuard’s handshake does, from any state; receive.c’s handshake checks let only messages of the exact type and length through; BLAKE2s, Poly1305 and the two ChaCha20-Poly1305 AEADs compute what reference implementations of RFC 7693, RFC 8439 and the XChaCha draft compute. Four of them put these pieces together the way the data path does, and that glue is assumed or copied, not verified.

crypto/punycode.c, the code of CVE-2022-3602 and CVE-2022-3786. Both functions accept any input and give only documented results, decoding follows RFC 3492, the reported sizes are exact, and OpenSSL decodes what an RFC 3492 encoder writes for any sequence of up to 3855 Unicode code points.

Twenty-five short specs: on any bytes the decoder stays within its buffers, frames of Raw and RLE blocks decode to exactly their content, invalid and truncated frames are refused, and the memory held stays within zstd’s own estimates. Nineteen longer specs draw compliant frames, compressed blocks and dictionaries included, within stated bounds.