Intrepyd
Intrepyd is a python module that provides a simulator and model checkers in form of a rich API, to allow the rapid prototyping of formal methods algorithms for the rigorous analysis of circuits, specifications and models.
- Circuits of inputs, latches and combinational nets over booleans, bounded and unbounded integers, reals and floats.
- A simulator, and four engines: bounded model checking, k-induction, backward reachability and IC3/PDR, whose proofs are checked; a portfolio runs them all in parallel, and answers with the first of them.
- Front-ends for Lustre and IEC 61131-3 Structured Text (PLCopen XML).
- Traces as pandas data frames.
pip install intrepyd
Wheels are available for Linux (x86-64, glibc 2.28 or newer) and Windows (x86-64), for python 3.11 or newer. Each one carries the intrepid model checking library for its platform, so there is nothing else to install.
import intrepyd as ip
from intrepyd.engine import EngineResult
ctx = ip.Context()
int8_t = ctx.mk_int8_type()
c = ctx.mk_latch('c', int8_t)
ctx.set_latch_init_next(c, ctx.mk_number('0', int8_t),
ctx.mk_add(c, ctx.mk_number('1', int8_t)))
bmc = ctx.mk_bmc()
bmc.add_target(ctx.mk_eq(c, ctx.mk_number('5', int8_t)))
bmc.set_current_depth(5)
assert bmc.reach_targets() == EngineResult.REACHABLE
The documentation, the source and the issue tracker are on GitHub; a collection of experiences using Intrepyd is in the Formal Methods Little Corner.
Intrepyd is free for noncommercial purposes, such as personal use and use
by universities and public research organizations, under the PolyForm
Noncommercial License 1.0.0. Any other use, in particular by companies for a
commercial purpose, requires a commercial license: write to
roberto.bruttomesso@gmail.com. Versions up to 0.14.0 were released under the
BSD 3-Clause license. The intrepid library bundled in the wheels is
proprietary, and its license, installed as intrepyd/LICENSE.intrepid,
allows it to be used and redistributed, unmodified, as part of intrepyd,
within the same terms. It links the Z3 SMT solver, released under the MIT
license.
1 maintainer
Metadata
1 maintainer
Release files for intrepyd 0.16.0
For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.
Built distributions (wheels)
| File | Interpreter | ABI | Platform | Reset |
|---|---|---|---|---|
| intrepyd-0.16.0-py3-none-win_amd64.whl | Python 3 | none | Windows x86-64 | Details |
| intrepyd-0.16.0-py3-none-manylinux_2_28_x86_64.whl | Python 3 | none | Linux glibc 2.28+ x86-64 | Details |
Total release size: 21.6 MB
Release files / intrepyd-0.16.0-py3-none-win_amd64.whl
| Download URL | intrepyd-0.16.0-py3-none-win_amd64.whl |
|---|---|
| Size | 7.3 MB |
| Tags | Python 3 Windows x86-64 |
|
SHA-256 checksum How to use checksums |
f0d7b8467940a34cab00949e7fecd09696aa4f5ec9cbf1adb6275cf246ace5bc
|
|
BLAKE2b-256 checksum How to use checksums |
e2a7fa4a0811d53c5391c0ee426924ba40d42de788e0c0c597cd8d008720ca64
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
Yes |
| Uploaded via |
twine/7.0.0 CPython/3.13.14
|
Provenance
Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.
PyPI Publish Attestation
PyPI verified that this artifact, at this checksum, originated from the publisher listed below.
Signed by GitHub Actions, verified by PyPI on Oct 9, 2026.
Transparency logRelease files / intrepyd-0.16.0-py3-none-manylinux_2_28_x86_64.whl
| Download URL | intrepyd-0.16.0-py3-none-manylinux_2_28_x86_64.whl |
|---|---|
| Size | 14.3 MB |
| Tags | Linux glibc 2.28+ x86-64 Python 3 |
|
SHA-256 checksum How to use checksums |
d1f535e3e55a6d3f2c2d6a4ec23b55629b09a9d2baee905f4d8af73ee26828e6
|
|
BLAKE2b-256 checksum How to use checksums |
82813000ba8b1339852b883f29d11e6a21e8560169023426b54f0e7b43da0b74
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
Yes |
| Uploaded via |
twine/7.0.0 CPython/3.13.14
|
Provenance
Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.
PyPI Publish Attestation
PyPI verified that this artifact, at this checksum, originated from the publisher listed below.
Signed by GitHub Actions, verified by PyPI on Oct 9, 2026.
Transparency log
