Upload Code
Package Summary Specifications Assumptions Verification Results Our open standard Verify it yourself Install Docker Docker image

Formal Verification Certificate

lean-zip — certified snapshot

This software package satisfies these specifications with these assumptions (see below). Specifically, everything shown with green text or background is auto-certified by VeriLib (and you can trivially re-verify it yourself), while what's shown with white background are unverified claims by the project team, included for pedagogy.

Certification date April 17, 2026
Package commit 78e5bd6
Functions Verified 773/773
Ethereum Proof Etherscan
Package Summary
GitHub VeriLib

lean-zip is a Lean 4 library that provides compression and archive support for zlib (RFC 1950), gzip (RFC 1952), raw DEFLATE (RFC 1951), tar, and ZIP formats. It offers two implementation paths:

  • C FFI path: High-performance wrappers around the system zlib library for production use.
  • Pure Lean native path: Implementations written entirely in Lean 4, with formal correctness proofs verified by Lean's type-checking kernel.

The formal verification effort covers the pure Lean native implementations in Zip/Native/ and their specifications in Zip/Spec/. The library proves roundtrip correctness — that compressing and then decompressing data returns the original input — for the DEFLATE, gzip, and zlib formats across all compression levels (0–9).

lean-zip was autoformalized from zlib (a C compression library) to Lean by a general-purpose AI, with no special training for theorem proving. If lean-zip is a faithful translation of zlib, then this verification of lean-zip would imply the correctness of zlib.

Main Specification/s

# Property/Area Description File Theorem
1 DEFLATE Roundtrip Unified roundtrip for all compression levels 0–9: inflate (deflateRaw data level) = .ok data Zip/Spec/DeflateRoundtrip.lean inflate_deflateRaw
2 Gzip Roundtrip Gzip format roundtrip with CRC-32 verification (RFC 1952) Zip/Spec/GzipCorrect.lean gzip_decompressSingle_compress
3 Zlib Roundtrip Zlib format roundtrip with Adler-32 verification (RFC 1950) Zip/Spec/ZlibCorrect.lean zlib_decompressSingle_compress
4 Decoder Correctness Native inflate agrees with formal bitstream specification Zip/Spec/InflateCorrect.lean inflate_correct
5 Decoder Completeness All spec-valid inputs are accepted by the decoder Zip/Spec/InflateComplete.lean inflateLoop_complete
6 Huffman Prefix-Free Canonical Huffman codes are prefix-free Zip/Spec/HuffmanTheorems.lean canonical_prefix_free
7 LZ77 Greedy Correctness Greedy LZ77 matcher produces valid decomposition Zip/Spec/LZ77NativeCorrect.lean lz77Greedy_resolves
8 LZ77 Lazy Correctness Lazy LZ77 matcher produces valid decomposition Zip/Spec/LZ77NativeCorrect.lean lz77Lazy_resolves
Specifications

An easier way to view the specifications is to click on the corresponding functions in VeriLib.

Assumptions
Lean Verifier

We assume that the Lean kernel is sound, and that the Lean verification system correctly implements its verification logic based on sound reasoning principles.

Hardware

As with any software, we trust that the hardware correctly executes the compiled machine code.

C FFI and System Libraries

The zlib C library, C compiler (cc), and pkg-config are required for the unverified FFI path only. These system dependencies are trusted without formal proof.

Dependencies

Lean's standard axioms (propext, Quot.sound, Classical.choice; no custom axioms). lean-zip-common (Git @ 87480b0): shared utilities checked by the kernel.

Unverified Functionality

Only the pure Lean native path (Zip/Native/) is formally verified. The C FFI path (wrapping system zlib), tar/ZIP archive support, and streaming APIs are tested for conformance but not formally proven.

Reference Specifications

RFC 1950 (Zlib), RFC 1951 (DEFLATE), RFC 1952 (GZIP), ISO 3309 / ITU-T V.42 (CRC-32).

Verification Results

Below are the formal verification results. Please check if the first test line says "VerificationSuccess": true.

