Metadata-Version: 2.4
Name: tlakit
Version: 0.1.1
Summary: A Python and notebook client for the TLA+ toolchain
Project-URL: Homepage, https://github.com/LUC-AI4FM/tlakit
Project-URL: Repository, https://github.com/LUC-AI4FM/tlakit
Project-URL: Issues, https://github.com/LUC-AI4FM/tlakit/issues
Project-URL: Try it in a browser, https://tlakit.pages.dev
Author: Eric Spencer
License: MIT
Keywords: formal-methods,jupyter,model-checking,tla+,tlaplus,tlc
Classifier: Development Status :: 3 - Alpha
Classifier: Framework :: Jupyter
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Education
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Topic :: Scientific/Engineering
Classifier: Topic :: Software Development :: Testing
Classifier: Typing :: Typed
Requires-Python: >=3.10
Requires-Dist: platformdirs>=4.0
Provides-Extra: dev
Requires-Dist: anywidget>=0.9; extra == 'dev'
Requires-Dist: fastapi>=0.110; extra == 'dev'
Requires-Dist: httpx>=0.27; extra == 'dev'
Requires-Dist: ipykernel>=6.0; extra == 'dev'
Requires-Dist: jupyter-client>=7.0; extra == 'dev'
Requires-Dist: nbclient>=0.9; extra == 'dev'
Requires-Dist: nbmake>=1.5; extra == 'dev'
Requires-Dist: pytest-timeout>=2.0; extra == 'dev'
Requires-Dist: pytest>=8.0; extra == 'dev'
Requires-Dist: python-multipart>=0.0.9; extra == 'dev'
Requires-Dist: traitlets>=5.0; extra == 'dev'
Requires-Dist: uvicorn>=0.27; extra == 'dev'
Provides-Extra: docs
Requires-Dist: mkdocs-material<10,>=9.5; extra == 'docs'
Requires-Dist: mkdocs<2,>=1.6; extra == 'docs'
Requires-Dist: mkdocstrings[python]<1,>=0.24; extra == 'docs'
Provides-Extra: kernel
Requires-Dist: ipykernel>=6.0; extra == 'kernel'
Requires-Dist: jupyter-client>=7.0; extra == 'kernel'
Provides-Extra: notebook
Requires-Dist: ipython>=8.0; extra == 'notebook'
Provides-Extra: serve
Requires-Dist: fastapi>=0.110; extra == 'serve'
Requires-Dist: pydantic>=2.0; extra == 'serve'
Requires-Dist: python-multipart>=0.0.9; extra == 'serve'
Requires-Dist: uvicorn>=0.27; extra == 'serve'
Provides-Extra: widget
Requires-Dist: anywidget>=0.9; extra == 'widget'
Requires-Dist: traitlets>=5.0; extra == 'widget'
Description-Content-Type: text/markdown

# tlakit

[![CI](https://github.com/LUC-AI4FM/tlakit/actions/workflows/ci.yml/badge.svg)](https://github.com/LUC-AI4FM/tlakit/actions/workflows/ci.yml)

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.

```python
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:

```python
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

```bash
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:

```tla
---- 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:

```python
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
```

## Or from a shell, with no Python at all

```bash
tlakit check Counter.tla                      # uses Counter.cfg if it is there
tlakit check Counter.tla --invariant Inv      # or build the config from flags
tlakit check Counter.tla --no-deadlock-check  # a spec that is meant to finish
tlakit parse Counter.tla                      # SANY only, no search
```

Exit codes make it composable, and they distinguish two things a shell
otherwise cannot:

| Code | Meaning |
| --- | --- |
| `0` | the spec checked out |
| `1` | the run succeeded and found something wrong with the spec |
| `2` | the run did not happen — bad flags, missing file, no JVM |

So `tlakit check Spec.tla && deploy` does not deploy on a violated invariant,
and a CI job can still tell a real failure from a typo in a path.

`--no-deadlock-check` is worth knowing about early: a specification meant to
*finish* has no successor state at the end, and TLC reports that as
`DEADLOCK` — correctly, since it cannot know termination was intended.

## Related work

tlakit is the next evolution of Läufer and Thiruvathukal's *TLA+ for All: Model
Checking in a Python Notebook* (TLA+ Community Event, 2025), which established
that a Python notebook driving `tla2tools.jar` is a good way to teach and use
TLA+. That result is the starting point here, not a competitor.

What tlakit adds is a difference in kind rather than in polish: **TLA+ is the
cell language.** `tlakit.kernel` is a Jupyter kernel, so a notebook is a TLA+
artifact rather than a Python file holding TLA+ strings — TLA+ `language_info`,
module cells that need no magic, and completion and hover answered *in TLA+*,
from operators defined in the session and from the `.tla` files inside
`tla2tools.jar` itself. A Python kernel cannot answer those: asked what `Su`
completes to, the only honest answer it has is a Python one.

The kernel is deliberately thin. All the behaviour lives in `tlakit.api` and
`tlakit.magics`; the kernel subclasses `IPythonKernel` and adds routing,
completion, and inspection on top. The previous from-scratch TLA+ kernel,
[kelvich/tlaplus_jupyter](https://github.com/kelvich/tlaplus_jupyter), died of
kernel and packaging maintenance rather than of anything TLA+-related — so the
one thing this kernel must not do is own the protocol. If it rots, the magics
keep working.

## Status

0.1.1 is the first release. Everything shown above is implemented: the Python
API and `sweep`, the `tlakit` command, the `%%tla` / `%%tlc` magics, the Jupyter
kernel, and HTML rendering of counterexamples and diagnostics.

Every push to `main` also publishes a dev build to
[TestPyPI](https://test.pypi.org/project/tlakit/), so a fix is installable
before it is released:

```bash
pip install --index-url https://test.pypi.org/simple/ \
            --extra-index-url https://pypi.org/simple/ --pre tlakit
```

## 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:

```bash
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.

## Documentation

[`docs/reference.md`](docs/reference.md) is the reference: every environment
variable, every magic and its arguments, and a map of the public names.
[`docs/api.md`](docs/api.md) generates the API from the docstrings.

Build the site locally with:

```bash
pip install -e ".[docs]" && mkdocs serve
```

## License

MIT
