A TLA+ Gate for PydanticAI Agent State Transitions

Put a check between an agent plan and a deployment

Autonomous development agents are often described as sequences of sensible stages: plan, write code, test, then deploy. The difficult part is not naming those stages. It is ensuring that a workflow cannot skip a required one when an agent produces an unexpected action or state.

MuLIAICHI/pydanticai-tla-guard is aimed at that boundary. Its README presents pydanticai-tla, a package that wraps a PydanticAI agent and validates state transitions with TLA+, a formal specification language commonly used to describe and model-check systems with many possible states. The project is for builders experimenting with agent pipelines who want to express rules about what must be true before the pipeline advances.

The repository makes an ambitious claim about guaranteeing bug-free transitions. The supplied evidence documents the intended guardrail and a demo, but it does not include model-checker output, a formal specification file, or test results establishing that claim. It is more useful to read the project as a concrete pattern: make workflow safety conditions explicit, then place validation at each transition instead of relying only on an agent's instructions.

Wrapping the agent rather than redesigning it

The documented interface is deliberately compact. A developer first creates a normal PydanticAI Agent, then passes it to TLAGuardedAgent:

from pydantic_ai import Agent
from pydanticai_tla import TLAGuardedAgent

my_agent = Agent("gpt-4o")
safe_agent = TLAGuardedAgent(my_agent)
await safe_agent.run("Build a payment processing module.")

According to the README, the wrapper intercepts PydanticAI state transitions and validates them against TLA+-derived invariants. If it encounters an illegal transition, the documented behavior is to raise ValueError.

That integration point matters. A wrapper is a focused way to add a control around an existing agent rather than ask every prompt, tool, or downstream system to remember the same policy. For a team already using PydanticAI, the intended developer experience is to preserve the agent construction they know and introduce a guarded object at run time.

The repository's stated workflow is linear: Plan flows to Code, Code to Test, and Test to Deploy. Each edge is labeled tla_verify(). The README says the agent's simulated state is compiled into a TLA+ specification and checked against invariants before the next node executes. That frames verification as a pre-transition decision, not a retrospective audit after deployment.

One invariant makes the policy tangible

The clearest example in the README is an invariant named NoDeployUntested:

[](pc = "deploy" implies "test_report" \in artifacts)

The repository explains it in plain language: whenever the program counter is at deploy, a test_report must be present in the artifacts. In other words, deployment is disallowed unless testing has produced the expected evidence.

This is a useful implementation lesson even for teams that do not adopt TLA+. A safety rule is stronger when it is stated as a condition over workflow state than when it appears only as prose in a system prompt. “Run tests before deployment” leaves room for interpretation. A requirement that a specific artifact exists at a specific transition gives the workflow a condition that software can evaluate.

The tradeoff is that the quality of the result depends on the model. The documented invariant only protects the property it encodes. It does not, by itself, establish that a test report is trustworthy, that the tests are adequate, or that every relevant state and transition has been represented. Formal methods can make specified properties checkable, but the specification still needs careful design.

A package and a visual demo

The package manifest identifies the published project as pydanticai-tla, version 0.1.1, with Python 3.10 or newer required. Its confirmed runtime dependencies are pydantic-ai and pydantic. Hatchling is configured as the build backend, while the optional development dependencies include pytest and pytest-asyncio.

Those details describe a narrow Python package surface. PydanticAI is the agent framework being wrapped. Pydantic is a declared dependency for Python data modeling and validation. The README also names LangGraph in its high-level description, but LangGraph is not listed in the supplied manifest, so the available evidence does not establish it as a packaged runtime dependency.

Alongside the package, the repository documents a local demonstration. It provides a demo_cli.py command with both a normal path and a --buggy mode, described as showing the guard catching a hallucinated transition. It also includes workflow_viewer.html, an interactive n8n-style viewer where readers can toggle safe and buggy modes and observe workflow badges. These are useful communication tools for a project about invisible control flow: users can see where a transition is expected to be blocked.

The demo should still be treated as a demonstration of the repository's intended behavior, not independent validation of its broader safety claims. Before using such a guard in a consequential pipeline, builders would need to inspect the implementation, identify how state is represented, review the exact invariants, and verify failure handling around the blocked transition.

A starting point for explicit agent workflow rules

pydanticai-tla-guard's central idea is straightforward: agent orchestration should have enforceable state rules, especially around irreversible steps such as deployment. Its value is less in a promise that all bugs vanish and more in the discipline of turning assumptions into invariants that a workflow gate can check.

Builders working with PydanticAI can inspect the package interface, demo workflow, and documented NoDeployUntested example in the verified repository: https://github.com/MuLIAICHI/pydanticai-tla-guard.