Manifest
{
  "VerificationSuccess": true,
  "branch": "master",
  "build_arg_commit": "78e5bd6950afdda3ab88dbd567e54bc6adedf3ae",
  "cert_readme_badge_alt": "VeriLib Certified",
  "cert_readme_badge_image_url": "https://verilib.org/assets/img/verilib-certified-badge-wide.svg",
  "cert_readme_page_url": "https://verilib.org/cert/5165",
  "commit": "78e5bd6950afdda3ab88dbd567e54bc6adedf3ae",
  "commit_date_utc": null,
  "image": "verilib/probe-lean-repo-5165:1",
  "image_build_date_utc": "2026-04-17T10:40:37Z",
  "probe_extract_completed_at_utc": "2026-04-17T10:40:37Z",
  "probe_lean_version": "0.6.2",
  "repo": "https://github.com/kim-em/lean-zip.git",
  "source_tree_sha256": "ce1e5ee20b158cb8ac9809e2a06bb34939d0ae3891d92853bab4cda2098986ee",
  "to_be_verified": 773,
  "unified_extract_json_path": "probe_extract.json",
  "unified_extract_json_sha256": "8ca0933ce3961c6e3c6fc2dd2709c79561c21b84228e2e2081ba81f152ee4068",
  "verification_source": "unified_extract_json",
  "verified_functions": [
    "probe:Adler32.Native.adler32",
    "probe:Adler32.Native.updateBytes",
    "probe:Adler32.Native.updateBytes_eq_updateList",
    "probe:Adler32.Native.updateBytes_valid",
    "probe:Adler32.Spec.MOD_ADLER",
    "probe:Adler32.Spec.State",
    "probe:Adler32.Spec.Valid",
    "probe:Adler32.Spec.checksum",
    "probe:Adler32.Spec.init",
    "probe:Adler32.Spec.init_valid",
    "probe:Adler32.Spec.pack",
    "probe:Adler32.Spec.unpack",
    "probe:Adler32.Spec.updateByte",
    "probe:Adler32.Spec.updateByte_fst_lt",
    "probe:Adler32.Spec.updateByte_snd_lt",
    "probe:Adler32.Spec.updateByte_valid",
    "probe:Adler32.Spec.updateList",
    "probe:Adler32.Spec.updateList_append",
    "probe:Adler32.Spec.updateList_cons",
    "probe:Adler32.Spec.updateList_nil",
    "probe:Adler32.Spec.updateList_valid",
    "probe:Archive.Entry",
    "probe:Archive.Entry.compressedSize",
    "probe:Archive.Entry.crc32",
    "probe:Archive.Entry.localOffset",
    "probe:Archive.Entry.method",
    "probe:Archive.Entry.path",
    "probe:Archive.Entry.uncompressedSize",
    "probe:Archive.create",
    "probe:Archive.createFromDir",
    "probe:Archive.extract",
    "probe:Archive.extractFile",
    "probe:Archive.instInhabitedEntry",
    "probe:Archive.instInhabitedEntry.default",
    "probe:Archive.instReprEntry",
    "probe:Archive.instReprEntry.repr",
    "probe:Archive.list",
    "probe:Archive.readExactStream",
    "probe:ByteArray.beq",
    "probe:Checksum.adler32",
    "probe:Checksum.crc32",
    "probe:Crc32.Native.crc32",
    "probe:Crc32.Native.crcBit_xor_high",
    "probe:Crc32.Native.crcByteTable_eq_crcByte",
    "probe:Crc32.Native.table",
    "probe:Crc32.Native.table_size",
    "probe:Crc32.Native.updateBytes",
    "probe:Crc32.Native.updateBytes_eq_updateList",
    "probe:Crc32.Spec.POLY",
    "probe:Crc32.Spec.checksum",
    "probe:Crc32.Spec.crcBit",
    "probe:Crc32.Spec.crcByte",
    "probe:Crc32.Spec.crcByteTable",
    "probe:Crc32.Spec.mkTable",
    "probe:Crc32.Spec.updateList",
    "probe:Crc32.Spec.updateList_append",
    "probe:Crc32.Spec.updateList_nil",
    "probe:Deflate.Correctness.Deflate.Correctness.fixedDistLengths_eq",
    "probe:Deflate.Correctness.Deflate.Correctness.fixedDistLengths_size",
    "probe:Deflate.Correctness.Deflate.Correctness.fixedLitLengths_eq",
    "probe:Deflate.Correctness.Deflate.Correctness.fixedLitLengths_size",
    "probe:Deflate.Correctness.NoLeafOnPath",
    "probe:Deflate.Correctness.TreeHasLeaf",
    "probe:Deflate.Correctness.acc_or_shift_bound",
    "probe:Deflate.Correctness.acc_or_shift_toNat",
    "probe:Deflate.Correctness.alignToByte_data",
    "probe:Deflate.Correctness.alignToByte_id_of_aligned",
    "probe:Deflate.Correctness.alignToByte_toBits",
    "probe:Deflate.Correctness.alignToByte_wf",
    "probe:Deflate.Correctness.bfinal_beq_nat_false",
    "probe:Deflate.Correctness.bfinal_beq_nat_true",
    "probe:Deflate.Correctness.bytesToBits_bitsToBytes_aligned",
    "probe:Deflate.Correctness.bytesToBits_bitsToBytes_take",
    "probe:Deflate.Correctness.bytesToBits_drop_testBit",
    "probe:Deflate.Correctness.canonicalCodes_correct_pos",
    "probe:Deflate.Correctness.canonicalCodes_correct_zero",
    "probe:Deflate.Correctness.canonicalCodes_go_size",
    "probe:Deflate.Correctness.canonicalCodes_hasLeaf",
    "probe:Deflate.Correctness.codeFor_some",
    "probe:Deflate.Correctness.copyLoop_eq_ofFn",
    "probe:Deflate.Correctness.count_foldl_take_le",
    "probe:Deflate.Correctness.decodeBits",
    "probe:Deflate.Correctness.decodeBits_of_hasLeaf",
    "probe:Deflate.Correctness.decodeCLSymbols_complete",
    "probe:Deflate.Correctness.decodeCLSymbols_inv",
    "probe:Deflate.Correctness.decodeDynamicTables_rest_le",
    "probe:Deflate.Correctness.decodeDynamicTrees_complete",
    "probe:Deflate.Correctness.decodeDynamicTrees_correct",
    "probe:Deflate.Correctness.decodeHuffman_complete",
    "probe:Deflate.Correctness.decodeHuffman_correct",
    "probe:Deflate.Correctness.decodeStored_complete",
    "probe:Deflate.Correctness.decodeStored_correct",
    "probe:Deflate.Correctness.decodeStored_invariants",
    "probe:Deflate.Correctness.decodeStored_rest_le",
    "probe:Deflate.Correctness.decodeSymbols_rest_le",
    "probe:Deflate.Correctness.decode_go_complete",
    "probe:Deflate.Correctness.decode_go_decodeBits",
    "probe:Deflate.Correctness.decode_pos_inv",
    "probe:Deflate.Correctness.decode_some_mem",
    "probe:Deflate.Correctness.decode_wf",
    "probe:Deflate.Correctness.distBase_eq",
    "probe:Deflate.Correctness.distExtra_eq",
    "probe:Deflate.Correctness.distExtra_le_32",
    "probe:Deflate.Correctness.fillEntries_extract",
    "probe:Deflate.Correctness.fillEntries_size",
    "probe:Deflate.Correctness.fillEntries_snd",
    "probe:Deflate.Correctness.fromLengths_complete",
    "probe:Deflate.Correctness.fromLengths_hasLeaf",
    "probe:Deflate.Correctness.fromLengths_leaf_spec",
    "probe:Deflate.Correctness.fromLengths_valid",
    "probe:Deflate.Correctness.hasLeaf_of_decodeBits",
    "probe:Deflate.Correctness.huffTree_decode_complete",
    "probe:Deflate.Correctness.huffTree_decode_correct",
    "probe:Deflate.Correctness.inflateLoop_complete",
    "probe:Deflate.Correctness.inflateLoop_correct",
    "probe:Deflate.Correctness.inflateLoop_fuel_le",
    "probe:Deflate.Correctness.inflate_correct",
    "probe:Deflate.Correctness.inflate_correct'",
    "probe:Deflate.Correctness.insert_go_complete'",
    "probe:Deflate.Correctness.insert_go_hasLeaf",
    "probe:Deflate.Correctness.insert_go_noLeafOnPath",
    "probe:Deflate.Correctness.insert_go_preserves",
    "probe:Deflate.Correctness.lengthBase_eq",
    "probe:Deflate.Correctness.lengthExtra_eq",
    "probe:Deflate.Correctness.lengthExtra_le_32",
    "probe:Deflate.Correctness.nat_beq_to_uint32_false",
    "probe:Deflate.Correctness.nat_beq_to_uint32_true",
    "probe:Deflate.Correctness.readBit_complete",
    "probe:Deflate.Correctness.readBit_toBits",
    "probe:Deflate.Correctness.readBit_wf",
    "probe:Deflate.Correctness.readBitsLSB_split",
    "probe:Deflate.Correctness.readBitsLSB_writeBitsLSB",
    "probe:Deflate.Correctness.readBits_complete",
    "probe:Deflate.Correctness.readBits_go_complete",
    "probe:Deflate.Correctness.readBits_pos_inv",
    "probe:Deflate.Correctness.readBits_toBits",
    "probe:Deflate.Correctness.readBits_wf",
    "probe:Deflate.Correctness.readBytes_complete",
    "probe:Deflate.Correctness.readBytes_toBits",
    "probe:Deflate.Correctness.readBytes_wf",
    "probe:Deflate.Correctness.readCLCodeLengths_complete",
    "probe:Deflate.Correctness.readCLCodeLengths_size",
    "probe:Deflate.Correctness.readNBytes_aligned",
    "probe:Deflate.Correctness.readNBytes_output_length",
    "probe:Deflate.Correctness.readNBytes_some_length",
    "probe:Deflate.Correctness.readUInt16LE_complete",
    "probe:Deflate.Correctness.readUInt16LE_data",
    "probe:Deflate.Correctness.readUInt16LE_toBits",
    "probe:Deflate.Correctness.readUInt16LE_wf",
    "probe:Deflate.Correctness.specTable_cw_nonempty",
    "probe:Deflate.Correctness.specTable_mem_codes",
    "probe:Deflate.Correctness.symVal_of_beq",
    "probe:Deflate.Correctness.toBits_length",
    "probe:Deflate.Correctness.toBits_nonempty_pos",
    "probe:Deflate.Correctness.toBits_readBitsLSB_byte",
    "probe:Deflate.Correctness.uint32_bit_eq_testBit",
    "probe:Deflate.Correctness.uint32_testBit",
    "probe:Deflate.Correctness.validLengths_toUInt8_roundtrip",
    "probe:Deflate.Correctness.writeBitsLSB_length",
    "probe:Deflate.Spec.CLEntry",
    "probe:Deflate.Spec.Deflate.Spec.rlDecode_go_code16",
    "probe:Deflate.Spec.Deflate.Spec.rlDecode_go_code17",
    "probe:Deflate.Spec.Deflate.Spec.rlDecode_go_code18",
    "probe:Deflate.Spec.Deflate.Spec.rlDecode_go_literal",
    "probe:Deflate.Spec.LZ77Symbol",
    "probe:Deflate.Spec.ValidSymbolList",
    "probe:Deflate.Spec.alignToByte",
    "probe:Deflate.Spec.bitsToByte",
    "probe:Deflate.Spec.bitsToBytes",
    "probe:Deflate.Spec.bitsToBytes.go",
    "probe:Deflate.Spec.bitsToNat",
    "probe:Deflate.Spec.bytesToBits",
    "probe:Deflate.Spec.bytesToBits.byteToBits",
    "probe:Deflate.Spec.bytesToBits.byteToBits_length",
    "probe:Deflate.Spec.bytesToBits_length",
    "probe:Deflate.Spec.clPermutation",
    "probe:Deflate.Spec.clPermutation_length",
    "probe:Deflate.Spec.clSymbolFreqs",
    "probe:Deflate.Spec.clSymbolFreqs_length",
    "probe:Deflate.Spec.clSymbolFreqs_pos",
    "probe:Deflate.Spec.codeLengthOrder",
    "probe:Deflate.Spec.computeHCLEN",
    "probe:Deflate.Spec.computeHCLEN_ge_four",
    "probe:Deflate.Spec.computeHCLEN_le_nineteen",
    "probe:Deflate.Spec.countRun",
    "probe:Deflate.Spec.countRun_le_length",
    "probe:Deflate.Spec.countRun_take",
    "probe:Deflate.Spec.decode",
    "probe:Deflate.Spec.decode.go",
    "probe:Deflate.Spec.decode.goR",
    "probe:Deflate.Spec.decodeDynamicTables",
    "probe:Deflate.Spec.decodeDynamicTables.decodeCLSymbols",
    "probe:Deflate.Spec.decodeDynamicTables_append",
    "probe:Deflate.Spec.decodeDynamicTables_valid_dist",
    "probe:Deflate.Spec.decodeDynamicTables_valid_lit",
    "probe:Deflate.Spec.decodeLitLen",
    "probe:Deflate.Spec.decodeLitLen_append",
    "probe:Deflate.Spec.decodeLitLen_of_endOfBlock",
    "probe:Deflate.Spec.decodeLitLen_of_literal",
    "probe:Deflate.Spec.decodeStored",
    "probe:Deflate.Spec.decodeStored.readNBytes",
    "probe:Deflate.Spec.decodeStored_append",
    "probe:Deflate.Spec.decodeSymbols",
    "probe:Deflate.Spec.decodeSymbols_append",
    "probe:Deflate.Spec.decode_deterministic",
    "probe:Deflate.Spec.decode_goR_exists",
    "probe:Deflate.Spec.decode_goR_fst",
    "probe:Deflate.Spec.decode_go_acc_prefix",
    "probe:Deflate.Spec.decode_go_suffix",
    "probe:Deflate.Spec.deflateLevel1_spec_roundtrip",
    "probe:Deflate.Spec.deflateLevel1_spec_roundtrip'",
    "probe:Deflate.Spec.deflateLevel2_spec_roundtrip",
    "probe:Deflate.Spec.deflateStoredPure_goR",
    "probe:Deflate.Spec.distBase",
    "probe:Deflate.Spec.distExtra",
    "probe:Deflate.Spec.encodeCLEntries",
    "probe:Deflate.Spec.encodeCLEntries_isSome",
    "probe:Deflate.Spec.encodeCLExtra",
    "probe:Deflate.Spec.encodeDynamicTrees",
    "probe:Deflate.Spec.encodeDynamicTrees_decodeDynamicTables",
    "probe:Deflate.Spec.encodeDynamic_decode_append",
    "probe:Deflate.Spec.encodeDynamic_goR_rest",
    "probe:Deflate.Spec.encodeFixed",
    "probe:Deflate.Spec.encodeFixed_decode",
    "probe:Deflate.Spec.encodeFixed_decode_append",
    "probe:Deflate.Spec.encodeFixed_goR_rest",
    "probe:Deflate.Spec.encodeLitLen",
    "probe:Deflate.Spec.encodeLitLen_decodeLitLen",
    "probe:Deflate.Spec.encodeLitLen_endOfBlock_isSome",
    "probe:Deflate.Spec.encodeLitLen_literal_isSome",
    "probe:Deflate.Spec.encodeLitLen_nonempty",
    "probe:Deflate.Spec.encodeLitLen_reference_isSome",
    "probe:Deflate.Spec.encodeStored",
    "probe:Deflate.Spec.encodeStored_decode",
    "probe:Deflate.Spec.encodeStored_decode_goR",
    "probe:Deflate.Spec.encodeSymbol",
    "probe:Deflate.Spec.encodeSymbol_decode",
    "probe:Deflate.Spec.encodeSymbol_fixed_isSome",
    "probe:Deflate.Spec.encodeSymbol_isSome",
    "probe:Deflate.Spec.encodeSymbol_mem",
    "probe:Deflate.Spec.encodeSymbols",
    "probe:Deflate.Spec.encodeSymbols_decodeSymbols",
    "probe:Deflate.Spec.encodeSymbols_isSome_of_all",
    "probe:Deflate.Spec.findDistCode",
    "probe:Deflate.Spec.findDistCode.go",
    "probe:Deflate.Spec.findDistCode_code_bound",
    "probe:Deflate.Spec.findDistCode_isSome",
    "probe:Deflate.Spec.findDistCode_spec",
    "probe:Deflate.Spec.findDistCode_upper",
    "probe:Deflate.Spec.findLengthCode",
    "probe:Deflate.Spec.findLengthCode.go",
    "probe:Deflate.Spec.findLengthCode_idx_bound",
    "probe:Deflate.Spec.findLengthCode_isSome",
    "probe:Deflate.Spec.findLengthCode_spec",
    "probe:Deflate.Spec.findLengthCode_upper",
    "probe:Deflate.Spec.findLongestMatch",
    "probe:Deflate.Spec.findLongestMatch.go",
    "probe:Deflate.Spec.findLongestMatch_dist_bounds",
    "probe:Deflate.Spec.findLongestMatch_dist_le_windowSize",
    "probe:Deflate.Spec.findLongestMatch_end_le",
    "probe:Deflate.Spec.findLongestMatch_len_ge",
    "probe:Deflate.Spec.findLongestMatch_matchLength",
    "probe:Deflate.Spec.fixedDistCodes_prefix_free",
    "probe:Deflate.Spec.fixedDistLengths",
    "probe:Deflate.Spec.fixedDistLengths_entry_bounds",
    "probe:Deflate.Spec.fixedDistLengths_getElem_le",
    "probe:Deflate.Spec.fixedDistLengths_getElem_pos",
    "probe:Deflate.Spec.fixedDistLengths_length",
    "probe:Deflate.Spec.fixedDistLengths_valid",
    "probe:Deflate.Spec.fixedLitCodes_prefix_free",
    "probe:Deflate.Spec.fixedLitLengths",
    "probe:Deflate.Spec.fixedLitLengths_entry_bounds",
    "probe:Deflate.Spec.fixedLitLengths_getElem_le",
    "probe:Deflate.Spec.fixedLitLengths_getElem_pos",
    "probe:Deflate.Spec.fixedLitLengths_length",
    "probe:Deflate.Spec.fixedLitLengths_valid",
    "probe:Deflate.Spec.flipped_allCodes_prefix_free",
    "probe:Deflate.Spec.instBEqLZ77Symbol",
    "probe:Deflate.Spec.instBEqLZ77Symbol.beq",
    "probe:Deflate.Spec.instReprLZ77Symbol",
    "probe:Deflate.Spec.instReprLZ77Symbol.repr",
    "probe:Deflate.Spec.lengthBase",
    "probe:Deflate.Spec.lengthExtra",
    "probe:Deflate.Spec.matchLZ77",
    "probe:Deflate.Spec.matchLZ77.go",
    "probe:Deflate.Spec.matchLZ77Lazy",
    "probe:Deflate.Spec.matchLZ77Lazy.go",
    "probe:Deflate.Spec.matchLZ77Lazy_encodable",
    "probe:Deflate.Spec.matchLZ77Lazy_length_le",
    "probe:Deflate.Spec.matchLZ77Lazy_validSymbolList",
    "probe:Deflate.Spec.matchLZ77_encodable",
    "probe:Deflate.Spec.matchLZ77_length_le",
    "probe:Deflate.Spec.matchLZ77_validSymbolList",
    "probe:Deflate.Spec.matchLength",
    "probe:Deflate.Spec.matchLength.go",
    "probe:Deflate.Spec.matchLength.go_bounds",
    "probe:Deflate.Spec.matchLength.go_correct",
    "probe:Deflate.Spec.matchLength.go_in_bounds",
    "probe:Deflate.Spec.matchLength_correct",
    "probe:Deflate.Spec.matchLength_in_bounds",
    "probe:Deflate.Spec.matchLength_le_258",
    "probe:Deflate.Spec.readBitsLSB",
    "probe:Deflate.Spec.readBitsLSB_append",
    "probe:Deflate.Spec.readBitsLSB_bound",
    "probe:Deflate.Spec.readBitsLSB_some_length",
    "probe:Deflate.Spec.readCLLengths",
    "probe:Deflate.Spec.readCLLengths_writeCLLengths",
    "probe:Deflate.Spec.resolveLZ77",
    "probe:Deflate.Spec.resolveLZ77_endOfBlock",
    "probe:Deflate.Spec.resolveLZ77_endOfBlock_empty",
    "probe:Deflate.Spec.resolveLZ77_extends",
    "probe:Deflate.Spec.resolveLZ77_literal",
    "probe:Deflate.Spec.resolveLZ77_literal_cons",
    "probe:Deflate.Spec.resolveLZ77_literals",
    "probe:Deflate.Spec.resolveLZ77_matchLZ77",
    "probe:Deflate.Spec.resolveLZ77_matchLZ77Lazy",
    "probe:Deflate.Spec.resolveLZ77_nil",
    "probe:Deflate.Spec.resolveLZ77_reference_dist_too_large",
    "probe:Deflate.Spec.resolveLZ77_reference_dist_zero",
    "probe:Deflate.Spec.resolveLZ77_reference_valid",
    "probe:Deflate.Spec.rlDecodeLengths",
    "probe:Deflate.Spec.rlDecodeLengths.go",
    "probe:Deflate.Spec.rlDecodeLengths_go_rlEncodeLengths_go",
    "probe:Deflate.Spec.rlDecodeLengths_rlEncodeLengths",
    "probe:Deflate.Spec.rlEncodeLengths",
    "probe:Deflate.Spec.rlEncodeLengths.go",
    "probe:Deflate.Spec.rlEncodeLengths_go_valid",
    "probe:Deflate.Spec.rlEncodeLengths_valid",
    "probe:Deflate.Spec.take_countRun_eq_replicate",
    "probe:Deflate.Spec.writeBitsLSB",
    "probe:Deflate.Spec.writeCLLengths",
    "probe:Gzip.DeflateState",
    "probe:Gzip.DeflateState.finish",
    "probe:Gzip.DeflateState.new",
    "probe:Gzip.DeflateState.nonemptyType",
    "probe:Gzip.DeflateState.push",
    "probe:Gzip.InflateState",
    "probe:Gzip.InflateState.finish",
    "probe:Gzip.InflateState.new",
    "probe:Gzip.InflateState.nonemptyType",
    "probe:Gzip.InflateState.push",
    "probe:Gzip.compress",
    "probe:Gzip.compressFile",
    "probe:Gzip.compressStream",
    "probe:Gzip.decompress",
    "probe:Gzip.decompressFile",
    "probe:Gzip.decompressStream",
    "probe:Gzip.instNonemptyDeflateState",
    "probe:Gzip.instNonemptyInflateState",
    "probe:Huffman.Spec.BuildTree",
    "probe:Huffman.Spec.BuildTree.depths",
    "probe:Huffman.Spec.BuildTree.depths_ge",
    "probe:Huffman.Spec.BuildTree.depths_ne_nil",
    "probe:Huffman.Spec.BuildTree.kraft_eq",
    "probe:Huffman.Spec.BuildTree.weight",
    "probe:Huffman.Spec.Codeword",
    "probe:Huffman.Spec.IsPrefixFree",
    "probe:Huffman.Spec.ValidLengths",
    "probe:Huffman.Spec.allCodeWords_prefix_free",
    "probe:Huffman.Spec.allCodes",
    "probe:Huffman.Spec.allCodes_mem_iff",
    "probe:Huffman.Spec.allCodes_nodup",
    "probe:Huffman.Spec.allCodes_prefix_free_of_ne",
    "probe:Huffman.Spec.assignLengths",
    "probe:Huffman.Spec.assignLengths_bounded",
    "probe:Huffman.Spec.assignLengths_length",
    "probe:Huffman.Spec.assignLengths_pos",
    "probe:Huffman.Spec.buildHuffmanTree",
    "probe:Huffman.Spec.buildTree_depths_nonempty",
    "probe:Huffman.Spec.canonical_prefix_free",
    "probe:Huffman.Spec.codeFor",
    "probe:Huffman.Spec.codeFor_injective",
    "probe:Huffman.Spec.codeFor_len_bounds",
    "probe:Huffman.Spec.codeFor_spec",
    "probe:Huffman.Spec.code_value_bound",
    "probe:Huffman.Spec.computeCodeLengths",
    "probe:Huffman.Spec.computeCodeLengths_bounded",
    "probe:Huffman.Spec.computeCodeLengths_length",
    "probe:Huffman.Spec.computeCodeLengths_nonzero",
    "probe:Huffman.Spec.computeCodeLengths_valid",
    "probe:Huffman.Spec.countLengths",
    "probe:Huffman.Spec.countLengths_eq",
    "probe:Huffman.Spec.count_foldl_mono",
    "probe:Huffman.Spec.count_le_pow_of_validLengths",
    "probe:Huffman.Spec.decode",
    "probe:Huffman.Spec.decode_deterministic",
    "probe:Huffman.Spec.decode_prefix_free",
    "probe:Huffman.Spec.decode_shorter",
    "probe:Huffman.Spec.decode_some_append",
    "probe:Huffman.Spec.decode_suffix",
    "probe:Huffman.Spec.fixKraftList",
    "probe:Huffman.Spec.fixKraftList_bounded",
    "probe:Huffman.Spec.fixKraftList_kraft",
    "probe:Huffman.Spec.fixKraftList_length",
    "probe:Huffman.Spec.fixKraftList_nonzero",
    "probe:Huffman.Spec.insertByWeight",
    "probe:Huffman.Spec.insertByWeight_length",
    "probe:Huffman.Spec.instDecidableValidLengths",
    "probe:Huffman.Spec.instReprBuildTree",
    "probe:Huffman.Spec.instReprBuildTree.repr",
    "probe:Huffman.Spec.isPrefixOf",
    "probe:Huffman.Spec.isPrefixOf_iff",
    "probe:Huffman.Spec.kraftSum",
    "probe:Huffman.Spec.natToBits",
    "probe:Huffman.Spec.natToBits_eq_iff",
    "probe:Huffman.Spec.natToBits_injective",
    "probe:Huffman.Spec.natToBits_length",
    "probe:Huffman.Spec.ncRec",
    "probe:Huffman.Spec.ncRec_shift",
    "probe:Huffman.Spec.nextCodes",
    "probe:Huffman.Spec.nextCodes.go",
    "probe:Huffman.Spec.nextCodes_eq_ncRec",
    "probe:Huffman.Spec.nextCodes_plus_count_le",
    "probe:Huffman.Spec.nextCodes_size",
    "probe:Huffman.Spec.validLengths_cons",
    "probe:RawDeflate.DeflateState.new",
    "probe:RawDeflate.InflateState.new",
    "probe:RawDeflate.compress",
    "probe:RawDeflate.compressStream",
    "probe:RawDeflate.decompress",
    "probe:RawDeflate.decompressStream",
    "probe:Tar.Entry",
    "probe:Tar.Entry.gid",
    "probe:Tar.Entry.gname",
    "probe:Tar.Entry.linkname",
    "probe:Tar.Entry.mode",
    "probe:Tar.Entry.mtime",
    "probe:Tar.Entry.path",
    "probe:Tar.Entry.size",
    "probe:Tar.Entry.typeflag",
    "probe:Tar.Entry.uid",
    "probe:Tar.Entry.uname",
    "probe:Tar.applyPaxOverrides",
    "probe:Tar.buildHeader",
    "probe:Tar.buildPaxEntry",
    "probe:Tar.buildPaxRecord",
    "probe:Tar.computeChecksum",
    "probe:Tar.create",
    "probe:Tar.createFromDir",
    "probe:Tar.createTarGz",
    "probe:Tar.extract",
    "probe:Tar.extractTarGz",
    "probe:Tar.extractTarGzNative",
    "probe:Tar.instInhabitedEntry",
    "probe:Tar.instInhabitedEntry.default",
    "probe:Tar.instReprEntry",
    "probe:Tar.instReprEntry.repr",
    "probe:Tar.list",
    "probe:Tar.needsPaxHeader",
    "probe:Tar.paddingFor",
    "probe:Tar.parseHeader",
    "probe:Tar.parsePaxRecords",
    "probe:Tar.readNumeric",
    "probe:Tar.splitPath",
    "probe:Tar.typeDirectory",
    "probe:Tar.typeGnuLongLink",
    "probe:Tar.typeGnuLongName",
    "probe:Tar.typePaxExtended",
    "probe:Tar.typePaxGlobal",
    "probe:Tar.typeRegular",
    "probe:Tar.typeSymlink",
    "probe:Tar.verifyChecksum",
    "probe:Zip.Native.BitWriter",
    "probe:Zip.Native.BitWriter.bitBuf",
    "probe:Zip.Native.BitWriter.bitCount",
    "probe:Zip.Native.BitWriter.data",
    "probe:Zip.Native.BitWriter.empty",
    "probe:Zip.Native.BitWriter.empty_toBits",
    "probe:Zip.Native.BitWriter.empty_wf",
    "probe:Zip.Native.BitWriter.flush",
    "probe:Zip.Native.BitWriter.flush_toBits",
    "probe:Zip.Native.BitWriter.toBits",
    "probe:Zip.Native.BitWriter.wf",
    "probe:Zip.Native.BitWriter.writeBits",
    "probe:Zip.Native.BitWriter.writeBits.go",
    "probe:Zip.Native.BitWriter.writeBits_toBits",
    "probe:Zip.Native.BitWriter.writeBits_wf",
    "probe:Zip.Native.BitWriter.writeHuffCode",
    "probe:Zip.Native.BitWriter.writeHuffCode.go",
    "probe:Zip.Native.BitWriter.writeHuffCode_toBits",
    "probe:Zip.Native.BitWriter.writeHuffCode_wf",
    "probe:Zip.Native.CompressFormat",
    "probe:Zip.Native.Deflate.LZ77Token",
    "probe:Zip.Native.Deflate.LZ77Token.toLZ77Symbol",
    "probe:Zip.Native.Deflate.ValidDecomp",
    "probe:Zip.Native.Deflate.array_get!Internal_eq",
    "probe:Zip.Native.Deflate.canonicalCodes",
    "probe:Zip.Native.Deflate.canonicalCodes.go",
    "probe:Zip.Native.Deflate.canonicalCodes_size",
    "probe:Zip.Native.Deflate.canonicalCodes_snd_le",
    "probe:Zip.Native.Deflate.canonicalCodes_snd_le'",
    "probe:Zip.Native.Deflate.deflateDynamic",
    "probe:Zip.Native.Deflate.deflateDynamic_spec",
    "probe:Zip.Native.Deflate.deflateFixed",
    "probe:Zip.Native.Deflate.deflateFixedBlock",
    "probe:Zip.Native.Deflate.deflateFixedBlock_spec",
    "probe:Zip.Native.Deflate.deflateFixedIter",
    "probe:Zip.Native.Deflate.deflateFixed_spec",
    "probe:Zip.Native.Deflate.deflateLazy",
    "probe:Zip.Native.Deflate.deflateLazyIter",
    "probe:Zip.Native.Deflate.deflateLazyIter_eq_deflateLazy",
    "probe:Zip.Native.Deflate.deflateLazy_spec",
    "probe:Zip.Native.Deflate.deflateRaw",
    "probe:Zip.Native.Deflate.deflateRaw_goR_pad",
    "probe:Zip.Native.Deflate.deflateRaw_pad",
    "probe:Zip.Native.Deflate.deflateStored",
    "probe:Zip.Native.Deflate.distExtra_le_13",
    "probe:Zip.Native.Deflate.emitTokens",
    "probe:Zip.Native.Deflate.emitTokensWithCodes",
    "probe:Zip.Native.Deflate.emitTokensWithCodes_spec",
    "probe:Zip.Native.Deflate.emitTokensWithCodes_wf",
    "probe:Zip.Native.Deflate.emitTokens_spec",
    "probe:Zip.Native.Deflate.emitTokens_wf",
    "probe:Zip.Native.Deflate.encodeSymbol_canonicalCodes_eq",
    "probe:Zip.Native.Deflate.encodeSymbol_distTable_eq",
    "probe:Zip.Native.Deflate.encodeSymbol_litTable_eq",
    "probe:Zip.Native.Deflate.encodeSymbols_append",
    "probe:Zip.Native.Deflate.encodeSymbols_append_inv",
    "probe:Zip.Native.Deflate.encodeSymbols_cons_some",
    "probe:Zip.Native.Deflate.encodeSymbols_tokensToSymbols_isSome",
    "probe:Zip.Native.Deflate.encodeSymbols_tokensToSymbols_lazy_isSome",
    "probe:Zip.Native.Deflate.findDistCode",
    "probe:Zip.Native.Deflate.findDistCode_agree",
    "probe:Zip.Native.Deflate.findLengthCode",
    "probe:Zip.Native.Deflate.findLengthCode_agree",
    "probe:Zip.Native.Deflate.findTableCode",
    "probe:Zip.Native.Deflate.findTableCode.go",
    "probe:Zip.Native.Deflate.findTableCode_go_extraN",
    "probe:Zip.Native.Deflate.findTableCode_go_idx_bound",
    "probe:Zip.Native.Deflate.fixedDistCodes",
    "probe:Zip.Native.Deflate.fixedDistCodes_size",
    "probe:Zip.Native.Deflate.fixedLitCodes",
    "probe:Zip.Native.Deflate.fixedLitCodes_size",
    "probe:Zip.Native.Deflate.freqPairs_witness",
    "probe:Zip.Native.Deflate.inflate_complete",
    "probe:Zip.Native.Deflate.inflate_deflateDynamic",
    "probe:Zip.Native.Deflate.inflate_deflateFixed",
    "probe:Zip.Native.Deflate.inflate_deflateFixedIter",
    "probe:Zip.Native.Deflate.inflate_deflateLazy",
    "probe:Zip.Native.Deflate.inflate_deflateLazyIter",
    "probe:Zip.Native.Deflate.inflate_deflateRaw",
    "probe:Zip.Native.Deflate.instBEqLZ77Token",
    "probe:Zip.Native.Deflate.instBEqLZ77Token.beq",
    "probe:Zip.Native.Deflate.instInhabitedLZ77Token",
    "probe:Zip.Native.Deflate.instInhabitedLZ77Token.default",
    "probe:Zip.Native.Deflate.lengthExtra_le_5",
    "probe:Zip.Native.Deflate.lz77Greedy",
    "probe:Zip.Native.Deflate.lz77Greedy.countMatch",
    "probe:Zip.Native.Deflate.lz77Greedy.countMatch_matches",
    "probe:Zip.Native.Deflate.lz77Greedy.go",
    "probe:Zip.Native.Deflate.lz77Greedy.go_matches",
    "probe:Zip.Native.Deflate.lz77Greedy.hash3",
    "probe:Zip.Native.Deflate.lz77Greedy.mainLoop",
    "probe:Zip.Native.Deflate.lz77Greedy.trailing",
    "probe:Zip.Native.Deflate.lz77Greedy.updateHashes",
    "probe:Zip.Native.Deflate.lz77GreedyIter",
    "probe:Zip.Native.Deflate.lz77GreedyIter.countMatch",
    "probe:Zip.Native.Deflate.lz77GreedyIter.go",
    "probe:Zip.Native.Deflate.lz77GreedyIter.hash3",
    "probe:Zip.Native.Deflate.lz77GreedyIter.mainLoop",
    "probe:Zip.Native.Deflate.lz77GreedyIter.trailing",
    "probe:Zip.Native.Deflate.lz77GreedyIter.updateHashes",
    "probe:Zip.Native.Deflate.lz77GreedyIter_eq_lz77Greedy",
    "probe:Zip.Native.Deflate.lz77Greedy_encodable",
    "probe:Zip.Native.Deflate.lz77Greedy_resolves",
    "probe:Zip.Native.Deflate.lz77Greedy_size_le",
    "probe:Zip.Native.Deflate.lz77Greedy_spec_decode",
    "probe:Zip.Native.Deflate.lz77Greedy_valid",
    "probe:Zip.Native.Deflate.lz77Lazy",
    "probe:Zip.Native.Deflate.lz77Lazy.countMatch",
    "probe:Zip.Native.Deflate.lz77Lazy.countMatch_matches",
    "probe:Zip.Native.Deflate.lz77Lazy.go",
    "probe:Zip.Native.Deflate.lz77Lazy.go_matches",
    "probe:Zip.Native.Deflate.lz77Lazy.hash3",
    "probe:Zip.Native.Deflate.lz77Lazy.mainLoop",
    "probe:Zip.Native.Deflate.lz77Lazy.mainLoop_encodable",
    "probe:Zip.Native.Deflate.lz77Lazy.mainLoop_length",
    "probe:Zip.Native.Deflate.lz77Lazy.mainLoop_valid",
    "probe:Zip.Native.Deflate.lz77Lazy.trailing",
    "probe:Zip.Native.Deflate.lz77Lazy.trailing_encodable",
    "probe:Zip.Native.Deflate.lz77Lazy.trailing_length",
    "probe:Zip.Native.Deflate.lz77Lazy.trailing_valid",
    "probe:Zip.Native.Deflate.lz77Lazy.updateHashes",
    "probe:Zip.Native.Deflate.lz77LazyIter",
    "probe:Zip.Native.Deflate.lz77LazyIter.mainLoop",
    "probe:Zip.Native.Deflate.lz77LazyIter.trailing",
    "probe:Zip.Native.Deflate.lz77LazyIter_eq_lz77Lazy",
    "probe:Zip.Native.Deflate.lz77Lazy_encodable",
    "probe:Zip.Native.Deflate.lz77Lazy_resolves",
    "probe:Zip.Native.Deflate.lz77Lazy_size_le",
    "probe:Zip.Native.Deflate.lz77Lazy_spec_decode",
    "probe:Zip.Native.Deflate.lz77Lazy_valid",
    "probe:Zip.Native.Deflate.mainLoop_encodable",
    "probe:Zip.Native.Deflate.mainLoop_length",
    "probe:Zip.Native.Deflate.mainLoop_valid",
    "probe:Zip.Native.Deflate.nativeFindDistCode_extraN_bound",
    "probe:Zip.Native.Deflate.nativeFindDistCode_idx_bound",
    "probe:Zip.Native.Deflate.nativeFindLengthCode_extraN_bound",
    "probe:Zip.Native.Deflate.nativeFindLengthCode_idx_bound",
    "probe:Zip.Native.Deflate.toUInt8Array_le",
    "probe:Zip.Native.Deflate.tokenFreqs",
    "probe:Zip.Native.Deflate.tokenFreqs.go",
    "probe:Zip.Native.Deflate.tokenFreqs_distCode_pos",
    "probe:Zip.Native.Deflate.tokenFreqs_eob_pos",
    "probe:Zip.Native.Deflate.tokenFreqs_go_distCode_pos",
    "probe:Zip.Native.Deflate.tokenFreqs_go_lengthCode_pos",
    "probe:Zip.Native.Deflate.tokenFreqs_go_literal_pos",
    "probe:Zip.Native.Deflate.tokenFreqs_go_mono",
    "probe:Zip.Native.Deflate.tokenFreqs_go_sizes",
    "probe:Zip.Native.Deflate.tokenFreqs_lengthCode_pos",
    "probe:Zip.Native.Deflate.tokenFreqs_literal_pos",
    "probe:Zip.Native.Deflate.tokenFreqs_sizes",
    "probe:Zip.Native.Deflate.tokensToSymbols",
    "probe:Zip.Native.Deflate.tokensToSymbols_encodable",
    "probe:Zip.Native.Deflate.tokensToSymbols_lazy_encodable",
    "probe:Zip.Native.Deflate.tokensToSymbols_length",
    "probe:Zip.Native.Deflate.tokensToSymbols_validSymbolList",
    "probe:Zip.Native.Deflate.trailing_encodable",
    "probe:Zip.Native.Deflate.trailing_length",
    "probe:Zip.Native.Deflate.trailing_valid",
    "probe:Zip.Native.Deflate.validDecomp_resolves",
    "probe:Zip.Native.Deflate.validDecomp_resolves_aux",
    "probe:Zip.Native.Deflate.writeDynamicHeader",
    "probe:Zip.Native.Deflate.writeDynamicHeader.writeCLEntries",
    "probe:Zip.Native.Deflate.writeDynamicHeader.writeCLLengths",
    "probe:Zip.Native.Deflate.writeDynamicHeader_spec",
    "probe:Zip.Native.Deflate.writeDynamicHeader_wf",
    "probe:Zip.Native.GzipDecode.decompress",
    "probe:Zip.Native.GzipDecode.decompressSingle",
    "probe:Zip.Native.GzipEncode.compress",
    "probe:Zip.Native.GzipEncode.compress_crc32",
    "probe:Zip.Native.GzipEncode.compress_eq",
    "probe:Zip.Native.GzipEncode.compress_header_bytes",
    "probe:Zip.Native.GzipEncode.compress_isize",
    "probe:Zip.Native.GzipEncode.compress_size",
    "probe:Zip.Native.HuffTree",
    "probe:Zip.Native.HuffTree.decode",
    "probe:Zip.Native.HuffTree.decode.go",
    "probe:Zip.Native.HuffTree.fromLengths",
    "probe:Zip.Native.HuffTree.fromLengthsTree",
    "probe:Zip.Native.HuffTree.insert",
    "probe:Zip.Native.HuffTree.insert.go",
    "probe:Zip.Native.HuffTree.insertLoop",
    "probe:Zip.Native.Inflate.codeLengthOrder",
    "probe:Zip.Native.Inflate.codeLengthOrder_size",
    "probe:Zip.Native.Inflate.copyLoop",
    "probe:Zip.Native.Inflate.decodeCLSymbols",
    "probe:Zip.Native.Inflate.decodeDynamicTrees",
    "probe:Zip.Native.Inflate.decodeHuffman",
    "probe:Zip.Native.Inflate.decodeHuffman.go",
    "probe:Zip.Native.Inflate.decodeStored",
    "probe:Zip.Native.Inflate.distBase",
    "probe:Zip.Native.Inflate.distBase_size",
    "probe:Zip.Native.Inflate.distExtra",
    "probe:Zip.Native.Inflate.distExtra_size",
    "probe:Zip.Native.Inflate.fillEntries",
    "probe:Zip.Native.Inflate.fixedDistLengths",
    "probe:Zip.Native.Inflate.fixedLitLengths",
    "probe:Zip.Native.Inflate.inflate",
    "probe:Zip.Native.Inflate.inflateLoop",
    "probe:Zip.Native.Inflate.inflateRaw",
    "probe:Zip.Native.Inflate.lengthBase",
    "probe:Zip.Native.Inflate.lengthBase_size",
    "probe:Zip.Native.Inflate.lengthExtra",
    "probe:Zip.Native.Inflate.lengthExtra_size",
    "probe:Zip.Native.Inflate.readCLCodeLengths",
    "probe:Zip.Native.ZlibDecode.decompress",
    "probe:Zip.Native.ZlibDecode.decompressSingle",
    "probe:Zip.Native.ZlibEncode.compress",
    "probe:Zip.Native.ZlibEncode.compress_adler32",
    "probe:Zip.Native.ZlibEncode.compress_cinfo",
    "probe:Zip.Native.ZlibEncode.compress_cm",
    "probe:Zip.Native.ZlibEncode.compress_cmf",
    "probe:Zip.Native.ZlibEncode.compress_eq",
    "probe:Zip.Native.ZlibEncode.compress_header_check",
    "probe:Zip.Native.ZlibEncode.compress_no_fdict",
    "probe:Zip.Native.ZlibEncode.compress_size",
    "probe:Zip.Native.bytesToBits_append",
    "probe:Zip.Native.bytesToBits_drop_prefix_three",
    "probe:Zip.Native.compressAuto",
    "probe:Zip.Native.decodeCLSymbols_inv",
    "probe:Zip.Native.decodeDynamicTrees_inv",
    "probe:Zip.Native.decodeHuffman_go_inv",
    "probe:Zip.Native.decodeHuffman_inv",
    "probe:Zip.Native.decodeStored_inv",
    "probe:Zip.Native.decode_inv",
    "probe:Zip.Native.decompressAuto",
    "probe:Zip.Native.detectFormat",
    "probe:Zip.Native.gzip_decompressSingle_compress",
    "probe:Zip.Native.inflateLoop_complete_ext",
    "probe:Zip.Native.inflateLoop_endPos_le",
    "probe:Zip.Native.inflateRaw_append_suffix",
    "probe:Zip.Native.inflateRaw_complete",
    "probe:Zip.Native.inflateRaw_endPos_eq",
    "probe:Zip.Native.inflateRaw_endPos_ge",
    "probe:Zip.Native.inflateRaw_endPos_le",
    "probe:Zip.Native.inflate_to_spec_decode",
    "probe:Zip.Native.readCLCodeLengths_inv",
    "probe:Zip.Native.zlib_decompressSingle_compress",
    "probe:Zip.Spec.DeflateStoredCorrect.decodeStored_align",
    "probe:Zip.Spec.DeflateStoredCorrect.decodeStored_on_block",
    "probe:Zip.Spec.DeflateStoredCorrect.deflateStoredPure",
    "probe:Zip.Spec.DeflateStoredCorrect.deflateStoredPure_size",
    "probe:Zip.Spec.DeflateStoredCorrect.deflateStoredPure_size_bound",
    "probe:Zip.Spec.DeflateStoredCorrect.fromLengths_fixedDist_ok",
    "probe:Zip.Spec.DeflateStoredCorrect.fromLengths_fixedLit_ok",
    "probe:Zip.Spec.DeflateStoredCorrect.inflateLoop_final_stored",
    "probe:Zip.Spec.DeflateStoredCorrect.inflateLoop_nonfinal_stored",
    "probe:Zip.Spec.DeflateStoredCorrect.inflate_deflateStoredPure",
    "probe:Zip.Spec.DeflateStoredCorrect.readBits_1_at_0",
    "probe:Zip.Spec.DeflateStoredCorrect.readBits_2_at_1",
    "probe:Zip.Spec.DeflateStoredCorrect.readBytes_at_aligned",
    "probe:Zip.Spec.DeflateStoredCorrect.readUInt16LE_align",
    "probe:Zip.Spec.DeflateStoredCorrect.readUInt16LE_at_aligned",
    "probe:Zip.Spec.DeflateStoredCorrect.storedBlockHdr",
    "probe:Zip.Spec.DeflateStoredCorrect.storedBlockHdr_size",
    "probe:Zip.Spec.DeflateStoredCorrect.uint16_le_roundtrip",
    "probe:Zip.Spec.DeflateStoredCorrect.uint16_xor_complement",
    "probe:ZipCommon.BitReader.toBits",
    "probe:ZipTest.Archive.tests",
    "probe:ZipTest.Benchmark.tests",
    "probe:ZipTest.Binary.tests",
    "probe:ZipTest.Checksum.tests",
    "probe:ZipTest.CompressFixtures.tests",
    "probe:ZipTest.Gzip.tests",
    "probe:ZipTest.NativeChecksum.tests",
    "probe:ZipTest.NativeCompressBench.tests",
    "probe:ZipTest.NativeDeflate.tests",
    "probe:ZipTest.NativeGzip.tests",
    "probe:ZipTest.NativeInflate.tests",
    "probe:ZipTest.NativeIntegration.tests",
    "probe:ZipTest.NativeScale.Pattern",
    "probe:ZipTest.NativeScale.Pattern.generate",
    "probe:ZipTest.NativeScale.Pattern.name",
    "probe:ZipTest.NativeScale.TimingEntry",
    "probe:ZipTest.NativeScale.TimingEntry.ns",
    "probe:ZipTest.NativeScale.TimingEntry.op",
    "probe:ZipTest.NativeScale.TimingEntry.pat",
    "probe:ZipTest.NativeScale.TimingEntry.size",
    "probe:ZipTest.NativeScale.levels",
    "probe:ZipTest.NativeScale.matrixSizes",
    "probe:ZipTest.NativeScale.patterns",
    "probe:ZipTest.NativeScale.sweepSizes",
    "probe:ZipTest.NativeScale.tests",
    "probe:ZipTest.RawDeflate.tests",
    "probe:ZipTest.Tar.tests",
    "probe:ZipTest.TarFixtures.tests",
    "probe:ZipTest.Utf8Fixtures.tests",
    "probe:ZipTest.ZipFixtures.tests",
    "probe:ZipTest.Zlib.tests",
    "probe:Zlib.compress",
    "probe:Zlib.decompress",
    "probe:assertThrows",
    "probe:byteArrayReadStream",
    "probe:calibrateIters",
    "probe:fmtMBps",
    "probe:fmtMs",
    "probe:fmtRatio",
    "probe:forceEval",
    "probe:fragmentingStream",
    "probe:main",
    "probe:mkConstantData",
    "probe:mkCyclicData",
    "probe:mkLargeData",
    "probe:mkPrngData",
    "probe:mkRandomData",
    "probe:mkTestData",
    "probe:mkTextData",
    "probe:pad",
    "probe:readFixture",
    "probe:sizeName",
    "probe:timeIO",
    "probe:writeFixtureTmp"
  ],
  "verified_functions_count": 773
}
Our open standard for verification certification

