levain-cli

The open toolchain for authoring Levain 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:

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.