Theorem does research and engineering in formal verification and AI.
OSS Verify proves that an open-source project's fuzz targets can't crash on any input up to 64 MiB. The theorems are about the compiled RISC-V binary, not the source code, and the Rocq kernel checks every proof. Qualifying projects pay nothing.
| Repository | What it holds |
|---|---|
| oss-verify | Enrollment and build instructions. To enroll, open a pull request that adds your project. |
| oss-verify-proofs | Theorem statements for 2,148 fuzz targets in 427 OSS-Fuzz projects, proofs for 60 of them, and the binaries they are about |
| rocq-linux-process-semantics | A Rocq model of a Linux process that runs a RISC-V binary. The statements are stated over it. |
| static-asan | The static AddressSanitizer for musl that the sanitizer builds use |
Questions: oss-verify@theorem.dev
