Metadata-Version: 2.5
Name: levain-cli
Version: 0.1.20
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.27.3
Provides-Extra: mcp
Requires-Dist: fastmcp==4.1.3; 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 recipe
formats that Levain agents are defined in.

A recipe package is one of two kinds, set by `kind` under `[tool.levain]`
in its `pyproject.toml`:

- **graph** (the default): a `graph.tla` PlusCal spec (the agent's node
  graph and state) plus a Python package with one function per node.
- **harness**: one engine session (Claude Code or Hermes) declared in
  `[tool.levain.harness]`: engine, model, effort, system prompt, tools,
  MCP servers and state fields. No graph and no Python.

This tool checks both and keeps a graph's two halves coherent:

- **validate** — parse a 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** — validate a package of either kind. For a
  graph: all of the above, plus Python source cross-checks (every
  `@node` function exists and is importable) and `pyproject.toml`
  checks. For a harness: the `[tool.levain.harness]` keys and values,
  the prompt file, the state fields and the MCP server names.
- **generate-state** — regenerate `_state.py`, the typed `GraphState`
  TypedDict a graph's node functions program against. A harness has
  no state module.

## 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, validate_recipe
```

`validate_recipe(dir)` reads the package's kind and returns a
`ValidatedSpec` for a graph or a `HarnessSpec` for a harness, or a list
of errors.

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.
