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.
- 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.9 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 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 freely,
unmodified, as part of intrepyd. It links the Z3 SMT solver, released under
the MIT license.
1 maintainer
Metadata
1 maintainer
Release files for intrepyd 0.13.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.13.0-py3-none-win_amd64.whl | Python 3 | none | Windows x86-64 | Details |
| intrepyd-0.13.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.13.0-py3-none-win_amd64.whl
| Download URL | intrepyd-0.13.0-py3-none-win_amd64.whl |
|---|---|
| Size | 7.3 MB |
| Tags | Python 3 Windows x86-64 |
|
SHA-256 checksum How to use checksums |
ccd3f446fd7631339141219c8624b9402d69146cef6d98a6221799ccc14a7313
|
|
BLAKE2b-256 checksum How to use checksums |
3fd707d4024fb2e98229b74f16718add90312c5cde77cab038622776fef14ba8
|
| 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 4, 2026.
Transparency logRelease files / intrepyd-0.13.0-py3-none-manylinux_2_28_x86_64.whl
| Download URL | intrepyd-0.13.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 |
82cc3194f4c099a9f093268d0a9a838f67d3e4512114a7fea02299998c269b30
|
|
BLAKE2b-256 checksum How to use checksums |
d696162691c2d4ce9c9b54a2615aa4e6b406f39dd5dded7383af8b26b31778f8
|
| 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 4, 2026.
Transparency log
