The project's README from github.com/theorem-labs/oss-verify-proofs. As one markdown file: README.md.
OSS-Fuzz runs the fuzz targets of open-source projects to search for inputs that make them fail. This repository holds Rocq proofs that, for some of these fuzz targets, no such input exists within stated limits. Each proof is about compiled binaries, not source code. It shows that, on every input within the limits, the build with a sanitizer behaves like the plain build and the sanitizer never detects an error, or that every execution of a build ends with a status the statement allows. OSS Verify is a Theorem program; a maintainer enrolls a project at theorem-labs/oss-verify.
61 entry points in 26 libraries have proofs. The proofs are checked with Rocq 9.2.0. They are stated in LPS, a formal model of a Linux process that runs a RISC-V binary.
LPS is best effort and not complete. It describes part of Linux, and it makes some assumptions that it does not check. A proof is only as good as LPS. docs/semantics.md gives the design principles of LPS and its limits.
| library | entry point | sanitizer builds proved |
|---|---|---|
| boost-beast | http_request | ASan, UBSan, ASan+UBSan |
| boost-json | fuzz_parse | ASan, UBSan, ASan+UBSan |
| bzip2 | bzip2_compress_target | ASan, UBSan, ASan+UBSan |
| cgif | cgif_file_fuzzer | ASan, UBSan, ASan+UBSan |
| cgif | cgif_rgb_fuzzer | ASan, UBSan, ASan+UBSan |
| cjson | cjson_read_fuzzer | ASan, UBSan, ASan+UBSan |
| coturn | FuzzStunClient | ASan, UBSan, ASan+UBSan |
| double-conversion | string_to_double_fuzzer | ASan, UBSan, ASan+UBSan |
| fast_float | from_chars | ASan, UBSan, ASan+UBSan |
| glaze | binary_reflection | ASan, UBSan, ASan+UBSan |
| json-c | json_object_fuzzer | ASan, UBSan, ASan+UBSan |
| jsoncons | fuzz_bigint | ASan, UBSan, ASan+UBSan |
| jsoncons | fuzz_bson_parser_max | ASan, UBSan, ASan+UBSan |
| jsoncons | fuzz_json_cursor | ASan, UBSan, ASan+UBSan |
| jsoncons | fuzz_json_encoder | ASan, UBSan, ASan+UBSan |
| jsoncons | fuzz_msgpack_encoder | ASan |
| jsoncons | fuzz_ubjson_encoder | ASan, UBSan, ASan+UBSan |
| jsoncons | fuzz_ubjson_parser_max | ASan, UBSan, ASan+UBSan |
| leptonica | bilateral_fuzzer | ASan, UBSan, ASan+UBSan |
| leptonica | colorfill_fuzzer | ASan, UBSan, ASan+UBSan |
| leptonica | edge_fuzzer | ASan, UBSan, ASan+UBSan |
| leptonica | fhmtgen_fuzzer | ASan, UBSan, ASan+UBSan |
| leptonica | graymorph_fuzzer | ASan, UBSan, ASan+UBSan |
| leptonica | grayquant_fuzzer | ASan, UBSan, ASan+UBSan |
| leptonica | jpegiostub_fuzzer | ASan, UBSan, ASan+UBSan |
| leptonica | kernel_fuzzer | ASan, UBSan, ASan+UBSan |
| leptonica | paintcmap_fuzzer | ASan, UBSan, ASan+UBSan |
| leptonica | pix1_fuzzer | ASan, UBSan, ASan+UBSan |
| leptonica | pix_orient_fuzzer | ASan, UBSan, ASan+UBSan |
| libpcap | fuzz_pcap | ASan, UBSan, ASan+UBSan |
| mbedtls | fuzz_pkcs7 | ASan, UBSan, ASan+UBSan |
| msgpack-c | unpack_pack_fuzzer | ASan, UBSan, ASan+UBSan |
| openssl | bignum | ASan, UBSan, ASan+UBSan |
| openssl | bndiv | ASan, UBSan, ASan+UBSan |
| openssl | ct | ASan, UBSan, ASan+UBSan |
| openssl | echconfiglist_parser | ASan, UBSan, ASan+UBSan |
| openssl | hashtable | ASan, UBSan, ASan+UBSan |
| openssl | pem | ASan, UBSan, ASan+UBSan |
| openssl | punycode | ASan, UBSan, ASan+UBSan |
| pupnp | FuzzHttp | ASan, UBSan, ASan+UBSan |
| simdjson | fuzz_atpointer | ASan, UBSan, ASan+UBSan |
| simdjson | fuzz_dump | ASan, UBSan, ASan+UBSan |
| simdjson | fuzz_dump_raw_tape | ASan, UBSan, ASan+UBSan |
| simdjson | fuzz_element | ASan, UBSan, ASan+UBSan |
| simdjson | fuzz_implementations | ASan, UBSan, ASan+UBSan |
| simdjson | fuzz_minifyimpl | ASan, UBSan, ASan+UBSan |
| simdjson | fuzz_ondemand | ASan, UBSan, ASan+UBSan |
| simdjson | fuzz_parser | ASan, UBSan, ASan+UBSan |
| simdjson | fuzz_print_json | ASan, UBSan, ASan+UBSan |
| simdjson | fuzz_utf8 | ASan, UBSan, ASan+UBSan |
| skcms | iccprofile_info | ASan, UBSan, ASan+UBSan |
| speex | speex_decode_fuzzer_float | ASan, UBSan, ASan+UBSan |
| spirv-tools | spvtools_binary_parser_fuzzer | ASan, UBSan, ASan+UBSan |
| tinyobjloader | fuzz_tobj_c | ASan, UBSan, ASan+UBSan |
| varnish | esi_parse_fuzzer | ASan, UBSan, ASan+UBSan |
| yajl-ruby | json_fuzzer | ASan, UBSan, ASan+UBSan |
| zlib | checksum_fuzzer | - |
| zstd | fse_read_ncount | ASan, UBSan, ASan+UBSan |
| zstd | huf_decompress | ASan, UBSan, ASan+UBSan |
| zstd | simple_decompress | ASan, UBSan, ASan+UBSan |
| zstd | zstd_frame_info | ASan, UBSan, ASan+UBSan |
index/PROOFS.md has one row for each entry point: the statements proved, the system-call failures they allow, the binaries, and where the proof is.
Every proof is about the binaries of this release and the statements under projects/. All of them use one LPS version and one static AddressSanitizer (Versions). docs/origin.md says how the proofs were made: the proving task, its submissions and its checker, and how a proof enters this repository.
Every proof here proves one or more agreement statements, halts statements, or both. There is one agreement statement for each sanitizer build: AddressSanitizer (ASan), UndefinedBehaviorSanitizer (UBSan), or both (ASan+UBSan). An agreement statement says:
On every input on which the plain build stays within its memory budget, neither build reaches an error, and the plain build and the sanitizer build have the same set of observable behaviours.
/ (docs/semantics.md).abort() (a failed assert(), a sanitizer report or an uncaught C++ exception), a failed UBSan check, or a step that LPS does not interpret. In a Rust fuzz target, a failed rustc UB check is not an error: it exits with status 79 after a line on standard error that the plain build does not write at that point, so agreement rules it out too.So an agreement proof rules out every error that the sanitizer build detects, on every input that the statement covers.
A halts statement is about one build alone. It says that on every covered input, every execution of that build ends, and that it ends with a status the statement allows: status 0 or 2 for most harnesses, and any status for espeak-ng's ssml-fuzzer. Its premises are its own: the build is never refused memory for exceeding 16 GiB, and the environment refuses nothing that the process's state does not force. A _halts_may_fail statement drops both premises and allows any status.
If the harness checks a property with assert(), abort() or a trap, and the check is in the binary, an agreement proof shows that the property holds on every covered input. A halts proof shows it only for the checks that the fuzz target's page names: a check seen in the binary, of a fuzz target whose linked code installs no handler that could end a failed check with a status of its own (failure_handlers: none). A failed check of these kinds then kills the process, which no halts statement allows. A check that ends the process with exit() instead is shown only when the call reaches the driver's exit guard (exit_reaches_guard: true), which ends the process with status 77 whatever status the source passes, and only by a halts statement whose allowed statuses leave out 77 (docs/facts.md, docs/exploring.md, docs/statements.md).
The Rocq definitions are in theories/Shapes.v. Each agreement and halts form is proved equal to its LPS definition: an agreement form to strong_universal_error_free_T_budgets or one of its variants, a halts form to halts_allowed_T_scfg_budgets or halts_allowed_T_scfg. docs/statements.md explains each form.
| item | version |
|---|---|
| Rocq | 9.2.0, the official release (opam package rocq-core). The proofs load their libraries with plain Require. |
| checker image | ghcr.io/theorem-labs/oss-fuzz-theorems-checker@sha256:cc9ae43a9f4b0dd59d7c8d30727d36e039bfe72a2a9f9c4a99c68e413037e902. It holds Rocq, LPS with its elf-snapshot tool, the Rocq libraries that the proofs use, dune and Python 3, and no proof automation (toolchain/checker.Dockerfile). |
| LPS | rocq-linux-process-semantics commit f1006fe81783, for every statement and every proof (docs/semantics.md) |
| static AddressSanitizer | static-asan commit b0506135: the published source of the static AddressSanitizer that built every ASan binary of this release (docs/building.md) |
| OSS-Fuzz | bd2ce219 |
| axioms | only the axioms in toolchain/allowed-axioms.txt: the primitive integer, array and string types of Rocq with their specifications, and six axioms of the standard library (classic, functional_extensionality_dep, constructive_indefinite_description, propositional_extensionality, sig_forall_dec and sig_not_dec) |
You need Docker, zstd, and Python 3 with the packages tools/oft/requirements.txt pins (PyYAML; for ./oft lint, also idna). The checker image holds Rocq and LPS, but not PyYAML, so the commands below mount it. On 16 cores, one proof check needs up to 20 GiB of memory. It compiles one file per core, so more cores need more memory; docker run --cpuset-cpus limits the cores. --ulimit stack=-1:-1 gives the container an unlimited stack limit: Rocq needs a hard limit of at least 1 GiB, and without the flag the check stops where Docker's limit is lower (docs/checking.md).
git clone https://github.com/theorem-labs/oss-verify-proofs && cd oss-verify-proofs
./oft fetch coturn # the project's binaries, each checked against its SHA-256
python3 -m pip install --require-hashes --target "$HOME/oft-pydeps" -r tools/oft/requirements.txt
docker run --rm --network none --ulimit stack=-1:-1 -u "$(id -u):$(id -g)" -e HOME=/tmp -e PYTHONPATH=/pydeps \
-v "$HOME/oft-pydeps:/pydeps:ro" -v "$PWD:/work" -w /work ghcr.io/theorem-labs/oss-fuzz-theorems-checker@sha256:cc9ae43a9f4b0dd59d7c8d30727d36e039bfe72a2a9f9c4a99c68e413037e902 \
./oft check coturn/FuzzStunClient --parts statements,proofs
oft check does these steps. It checks each binary against its SHA-256. It builds the memory images and the statements. It compiles each proof. It compiles a small wrapper that gives the proof's theorem the type of the statement. Then it reads what Print Assumptions prints for the wrapper, and it refuses every assumption that is not in the allowed list (docs/checking.md).
CI runs the same check. The release-check workflow checks what each push to main changes, and every committed proof once a week, and the badge at the top shows its result. The pr workflow checks what a pull request changes. The weekly workflow checks every statement and every proof, with no cache (docs/checking.md).
Each binary is a static riscv64 Linux program, built with clang 20.1.8 against musl. An entry point has up to four builds: plain, ASan, UBSan and ASan+UBSan. docs/building.md gives the compiler flags and the sanitizer settings. docs/running.md tells you how to run a binary and what its input file holds.
Each proof has a build record in proofs/<project>/<harness>/provenance/. The record gives the upstream repository and commit, the harness file, the recipe (for a port-built project, the OSS Verify port's build manifest and its files for the project), the compiler, the builder image, the static AddressSanitizer commit, the compiler and linker flags, the SHA-256 of each binary, and the licences. docs/reproducing.md tells you how to rebuild a binary and compare its SHA-256.
Each project's published binaries are attached to the release as one archive, and each binary is pinned by its SHA-256 in its harness.yaml. Where a project page names them, the project's upstream source trees are attached with the build recipe its binaries were built with, in the releases the page links (the source trees beside the binaries, or in a second release, v<release>-src, since a GitHub release holds at most 1,000 files); together they rebuild the binaries (docs/reproducing.md).
docs/exploring.md points to what the proofs show beyond "no sanitizer error": properties that the harnesses check, and lemmas about what the library code computes. It also tells you how to find the machine-generated data in a proof.
This repository also states theorems about many OSS-Fuzz fuzz targets, proved or not. For each of the 1,381 projects in OSS-Fuzz there is a directory under projects/. We can build the fuzz targets of 427 of these projects. 2,148 of their 5,290 fuzz targets have statements in this release; index/STATUS.md says why the others do not. Each of these fuzz targets is compiled up to four ways (2,141 of the 2,148 harnesses have all four), and each build gets Rocq statements about those exact bytes. These are statements, not results: 336 are proved, some are known to be false, and proofs are added as they are found.
In this release: 20,164 statements: 336 proved, 5 known false (0 counterexamples, 5 false (witnessed)), 0 suspected false, 229 blocked by the model, 0 withheld (0 waiting for their source bundle, 0 not published yet), 19,594 open. analyses/known-issues.md lists every statement that is not open or proved, with the reason.
There are four kinds of statement: a build halts; a sanitizer build agrees with the plain build; the two builds disagree on at most a fraction b of a stated input distribution; and the inputs on which they agree are decidable (docs/statements.md). One example:
lzo/lzo_compress_target/plain_halts: on every input on which the plain build is never refused memory for exceeding 16 GiB, and when the environment refuses nothing that it is not forced to (both are premises), every execution exits with status 0 or 2. The harness lzo_compress_target asserts that for compressible input (compressed_len < size), lzo1x_decompress into size+1 bytes must return LZO_E_OK and produce exactly size bytes. ONLY THE LENGTH is compared: the decompressed content is never memcmp'd against the input, so a decoder that returned the right number of wrong bytes would pass, so a proof shows that these hold on every input it covers.
Definition plain_halts : Prop :=
halts_within_budget Budgets.Standard.lim_source Exits.ok_or_refused Images.plain.
| status | projects |
|---|---|
| available | 427 |
| language pending | 781 |
| not yet built | 97 |
| needs model support | 3 |
| no compiler | 3 |
| no harness | 32 |
| excluded | 6 |
| held | 32 |
| all OSS-Fuzz projects | 1,381 |
The 427 available projects have 2,148 harnesses with statements and 20,164 statements; 8,578 binaries are attached to this release or an earlier one, and 0 more are withheld. index/STATUS.md lists every project; index/*.tsv has the same data for scripts.
To prove or refute a statement, see docs/proving.md and CONTRIBUTING.md. A counterexample that shows a bug in a library goes to that library first (SECURITY.md). To enroll your own project, see theorem-labs/oss-verify.
vm_compute), and the axioms in toolchain/allowed-axioms.txt.elf-snapshot, and rocq-read-file 0.0.2, an OCaml plugin that reads the image's bytes into Rocq at compile time.oft check: the wrapper that it writes, and its reading of Print Assumptions (tools/oft/check.py).docs/trust.md says what each of these covers.
| path | contents |
|---|---|
proofs/<project>/<harness>/<statement>/ |
the proof of one statement, and its proof.yaml |
proofs/<project>/<harness>/provenance/ |
the build record of that harness's binaries |
proofs/<project>/<harness>/lib/ |
the lemmas that the proofs of that harness share |
projects/<project>/<harness>/ |
the facts (harness.yaml), the statements (Statements.v), the images (Images.v), the harness page, and, for most harnesses, a copy of the harness source (source/) |
theories/ |
the statement forms (Shapes.v), the image library, and the input-file format (Driver.v) |
index/ |
tables of every proof, project, harness, statement and binary |
toolchain/ |
the Dockerfiles of the checker and runner images, which release.yaml pins by digest, the allowed axioms, and the list of LPS files |
tools/oft/ |
the oft tool: fetch, generate, lint and check |
tests/ |
a generator of toy binaries, and controls that the checker must accept or refuse |
counterexamples/ |
inputs that make a binary break a statement, each with a control input |
analyses/ |
the checks that the harnesses make (harness-checks/), and every statement that is not open or proved (known-issues.md) |
LICENSES/ |
licence texts of proof files made from proofs under another licence |
docs/ |
the documentation |
CITATION.cff. A statement is cited as project/harness/statement@r<revision>, for example lzo/lzo_compress_target/plain_halts@r1. Until LPS is released, revisions are provisional (docs/versioning.md).
What we wrote is under the MIT licence (LICENSE): the statements, the tools, the documentation and our proofs. Proofs that we made from proofs that Anthropic licensed under the Apache License 2.0 or the MIT licence, at the recipient's option, keep those licences. The licence texts are LICENSES/anthropic-proofs-LICENSE and LICENSES/anthropic-proofs-LICENSE-MIT and the notices are LICENSES/anthropic-proofs-NOTICE; the build record of each such proof names these three files (docs/licensing.md). The binaries, the source archives and the harness copies keep their own licences (NOTICE). This project is not affiliated with or endorsed by Google or the OSS-Fuzz project.
OSS-Fuzz runs the fuzz targets of open-source projects to search for inputs that make them fail. This repository holds Rocq proofs that, for some of these fuzz targets, no such input exists within stated limits. Each proof is about compiled binaries, not source code.