The engines' license¶

From intrepid 1.7, the library inside intrepyd, the engines (BMC and k-induction, backward reachability, PDR, and the portfolio that runs them) run under a license only. Building circuits, simulating them, exporting them and generating code need none.

The end-user license agreement¶

From intrepyd 1.0, the engines also need the end-user license agreement accepted: python -m intrepyd.eula accept, or INTREPID_ACCEPT_EULA=2026-10 in a script or a container. The editors ask for it before their first verification. For now an engine made without it warns, once a process; a next release will refuse it.

Noncommercial use¶

Each wheel of intrepyd on PyPI carries a noncommercial license, next to the library, valid for a year from the day of its release: pip install intrepyd is all the noncommercial use that the license of intrepyd allows needs. When it expires, a newer release of intrepyd carries a new one.

Commercial use¶

A company uses the commercial license it was given, a JSON file, in one of these ways. intrepid looks for a license in this order:

given by the program:

import intrepyd.license

intrepyd.license.set_license_file("/path/to/license.json")
# or intrepyd.license.set_license(text), with the license's JSON itself

the INTREPID_LICENSE environment variable: the path of the license's file, or its JSON itself (convenient for a CI secret, or a container);
the file ~/.intrepid/license.json (%APPDATA%\intrepid\license.json on Windows);
the noncommercial license the wheel carries.

One given by the program is the one used. Otherwise the first valid one is, and those before it are passed over: an expired license, or one for another build of intrepid, does not hide the wheel's. license_info() lists them under skipped, each with where it is and why it was passed over.

A commercial license keeps working, after it expires, for the releases of intrepid made before then: a later release needs it renewed.

What intrepyd says¶

import intrepyd.license

print(intrepyd.license.license_info())

gives the license the engines run under: its id, licensee, kind, issue and expiry dates, whether it is valid (and, if not, the error), where it was found (source), and the release date of the library. Without a valid license, making an engine raises RuntimeError saying why: no license found (and where it was looked for), a signature that is not valid, a license that expired, or one that does not cover this release.

The processes the portfolio starts run under the same license: set_license and set_license_file put it in INTREPID_LICENSE, which they inherit.