Antigravity TLA+ Verification Guard

Antigravity TLA+ Verification Guard

Instructions

You are equipped to help developers add formal mathematical verification (based on TLA+ concepts) to their AI agent workflows. This ensures a zero-bug guarantee for state transitions and prevents dangerous LLM hallucinations from executing in production.

Step 1: Identify State and Transitions

When building an agent pipeline, first identify the critical state transitions (the "program counter" or pc, e.g., plan → code → test → deploy).

Step 2: Implement the TLA+ Verifier

Provide the developer with a tla_verify guardrail function. This function must be called before any critical state transition occurs.

Key requirements for the verifier:

1. Extract current state and artifacts (e.g., from a LangGraph state dict).
2. Check strict invariants. The core invariant is usually NoDeployUntested (cannot transition to "deploy" without a "test_report" artifact).
3. If an invariant fails, immediately raise a ValueError and halt execution, simulating a TLA+ specification failure by printing the invalid TLA+ spec.

Step 3: Embed in the Agent Workflow

Integrate the verifier into the graph routing logic or state machine. Every node transition must pass the tla_verify check before proceeding.

Code Patterns to Use

When asked to implement this pattern, use the following standard Python file content:

from typing import Dict, List

def generate_tla_spec(state: dict):
    """
    Generates a TLA+ specification string from the current agent state.
    Used for formal verification before critical transitions.
    """
    artifacts = state.get("artifacts", [])
    # In state dict, artifacts might be Pydantic objects or dicts
    artifact_types = []
    for a in artifacts:
        if isinstance(a, dict):
            artifact_types.append(f'"{a.get("type")}"')
        else:
            artifact_types.append(f'"{a.type}"')