Skip to content
@theorem-labs

Theorem

Formal verification and AI. OSS Verify: free machine-checked proofs for open-source fuzz targets.
README.md

Verify all software.

Theorem does research and engineering in formal verification and AI.

OSS Verify: free formal verification for open source

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.

Enroll your project

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

Pinned Loading

  1. oss-verify-proofs oss-verify-proofs Public

    Theorem statements about OSS-Fuzz fuzz targets as compiled RISC-V binaries, and machine-checked Rocq proofs of them

    Rocq Prover 200 16

  2. rocq-linux-process-semantics rocq-linux-process-semantics Public

    A Rocq model of a Linux process that runs a RISC-V binary

    Rocq Prover 57 12

  3. oss-verify oss-verify Public

    OSS Verify: enrollment and build instructions for formally verifying open-source fuzz targets

    Python 105 18

Repositories

Showing 10 of 34 repositories
View all repositories