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

A fuzz test throws random inputs at your code, trying to find one that causes a crash. OSS Verify turns your fuzz tests into theorems — "This entry point never crashes, on any input" — and proves them in Rocq. It’s as if the test was run forever. And indeed, once you prove a test like this, you never need to run it again.

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. For example, if your test is instrumented with ASan, then proving it doesn’t crash means proving that it never accesses memory improperly. We prove these properties on the binary level, which makes the theorems meaningful: They’re asserting things about the actual assembly instructions that people execute, not the source code that gets compiled.

What you get

A proof about your binary. The theorem is about the compiled program, not a model of the source: no crash, and no error caught by AddressSanitizer or UndefinedBehaviorSanitizer, for every input up to 64 MiB. What a proof covers gives the exact claim and its limits.
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. Findings and patches are generated by AI models, and we don’t promise that a person reviews them before we send them, so review every patch before you use it.
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. Our builder makes static riscv64 binaries, so the build needs porting. A coding agent can do most of it: point it at the repository’s AGENTS.md.

homepage: "https://libexample.org"
language: c
primary_contact: "[email protected]"
auto_ccs:
  - "[email protected]"
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 lines OSS-Fuzz uses: 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 start with widely used critical infrastructure. Smaller projects, measured in kilobytes 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.

How does attribution work?

It’s not required, but if you fix a bug that OSS Verify found, we’d appreciate a line in your commit message (or wherever you put credits) with the ID from our report, for example:

Found by Theorem's OSS Verify, as finding THM-2026-7K3QF9XA.

A finding ID is THM-, the year we first reported the finding, a hyphen, and 8 random characters from Crockford’s base32 alphabet (digits and capital letters, without I, L, O and U). The ID helps us track which findings were real and got fixed.

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 [email protected], or feel free to ask any lingering questions when making your enrollment PR.

Free formal verification for open source.