We have designed our VeriLib verification certificates to meet three goals:

  • Transparency: Easy to see precisely what has been verified about what code with what tooling & assumptions
  • Reproducibility: Easy for user to automatically reproduce all certified claims, so no need to trust the issuer of the certificate
  • Usability: Quick and easy to build the desired level of trust:
    • Busy users can choose trust crowdsourcing: simply trusting software with the green checkmark, knowing that if it were fraudulent, someone else would probably have tried to reproduce it, failed, sounded the alarm, and permanently destroyed VeriLib’s credibility.
    • More hardcore users can automatically repeat and inspect the entire verification process on their own machine.

Here is how this works in detail. The green checkmark displayed (at the top of certificate pages such as this one) is not static, but dynamically generated if and only if three hashes stored on the Ethereum blockchain satisfy these properties:

a) The GitHub repo hash matches that of the linked repo (certifying that we’re verifying the right code)

b) The DockerHub container hash matches that of the linked container (certifying that we’re using the right verification tooling)

c) The manifest hash matches that of the displayed manifest (certifying that we’re showing the right verification result)

d) That the manifest shows VerificationSuccess = true

Blockchain commit time — (on-chain timestamp: Ethereum proof)
GitHub / repo hash 78e5bd6950afdda3ab88dbd567e54bc6adedf3ae (browse tree)
DockerHub / container hash sha256:35a8278977e69d93c08d9ab9c3a9661c1651d9f23296b524c5b1c842d91f01ed
Manifest hash 0464c6bbd288ab6fbff75d240095cb3b340bb79d661ca67ac40d7d0a1eae8bcd (SHA-256 of published JSON file)

