Metadata-Version: 2.5
Name: levain-cli
Version: 0.1.0
Summary: Levain recipe toolchain: PlusCal validator, TLC model checking, and GraphState codegen for agent recipes
License-Expression: Apache-2.0
License-File: LICENSE
Requires-Python: >=3.12
Requires-Dist: httpx==0.28.1
Requires-Dist: pydantic==2.13.4
Requires-Dist: tree-sitter-tlaplus==1.5.0
Requires-Dist: tree-sitter==0.26.0
Requires-Dist: typer==0.26.8
Provides-Extra: mcp
Requires-Dist: fastmcp==3.4.7; extra == 'mcp'
Description-Content-Type: text/markdown

# levain-cli

The open toolchain for authoring [Levain](https://levainlabs.com) agent
recipes: a validator, model checker, and code generator for the PlusCal
recipe format that Levain agents are defined in.

A recipe package is a `graph.tla` PlusCal spec (the agent's node graph
and state) plus a Python package with one function per node. This tool
checks both halves and keeps them coherent:

- **validate** — parse the spec, enforce the recipe grammar profile,
  check graph topology, translate PlusCal to TLA+, and model-check the
  result with TLC (deadlock and termination).
- **validate-package** — all of the above, plus Python source
  cross-checks (every `@node` function exists and is importable) and
  `pyproject.toml` checks.
- **generate-state** — regenerate `_state.py`, the typed `GraphState`
  TypedDict node functions program against.

## Install

```
uv tool install levain-cli
```

TLC model checking (stages 4-5) needs a Java runtime; `tla2tools.jar`
is fetched automatically on first use. Without Java the tool degrades
to the pure-Python stages and says so — the Levain platform re-runs
full validation on every push, so nothing is lost, only local
feedback latency.

## Use

```
levain validate graph.tla
levain validate-package .
levain generate-state .
levain --version
```

The import package is `levain_recipe` — use it to lint recipes from
your own CI or scripts:

```python
from levain_recipe.validate import validate_fast
```

Validation errors are prescriptive (`[stage] line N: message`, with
TLC counterexample traces) — they are the recipe format's primary
teaching interface, for humans and agents alike.

For MCP clients that cannot run shell commands (e.g. Claude Desktop),
`levain mcp` serves the same operations over stdio; install
with the `[mcp]` extra.

## What this is not

Recipe *execution* — compiling a validated spec into a running agent,
sandboxing, integrations — happens on the Levain platform. Passing
local validation is necessary, not sufficient: the platform validates
again server-side before a version can be published.
