OSS Verify | Theorem

Our AI-driven approach to formal verification lets us verify arbitrary properties at the binary level. Now we're offering it to qualifying open source projects for free.

What we do

OSS Verify is an initiative that takes open source software and proves arbitrary properties about that code in a proof assistant, guaranteeing that your program is secure.

Previously, bug discovery relied on methods like fuzz testing, which throws random inputs at your code, trying to find one that causes a crash. With OSS Verify, you can now receive a proof that your fuzz test will never find another bug, no matter how long it runs.

Consider proving a theorem such as, “This entry point never crashes, on any input”. This technique can be used to indirectly prove all kinds of useful properties. All you have to do is write a test that crashes for the right reason.

Most formal verification works by translating source code into Rocq or Lean, then proving things about the translation. We take things a step further: Our proofs target the actual assembly instructions that make up a compiled binary. These proofs are much larger (and much harder to complete), but because they describe reality more accurately, they give you a much stronger guarantee.

What you receive

A proof about your binary. The theorem is about the compiled fuzz test, not its source code. It states that no input up to 64 MiB can cause a crash, either by violating a fuzz test or triggering ASan. See What a Proof Covers for details on the exact claim.
Checked by a machine. The proof is checked by the Rocq kernel. You don’t need to trust it; you only need to trust Rocq.
The bugs we find on the way. Naturally, it’s impossible to prove something that isn’t true. If there’s a bug that would cause your test to crash, we’ll find it and report it to you privately.
No cost. Qualifying open source projects pay nothing.

How to enroll

Enrollment works like OSS-Fuzz. Open a pull request against theorem-labs/oss-verify that adds a directory projects/<your-project>/ with three files:

project.yaml, which says who you are (below).
Dockerfile, which sets up the build environment and checks out your code.
build.sh, which builds your fuzz targets into $OUT.

If your project is already in OSS-Fuzz, start from those files. OSS Verify requires static riscv64 binaries, so your build may need porting; we recommend pointing a coding agent at our repository’s AGENTS.md.

homepage: "https://libexample.org"
language: c
primary_contact: "maintainer@example.org"
auto_ccs:
  - "security@example.org"
repo: "https://github.com/example/libexample#v1.2.3"
fuzz_targets:
  - parse_fuzzer

Field
`repo`	required	The git repository to build, as an https URL. Add `#branch` or `#tag` to follow one, or `#<commit>` to fix one. It doesn’t have to be on GitHub.
`primary_contact`	required	The email address that receives reports.
`language`	required	The language of your fuzz targets, as OSS-Fuzz names it. The repository’s project.yaml reference lists the languages we support.
`homepage`	optional	The project’s homepage.
`auto_ccs`	optional	More addresses to copy on every report.
`fuzz_targets`	optional	The targets in `$OUT` to verify, by name. Leave it out to verify them all.
`sanitizers`	optional	The sanitizer builds besides the plain one: `address`, `undefined`, or both (the default).
`patch_style`	optional	Where your `patch_style.md` is: which findings and patches you want, and how.
`publish`	optional	When we publish the proofs: as they progress, after the fixes are public (the default), or never.
`pgp`	optional	A public key to encrypt reports with. Reports then go to `primary_contact` only.
`disabled`	optional	Set to `true` to pause.

The repository’s project.yaml reference describes every field.

FAQ

What projects are eligible?

We review each project individually, along the same lines as OSS-Fuzz: how established and actively maintained it is, how widely it’s used, whether it’s under an OSI-approved license, and how much of it sits on a security boundary or underneath other software (parsers, compression, cryptography, image and font decoders, protocol implementations). In addition, we check that contact email in the project.yaml belongs to a project maintainer. Only a project’s core maintainers can enroll it.

We will prioritize widely used critical infrastructure. Smaller projects (<1MB of binary .text) are likely to be verified sooner.

What will maintainers receive?

For each fuzz target, you will receive a proof (in Rocq) that the target does not crash regardless of input. Typically, this proof will indirectly prove other important properties, like memory safety. If we encounter bugs during the proof effort, we will privately disclose them to maintainers via email (encrypted with pgp if specified). Findings and patches are generated by AI models, and we don’t promise that a person reviews them before we send them. We set no disclosure deadline, and we don’t publish findings. Bugs found in a project’s dependencies are reported to the maintainers of those dependencies, not to the maintainer of the project.

When will my project receive a report?

These proofs can take multiple days to produce, so don’t expect to hear back immediately. After the initial proof is completed, we’ll update it on a regular basis as needed.

Can I pause or opt out?

Yes. To pause, open a pull request that sets disabled: true in your project.yaml. To leave, open one that deletes your project’s directory.

What if my question isn’t listed here?

Write to oss-verify@theorem.dev, or feel free to ask any lingering questions when making your enrollment PR.

Free formal verification for open source.