Running the Verify it yourself script (instructions below) checks that applying the verification tooling (b) to the code (a) reproduces the manifest (c).

To save you time, VeriLib has already auto-run this same script, which produces both pedagogical output to the terminal and the result summary file manifest.json.

We encourage you to not only run this tooling, but also inspect it for correctness. You can build trust in this certificate page by checking the text in green against the manifest, and by noting that the manifest lists as successfully verified all functions in the Specifications section.

Verify it yourself

You do not need to clone any repository. Download the small bash script below using wget or curl. Running it pulls the prebuilt image from Docker Hub and writes the same manifests and lists this page publishes. A full run can take a long time and use significant disk space—plan for that before you start.

  1. Get the script with wget (saves as verify.sh in the current directory):
    wget -O verify.sh https://verilib.org/cert/5165/verify-script

    Same URL with curl: curl -fsSL -o verify.sh https://verilib.org/cert/5165/verify-script

  2. bash verify.sh --cert-verify-url 'https://verilib.org' 'verilib/probe-lean-repo-5165@sha256:35a8278977e69d93c08d9ab9c3a9661c1651d9f23296b524c5b1c842d91f01ed' 'VERIFICATION_RESULTS'

Once you have finished running the script, the file VERIFICATION_RESULTS/manifest.json should match what is shown in the Results section above (downloadable here).

