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 that the sanitizer never detects an error. OSS Verify is a Theorem program; a maintainer enrolls a project at theorem-labs/oss-verify.

60 entry points in 25 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.

• What is proved
• The theorem, in words
• What a proof does not say
• Versions
• Check a proof
• How the binaries are built
• Explore the proofs
• Statements for OSS-Fuzz fuzz targets
• What you have to trust
• Repository layout

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

• Every input means every process input that LPS accepts as valid: the arguments, the environment variables, the files (so the input file, its contents or its absence), standard input, and the rest of what a process receives. LPS leaves out a few inputs; for example, an argument after the program name may not contain / (docs/semantics.md).
• An error is a crash, an invalid memory access, an 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.
• Observable behaviours are the bytes that the process reads and writes on its standard streams and connections, in order, its exit status, and the final contents of its files.
• The memory budget of the plain build is 2 GiB in a statement about a build with ASan (ASan or ASan+UBSan), and 16 GiB in a statement about the UBSan build. The budget is a premise: an input on which the plain build needs more memory is not covered.
• System-call failures. Each statement says which system calls the environment may refuse without cause. In most of the proofs here, a memory request is refused only when the budget is spent or no address range is free.

So a proof rules out every error that the sanitizer build detects, on every input that the statement covers. If the harness checks a property with assert(), abort() or a trap, and the check is in the binary, the proof also shows that the property holds on every covered input (docs/exploring.md).

The Rocq definitions are in theories/Shapes.v. Each agreement form is proved equal to its LPS definition, strong_universal_error_free_T_budgets or one of its variants. docs/statements.md explains each form.

• It does not say that the library is correct. Errors that the sanitizers cannot detect are not excluded: for example, a wrong result or a memory leak.
• It is about the code that one entry point reaches, not about the whole library.
• It is about these binaries: static riscv64 programs, built with clang 20.1.8 against musl. It is not about the source code, and not about the x86-64 builds of OSS-Fuzz.
• It is true in LPS. Where LPS differs from Linux, the proof may not apply (docs/semantics.md).
• An agreement statement does not exclude a run that never ends. Only a halts statement does. No proof in this release proves a halts statement, so none of them rules out a run that never ends.

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.

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 -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 every committed proof on each push to main and 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: 138 are proved, some are known to be false, and proofs are added as they are found.

In this release: 20,164 statements: 138 proved, 0 known false (0 counterexamples, 0 false (witnessed)), 0 suspected false, 229 blocked by the model, 0 withheld (0 waiting for their source bundle, 0 not published yet), 19,797 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:

zlib/checksum_fuzzer/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 checksum_fuzzer asserts that CRC-32 combine law, per chunk (chunk size = data[0], min 1): crc32_combine_op(crc_so_far, crc32(0,chunk), crc32_combine_gen(chunk_len)) must equal crc32_z(crc_so_far, chunk); chunked crc32_z over the whole input (chunk size data[0]) must equal the one-shot crc32(0, data, len) (and 4 checks more), 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.

The 427 available projects have 2,148 harnesses with statements and 20,164 statements; 8,578 binaries are attached to this release 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.

• The Rocq kernel, with its bytecode machine (vm_compute), and the axioms in toolchain/allowed-axioms.txt.
• LPS, at the commit that release.yaml names (docs/semantics.md).
• The tools that turn an ELF file into an LPS memory image: LPS's 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.

CITATION.cff. A statement is cited as project/harness/statement@r<revision>, for example zlib/checksum_fuzzer/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.