Theorem

OSS Verify Agreement

Last updated: 22 October 2026

This OSS Verify Agreement (the “Agreement”) governs your ("Participant") enrollment of a project in OSS Verify (the “Service”), run by Theorem Labs, PBC ("Theorem"). Participant accepts this Agreement by ticking “I accept the OSS Verify terms” in an enrollment pull request to theorem-labs/oss-verify.

  1. Generally. Participant will enroll an open-source project that Theorem accepts for the Service (each, a “Project”). Theorem may accept a Project or withdraw its acceptance, in its sole discretion. Theorem will try to formally verify correctness and safety properties of the Project’s software, and may send Participant the resulting proofs. The documentation of theorem-labs/oss-verify describes what the Service currently proves and the limits of each claim; Theorem may change both. If a bug stops a proof, Theorem will send Participant a report of it (each, a “Report”), intended to include a description of the bug, a reproducer and a proposed patch. Verification can take a long time, and Theorem may stop work on any part of a Project without finishing a proof. The Service, each Report and each proof are provided “as is”. Participant uses them at its own risk.

  2. Requirements.

    a. Participation. By enrolling a Project, Participant represents that (a) Participant is a core maintainer of the Project, or is authorized by its core maintainers to enroll it, and (b) if Participant maintains the Project as an employee of an organization that serves as its maintainer, Participant has that organization’s permission to enroll it. The contact address Participant gives at enrollment must belong to a Project maintainer. Theorem may verify Participant’s authorization, including by contacting the Project’s maintainers through other channels, and may remove a Project whose authorization it cannot verify.

    b. Project. The Project must be open source, under an OSI-approved licence that lets Theorem build it and redistribute the binaries it builds and the source it builds them from. Theorem accepts projects case by case, along the lines OSS-Fuzz uses: how established and actively maintained the Project is, how widely it is used, and how much of it handles untrusted input or sits underneath other software. Theorem may decline a Project that has already been submitted.

  3. Permitted Use of Reports. Participant may use Reports only to identify, assess and fix bugs in the Project and its dependencies (the “Permitted Use”). Participant may share Reports with authorized maintainers of the Project. Participant may not use a Report for any other purpose, including to attack, exploit or gain access to any third-party computer system or code repository.

  4. Disclaimer.

    a. Nature of Reports. Each Report is generated by artificial intelligence models, and Theorem does not promise that a person reviews a Report before it is sent. Reports may be incomplete and inaccurate. Without limiting the foregoing, a Report may fail to identify bugs, may describe as a bug something that is not one, may misjudge how serious an issue is, and may propose a patch that is incomplete or that impairs or breaks functionality.

    b. Disclaimer. THE SERVICE, ALL REPORTS, ALL PROPOSED PATCHES AND ALL PROOFS ARE PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND. TO THE FULLEST EXTENT PERMITTED BY APPLICABLE LAW, THEOREM DISCLAIMS ALL WARRANTIES, WHETHER EXPRESS, IMPLIED OR STATUTORY, INCLUDING ANY WARRANTIES OF ACCURACY, COMPLETENESS, MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, TITLE AND NON-INFRINGEMENT, AND ANY WARRANTIES ARISING FROM COURSE OF DEALING OR USAGE OF TRADE. WITHOUT LIMITING THE FOREGOING, THEOREM DOES NOT WARRANT THAT ANY REPORT WILL IDENTIFY ALL BUGS, THAT ANY PROPOSED PATCH WILL BE COMPLETE, WILL FUNCTION AS INTENDED OR WILL NOT IMPAIR FUNCTIONALITY, OR THAT THEOREM WILL PRODUCE A PROOF FOR ANY TARGET. NO ADVICE OR INFORMATION, WHETHER ORAL OR WRITTEN, OBTAINED FROM THEOREM OR THROUGH THE SERVICE WILL CREATE ANY WARRANTY NOT EXPRESSLY STATED IN THIS AGREEMENT.

    c. Participant’s Responsibility. Participant is responsible for reviewing each Report, and any patch proposed in it, before making changes to the Project in reliance on a Report or sharing that Report.

  5. Security and Disclosure. Reports may include sensitive information, including descriptions of unfixed bugs. Participant will take reasonable steps to keep them confidential and secure until the bug is fixed or publicly disclosed. Theorem sends Reports privately, to the contacts the Project gives at enrollment, encrypted if the Project asks for it. Theorem sets no disclosure deadline and does not publish findings. A bug Theorem finds in one of the Project’s dependencies is reported to that dependency’s maintainers, not to Participant.

  6. Proofs and Publication. Theorem sends Participant the proofs for the Project. Theorem may also publish the proofs, their theorem statements, and the binaries and source archives it built, in theorem-labs/oss-verify-proofs, as the Project’s publish setting allows: as they progress, after the fixes for the bugs Theorem reported are public (the default), or never. Until a finding is public, Theorem holds back every statement it affects, and nothing Theorem publishes describes it. If a proof needed a patch to the Project’s code, Theorem publishes it only once the finding that patch fixes is public, and lists the patch with its text, a summary and its upstream state. Published proofs carry the licences stated in that repository.

  7. Contributions. The files Participant adds to theorem-labs/oss-verify (project.yaml, Dockerfile, build.sh, patch_style.md and the like) are contributions under the Apache License 2.0, as the repository’s CONTRIBUTING.md says. There is no separate contributor licence agreement.

  8. No fees. The Service is provided at no cost.

  9. Limitation of Liability. To the fullest extent permitted by law, Theorem is not liable for any use of a Report, a proposed patch, a proof or the Service, including any use outside the Permitted Use, or for any loss arising from reliance on a Report, a proposed patch or a proof. Theorem’s total liability arising from this Agreement or the Service will not exceed $1,000.

  10. Term. This Agreement remains in effect while the Project is enrolled. Participant may pause or end enrollment at any time, as the enrollment instructions describe. Theorem may modify, suspend or end the Service, or any enrollment, at any time and for any reason. Sections 3, 4, 5 and 9 survive after this Agreement ends.

  11. Governing Law. This Agreement is governed by, and will be construed in accordance with, the laws of the State of California, without giving effect to conflict-of-law principles. Any dispute arising out of or relating to this Agreement or the Service will be resolved exclusively in the state or federal courts located in California, and Participant and Theorem submit to the personal jurisdiction of those courts.