Install Docker

You need a working Docker install before you can pull the certificate image or run the verification script. For the canonical, up-to-date steps (including licensing and system requirements), use Docker’s official guide: Get Docker.

  • macOS: Install Docker Desktop for Mac (Apple Silicon or Intel per your Mac). Open the app from Applications, complete onboarding, and wait until Docker reports “running”. Detailed steps: Install Docker Desktop on Mac.
  • Windows: Install Docker Desktop for Windows. Use WSL 2 backend when prompted. After install, start Docker Desktop and wait until it is ready. Detailed steps: Install Docker Desktop on Windows.
  • Linux: Install Docker Engine (and optionally Docker Compose plugin) for your distribution—do not rely on a random apt package without checking Docker’s repo instructions. Detailed steps: Install Docker Engine (choose your distro: Ubuntu, Debian, Fedora, etc.).

Smoke test: In a terminal, run docker version. You should see both Client and Server sections. If you see docker: command not found, the CLI is not on your PATH yet—restart the terminal or finish Docker Desktop’s setup.

Reproducible Docker image (open source)

Latest certificate: v1 — /cert/5165 and /cert/5165?p=1&c=v1 pin the image below.

The Docker image verilib/probe-lean-repo-5165@sha256:35a8278977e69d93c08d9ab9c3a9661c1651d9f23296b524c5b1c842d91f01ed on Docker Hub matches this certificate’s published dockerHubImageDigest / manifest image. Use Verify it yourself to pull and run—no clone required.