OSS Verify

OSS Verify is a Theorem program that verifies open-source software. We prove theorems about the compiled fuzz targets of a project. For example, we prove that no input makes a fuzz target crash, hang or fail a sanitizer check. This page tells a maintainer how to enroll a project. A coding agent starts at AGENTS.md.

Who can enroll

We accept an established open-source project (theorem.dev/oss-verify tells how we choose projects). A project must also obey these conditions:

1. The person who enrolls the project is a core maintainer of it.
2. The project has a licence that the Open Source Initiative approves.
3. The project has a public git repository, which we get anonymously over https. One project directory names one repository.
4. The project has at least one fuzz target: its own, its OSS-Fuzz fuzz targets, or new ones.
5. Our builder can build the project. The language table tells which languages it builds today.
6. The enrollment names, in primary_contact, the one address that gets findings.

A project of any size can enroll. Because of our capacity, we are most likely to respond quickly to a project in C whose plain binaries (<target>.plain) are statically linked and have less than 1 MB of code: the larger of their .text section, the size that tools/check shows, and their executable segments (which can hold read-only data too). If your organisation wants to help us increase that capacity, so that we can take on more projects now, write to oss-verify@theorem.dev. We are interested in corporate partners and sponsorship.

We seeded some projects already, and a maintainer can adopt one (docs/project-yaml.md).

Enroll with a coding agent

Copy and paste this prompt into your coding agent (Claude Code, Codex, Cursor, etc.). Start the agent in a checkout of your project.

Enroll this project in OSS Verify by following the instructions here:
https://raw.githubusercontent.com/theorem-labs/oss-verify/refs/heads/main/AGENTS.md

The agent asks you what "correct" means for your code, and which findings and patches you want. Then it makes projects/<name>/ and runs the checks, on a machine that has what Enroll a project lists. You push its branch to your fork of this repository, and you open the pull request.

WARNING: The agent runs tools/check. tools/check builds the project's Dockerfile with network access. Use the agent only on a project that you trust (SECURITY.md).

Enroll a project

WARNING: tools/check builds the project's Dockerfile with network access. Use it only on a project that you trust (SECURITY.md).

You need a Linux x86-64 machine with Docker and its buildx plugin, git, and Python 3 with PyYAML (on Ubuntu, apt install docker.io docker-buildx python3-yaml), and about 10 GB of free disk. The first run of tools/check downloads a toolchain image of about 1.1 GB, which unpacks to about 5 GB.

1. Fork this repository.
2. Make projects/<name>/ from templates/: project.yaml (docs/project-yaml.md), a Dockerfile and a build.sh (docs/build-contract.md).
3. Optional: write a patch_style.md. Tell us which findings, reports and patches you want, and how they must look.
4. Run tools/validate.py projects/<name>. Correct each problem that it shows.
5. Run tools/check --no-shell --twice <name>. Make sure that it builds each fuzz target, and that the second build has the same bytes. Without --no-shell, tools/check opens a shell in the build image when it finishes.
6. Open a pull request. Complete its checklist.

When the checks pass

When every required check of your pull request passes, and each plain binary has at most 1 MB of code, we start to write the theorem statements for the commit that the pull request is at. The code of a binary is the larger of its .text section and its executable segments, which can hold read-only data too. If a plain binary has more than 1 MB of code, or a size that we cannot read, the pull request gets the label size-review, and we decide what to do. Python and Go projects are paused for now (our tools do not write theorem statements for Go yet): such a pull request gets the label language-paused. A project name with a dot, which the names in our statements repository cannot have, or a name that we already use there for another project, gets the label name-review. If GitHub does not show that you maintain the repository that repo names by a role there (owner, member, collaborator, public member of its organisation) or by merges of its recent pull requests, together with your commits of the last 12 months or those merges, or that repository is not on GitHub, the pull request gets the label maintainer-review, and we decide what to do. If our review of the commit finds that a fuzz target can end the run itself, catch every error or handle a signal (check F2 of review.md), or is not fit for a proof (check F7), the pull request gets the label review-blocking. If the review could not decide those two checks, it gets the label review-pending. With either label, no statements start by themselves. A person at Theorem decides each review-pending pull request: they ask for a new review, or start the statements by hand. When the statements start, we build the project again and check its binaries again. If a check of the binaries fails in that build (the ELF and instructions check, or the quiet and loud check), the pull request gets the label checks-failing, not size-review, whatever the size of that build's binaries, and the statements wait for a commit whose binaries pass these checks. The label comes off when a later commit's binaries pass them. A new commit on the pull request starts this again, and so does an edit of its title or description; a commit whose statements we already wrote is not written again. A pull request that changes a project that is already enrolled starts it too.

For these statements, we build the fuzz targets two times, and pin the SHA-256 of each binary in a lock.

After we merge

We merge an enrollment when we intend to prove the project. If we merge your pull request before its theorem statements started, the merge starts them.

1. We prove the theorem statements (docs/what-gets-proven.md). Our tools do not write theorem statements for Go projects yet (docs/project-yaml.md).
2. We send each finding privately to primary_contact, with a patch when we have one. There is no disclosure deadline, and we do not publish findings.
3. We publish the proofs when the publish field tells us to.

Findings and patches are generated by AI models, and they can be wrong or incomplete. We do not promise that a person reviews them before we send them. Review every patch before you use it. We follow your project's policy on AI-generated contributions.

Pause or leave

To pause the project, set disabled: true in project.yaml. To leave, remove projects/<name>/. Make each change in a pull request.

Learn more

The OSS Verify FAQ answers questions. To send feedback about a finding or a patch, reply to its report, or write to oss-verify@theorem.dev. SECURITY.md tells how to report a vulnerability in this repository. Use of OSS Verify is subject to the OSS Verify terms. Most pull requests here enroll a project; CONTRIBUTING.md tells how other changes are reviewed.

Licence

This repository is under the Apache License 2.0 (LICENSE). The driver that $LIB_FUZZING_ENGINE links into a fuzz target, infra/base-builder/driver/, is under MIT OR Apache-2.0 (LICENSES/MIT.txt), so that a program under version 2 of the GNU GPL can be linked with it. NOTICE says which files and lines have another licence, and why.