tlakit

CI

A Python and notebook client for the TLA+ toolchain.

TLA+ has good tools — TLC, SANY, the TLA+ Debugger, the animation modules. None of them are reachable from Python, and none of them compose with a notebook. tlakit is the missing client. It does not reimplement any of them.

import tlakit

spec = tlakit.load("Microwave.tla")
result = spec.check(invariants=["Safety"])

if not result.ok:
    print(result.outcome)                       # Outcome.INVARIANT_VIOLATION
    print(result.trace.delta(3))                # frozenset({'radiation'})
    result.trace.to_dataframe(flatten=True)     # nested records as columns

Sweep a constant and get the smallest configuration that breaks:

sweep = spec.sweep({"Servers": [3, 4, 5]}, invariants=["Inv"],
                   workers=3, heap="2G")
sweep.first_failure().constants     # {'Servers': 4}
sweep.to_dataframe()                # one row per configuration

As a Jupyter kernel

pip install "tlakit[kernel]"
python -m tlakit.kernel.install

Then pick TLA⁺ (tlakit) from Jupyter's kernel list and write TLA+ directly — no magics, no Python wrapper:

---- MODULE Microwave ----
EXTENDS Naturals
VARIABLES door, radiation
...
====

SPECIFICATION Spec
INVARIANT Safety

Python still works in the same notebook, which is the point of building on IPython rather than replacing it:

result.trace.to_dataframe()

Or as magics in an ordinary Python kernel

%load_ext tlakit

%%tla Microwave
---- MODULE Microwave ----
...
====

%%tlc Microwave
SPECIFICATION Spec
INVARIANT Safety

Status

M1 is complete: CliRunner, normalized results, %%tla / %%tlc magics, and static HTML rendering of counterexamples and diagnostics. See docs/superpowers/specs/ for the design and docs/superpowers/plans/ for the implementation plan.

Requirements

  • Python 3.10+
  • Java
  • TLA+ tools v1.8.0 or newer — tlakit runs TLC with -dumpTrace json; v1.7.4 (TLC 2.19) does not have that option

Fetch the pinned, checksummed tools:

python -m tlakit.install

Or point tlakit at jars you already have with TLAKIT_TLA2TOOLS=/path/to/tla2tools.jar. TLAKIT_COMMUNITY_MODULES optionally locates CommunityModules-deps.jar, which SVG.tla and Json.tla need.

License

MIT

Project links

Data verified by PyPI on Aug 8, 2026
Data provided by the project maintainers, verified at the time the release was uploaded to PyPI.

Key dates

PyPI data
Data sourced directly from PyPI's database.
  • Released:
Newer release available (0.1.1)

1 maintainer

PyPI data
Data sourced directly from PyPI's database.
Avatar for EricSpencer00 from gravatar.com EricSpencer00

Credits

Author: Eric Spencer

GitHub Statistics

Data verified by PyPI on Aug 8, 2026
The GitHub source repository was provided by the project maintainers and verified by PyPI at the time of upload. Stars, forks, and open issues/PRs are derived from that repository and have not been independently verified.

License

MIT License (MIT)

Requires

Python >=3.10

Provides Extra

dev kernel notebook serve

Tags

formal-methods jupyter model-checking tla+ tlaplus tlc

Classifiers

Report project as malware

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

tlakit-0.0.1.tar.gz (121.0 kB view details)

Uploaded Source

Built Distribution

If you're not sure about the file name format, learn more about wheel file names.

tlakit-0.0.1-py3-none-any.whl (64.8 kB view details)

Uploaded Python 3

File details

Details for the file tlakit-0.0.1.tar.gz.

File metadata

  • Download URL: tlakit-0.0.1.tar.gz
  • Upload date:
  • Size: 121.0 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? Yes
  • Uploaded via: twine/7.0.0 CPython/3.13.14

File hashes

Hashes for tlakit-0.0.1.tar.gz
Algorithm Hash digest
SHA256 49864b0c62934ee52848ff8ecc89bc495685c79d261a01eeb4bd547e442808fc
MD5 663eb7edf4a66f7f552b476d1ea5e693
BLAKE2b-256 8a38d241a2daf8f776178d35c40b5bc41014f639350e5209fad763f61c0f307d

See more details on using hashes here.

Provenance

The following attestation bundles were made for tlakit-0.0.1.tar.gz:

Publisher: release.yml on LUC-AI4FM/tlakit

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file tlakit-0.0.1-py3-none-any.whl.

File metadata

  • Download URL: tlakit-0.0.1-py3-none-any.whl
  • Upload date:
  • Size: 64.8 kB
  • Tags: Python 3
  • Uploaded using Trusted Publishing? Yes
  • Uploaded via: twine/7.0.0 CPython/3.13.14

File hashes

Hashes for tlakit-0.0.1-py3-none-any.whl
Algorithm Hash digest
SHA256 3f1cdf85090005e3986fa8ccd9d51a2cba3c92b799ea34bd497310f57f1dd459
MD5 d90293366bc87c464813d93c7cb19fcc
BLAKE2b-256 b01e2d2a24a733e8ca397b331dc0db03fe818bf41e49d556c475db1e64af2a4d

See more details on using hashes here.

Provenance

The following attestation bundles were made for tlakit-0.0.1-py3-none-any.whl:

Publisher: release.yml on LUC-AI4FM/tlakit

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

Supported by

AWS Cloud computing and Security Sponsor Datadog Monitoring Depot Continuous Integration Fastly CDN Google Download Analytics Sentry Error logging StatusPage Status page