Formal Verification via Agentic Statecharts: Beyond Probabilistic Unit Testing in Production Codebases

The Verification Ceiling: Why Probabilistic Testing Misses Concurrency Heisenbugs

Every distributed systems engineer eventually hits the verification ceiling. When writing asynchronous state machines—whether managing multi-tenant worker leases, distributed lock renewals, or optimistic UI state reconciliation—the conventional safety net breaks down. Unit tests execute isolated happy paths. Integration tests mock the messy parts of the transport layer. Property-based fuzzing tools like Hypothesis or fast-check do an admirable job generating randomized inputs, but they remain strictly probabilistic. If a double-lease bug requires an exact seven-step interleaving across asynchronous event boundaries, random test execution can run overnight and never hit the critical state permutation.

Standard coding agents don't solve this problem; they amplify it. When you prompt a frontier LLM to review a complex async/await state machine, it performs intuitive pattern recognition. It checks for obvious null pointers, dangling promises, or unhandled errors, but it cannot mentally compute the Cartesian product of concurrent state transitions. I have seen countless pull requests where an agent confidently proclaimed a lease renewal mechanism race-free, only for the runtime to silently corrupt state under burst concurrency. We have explored automated review before in Beyond Tone Polish: Deconstructing Google Deep Review's Inference-Scaled Formal Auditing, but probabilistic code inspection simply cannot verify concurrency.

This is why I find the approach in pstack's /create-formal-verification-skill compelling. Instead of trusting an agent’s intuition or relying on random test execution, the skill orchestrates a neurosymbolic bridge. It uses the LLM for what it does well—synthesizing structural abstractions from messy, unannotated code into visual statecharts—and hands the resulting state model over to an exhaustive formal solver like TLC (for TLA+/PlusCal), Kani (for Rust), or Z3.

Probabilistic Fuzzing:        [Rand] ──> [Rand] ──> [Pass?]  (Sparse coverage)
LLM Code Review:             [Code] ──> [Intuition] ──> "Looks good" (Zero guarantee)
Neurosymbolic Verification:  [Code] ──> [Statechart] ──> [Model Checker] ──> Exhaustive Proof

A model checker does not sample; within bounded parameters (such as two workers, a queue depth of three, and a single renew retry), it evaluates every reachable permutation of system states. If an execution path exists that violates an invariant—such as two active leases coexisting simultaneously—the solver mathematically flags it. By packaging this engine into an automated agent skill, formal verification moves from an academic exercise reserved for critical infrastructure protocols into an automated check running directly against application components.

The Extraction Pipeline: Translating Mermaid Statecharts into Solvable Specifications

The primary reason formal verification has historically failed to gain traction in product engineering is the immense barrier to entry. Writing raw TLA+, PlusCal, or SMT2 definitions requires specialized mathematical fluency that most product developers lack. The innovation behind the /create-formal-verification-skill pipeline is positioning a visual Mermaid statechart as an intermediate cognitive bridge between messy code and rigid formal logic.

When you invoke the command against a state-heavy component—like a distributed lease engine—the agent reads the unannotated application code and extracts a discrete state machine serialized as a Mermaid state diagram. It identifies the operational states (Acquiring, Active, Renewing, Expired, Revoked), the transitions between them, the triggering events, and the conditional guards.

This visual statechart serves a critical dual purpose. For the human engineer, it acts as an immediate audit layer. I can glance at a rendered diagram in five seconds and spot obvious discrepancies: "Why is there a direct transition from Renewing to Revoked that bypasses error handling?" For the agent, the statechart formalizes system boundaries, converting ad-hoc branching logic into a structured mathematical graph that directly maps to formal specification primitives.

sequenceDiagram
    autonumber
    actor Developer
    participant Agent as Coding Agent
    participant Chart as Mermaid Statechart
    participant Spec as PlusCal/TLA+ Model
    participant Solver as TLC Model Checker
    participant Code as Production Code

    Developer->>Agent: /create-formal-verification-skill (Lease Engine)
    Agent->>Code: Parse logic & concurrency boundaries
    Agent->>Chart: Synthesize state transitions & guards
    Chart-->>Developer: Visual audit of system states
    Agent->>Spec: Compile statechart into PlusCal & safety invariants
    Agent->>Solver: Run model checker over bounded states
    Solver-->>Agent: Violation found: emit minimal counterexample trace
    Agent->>Code: Apply synchronization guard / patch logic
    Agent->>Chart: Update transitions & rollback states
    Agent-->>Developer: Verification passed & local skill generated

Once the state machine is framed, the agent translates the diagram and user-specified safety invariants into a formal model. In a distributed TypeScript or Go setting, it synthesizes a PlusCal model executed via TLC, encoding non-negotiable safety properties such as [](ActiveLeases <= 1). In Rust codebases, it can target Kani bounded model checking harnesses directly.

The pipeline doesn't stop at solving the immediate model; it generates a persistent, project-local skill directory (such as .cursor/skills/verify-lease-invariants/SKILL.md). This guarantees that subsequent agent invocations retain the harness, keeping future code modifications accountable to the mathematical model without manually rebuilding the verification pipeline.

Dissecting Counterexample Traces: From Solver Violations to Concrete Patches

When a model checker fails, it doesn't return a vague assertion error or an unhelpful stack trace. It produces a minimal counterexample trace: a step-by-step, chronological sequence of states that leads directly to an invariant breach. Understanding how to operationalize these traces is where the synergy between formal solvers and coding agents becomes transformative.

Consider an invariant in a concurrent lease manager: mutual exclusion dictates that two worker processes must never hold Active status over the same resource partition. When TLC runs against an extracted PlusCal model of a typical lease engine, it might explore 4,200 unique states across variable interleavings before finding a failure at step 6:

1. State 1: Worker A initiates lease acquisition; state moves to Acquiring.
2. State 2: Worker A successfully acquires lease; state updates to Active with TTL $T$.
3. State 3: Timer advances past $T$; Worker A issues an asynchronous renewal request, transitioning to Renewing.
4. State 4: The network delays the renewal response. Concurrently, the master node flags the lease as Expired and accepts an acquisition request from Worker B.
5. State 5: Worker B transitions to Active.
6. State 6: Worker A's delayed renewal response resolves successfully without checking current master term epoch; Worker A transitions from Renewing back to Active.
7. Failure: Len({w \in Workers : state[w] = "Active"}) > 1 — safety invariant violated.

An agent consuming this structured counterexample trace does not have to guess where the bug lives. The trace maps the exact interleaving flaw: the transition from Renewing back to Active failed to validate whether ownership had lapsed during the asynchronous network gap.

The agent maps this failure trace directly to the application source code. It introduces a monotonic fencing token or lease epoch check inside the asynchronous resolution block, ensuring that an expired lease cannot be refreshed out of band.

Crucially, the agent then reflects this fix back into the Mermaid statechart. It adds a conditional transition: if the lease epoch is stale upon renewal return, the engine must divert to an explicit Invalidated recovery state rather than returning to Active. By forcing the model checker to rerun against the updated code and statechart, the loop verifies that the patch genuinely resolves the violation without introducing secondary deadlocks into the reachable state space.

The Semantic Divergence Hazard: The Trap of the Verified Mirage

The most seductive failure mode in formal verification is the verified mirage: a mathematical proof that succeeds completely while leaving the underlying production service entirely broken. Model checkers like TLC or Z3 do not inspect your compiled bytecode or runtime event loop; they evaluate the abstract mathematical model synthesized by the agent. If that model abstracts away the exact mechanical defect responsible for production failures, the verifier simply returns a clean bill of health over a fantasy.

In my experience, this breakdown almost always traces back to the assumption of atomicity. When an agent extracts a statechart from application logic, it instinctively compresses multi-step asynchronous transitions into clean, discrete edges. A distributed lease renewal looks deceptively simple on paper: a worker holding an active lease requests an extension and moves straight to renewed. But production runtimes never execute asynchronous I/O atomically.

stateDiagram-v2
    direction TB

    state "Idealized Specification (Agent Model)" as Idealized {
        [*] --> ModelActive
        ModelActive --> ModelRenewed : renew() [Atomic]
        ModelRenewed --> [*]
    }

    state "Production Runtime (Asynchronous Reality)" as Production {
        [*] --> ProdActive
        ProdActive --> RedisPending : dispatch renew()
        RedisPending --> NetworkTimeout : socket drop / unhandled lag
        NetworkTimeout --> UnheldRelease : master expires lease TTL
        RedisPending --> ProdRenewed : response OK
        UnheldRelease --> ConcurrentCollision : late response processed as active
    }

Between dispatching an update to Redis and processing the response, the thread yields across the asynchronous boundary. If a network timeout or connection reset occurs during that interval, the system enters intermediate states—RedisPending, NetworkTimeout, or UnheldRelease—where the master node expires the lease TTL while the client still believes it is actively renewing. When the delayed response finally resolves, the worker treats its lease as valid, blindly colliding with a new worker that acquired the resource in the interim. If the agent's statechart omits those intermediate states, the formal engine mathematically proves safety across an idealized graph that bears little resemblance to runtime reality.

This semantic gap is compounded by vacuous proofs. A safety property like [](ActiveLeases <= 1) asserts that a bad state never occurs. If an agent synthesizes defensive transition guards that accidentally starve the system of transitions altogether, or if it forgets to model error recovery, the system can freeze in an unhandled deadlock. Because no two leases are active, the solver reports a pass. A safety invariant that passes because the state machine cannot make forward progress is worse than a failing test; it provides mathematical justification for dead code.

Finally, operators must confront bounded state-space truncation. Model checkers require concrete finite bounds to avoid exponential state explosions. An agent will typically configure bounded parameters such as two concurrent workers, a queue depth of three, and a single retry. While this allows the solver to complete exhaustive traversals in seconds, many concurrency bugs require deeper interleavings—such as three workers racing under a retry cascade at depth four—to manifest. Bounding the solver prunes away the combinatorial tail where the actual failure mode lives.

Architectural Alternatives: Comparing Agentic Specs, Runtime FSMs, and Direct Model Checkers

Choosing how to enforce state invariants requires balancing mathematical rigor against implementation friction. The pstack approach of generating external verification skills represents a distinct architectural choice: using an LLM to build a decoupled specification sidecar that leaves production code structurally untouched.

quadrantChart
    title Verification Rigor vs Implementation Friction
    x-axis Low Friction --> High Friction
    y-axis Low Rigor --> High Rigor
    quadrant-1 Specialized Rigor High Friction
    quadrant-2 Agentic Sweet Spot
    quadrant-3 Shallow Heuristics
    quadrant-4 Heavy Architectural Refactoring
    pstack Agentic Skills: [0.22, 0.82]
    Direct AST Kani and CBMC: [0.55, 0.90]
    Manual TLA+ and Dafny: [0.88, 0.94]
    Property-Based Testing: [0.42, 0.52]
    Executable XState: [0.78, 0.48]

To understand where this pattern fits, I evaluate it against three established paradigms across industry stacks:

Paradigm	Verification Rigor	Specification Drift Risk	Entry Barrier & Friction	Concurrency Coverage
pstack Meta-Skills (/create-formal-verification-skill)	High (exhaustive state exploration within bounded parameters)	High (model is decoupled from runtime source code)	Very Low (synthesizes formal models directly from legacy code)	Excellent (excels at distributed interleavings, locks, and async queues)
Executable Statecharts (e.g., XState, Stately)	Medium (validates defined graph paths via integration mocks)	Zero (the statechart is the actual executable runtime engine)	High (requires architecting the codebase around explicit statecharts)	Fair (single-process state machines; weak on distributed actor races)
Property-Based Testing (e.g., Hypothesis, fast-check)	Medium-High (probabilistic fuzzing across stateful action chains)	Zero (executes directly against real runtime APIs and dependencies)	Medium (requires writing custom generators, stateful rules, and harnesses)	Fair-Good (frequently misses narrow, multi-step concurrent race paths)
Direct SMT / AST Verification (e.g., Kani, CBMC)	Mathematical Proof (symbolic execution directly over compiled representations)	Zero (proves invariants directly on code AST / MIR)	High (restricted to specific languages like Rust/C; proof harnesses are rigid)	Language Dependent (checks thread interleavings, but cannot model distributed protocols)

Executable state machines like XState solve the specification drift problem at the root. Because the statechart is the runtime execution engine, the code cannot diverge from the model; invalid transitions are mechanically forbidden by the interpreter. However, requiring a development team to rewrite complex, ad-hoc business logic into formal hierarchical state machines imposes severe architectural friction. It is rarely viable for sprawling legacy backends.

Direct AST-level verifiers like Kani provide unmatched mathematical guarantees by feeding bounded compiler representations straight into SMT solvers, eliminating the intermediate translation layer entirely. But they remain confined to low-level systems languages like Rust and struggle to represent high-level distributed protocols across separate network nodes. Property-based testing engines like Hypothesis or fast-check run against real production code and network calls without mathematical abstraction, but their generative nature remains probabilistic. A randomized fuzzer can execute millions of state sequences without ever hitting the exact seven-step race sequence that triggers a split-brain condition.

The appeal of pstack lies in decoupled extraction: it gives teams the concurrency checking of formal model checkers without forcing an architectural rewrite of messy TypeScript, Python, or Go codebases. The operational compromise is maintenance discipline. Because the formal specification lives as an external artifact, teams must automate continuous synchronization on every pull request, or the model will quietly drift into irrelevance.

Hardening Verification in Continuous Integration: Mutation Checks and Spec Maintenance

Transitioning formal verification from an ad-hoc local prompt into an automated pull request gate introduces sharp operational hurdles. Left unmanaged, external specification files rot within weeks as method signatures change, and agents tasked with verification generate tautological proofs that pass without exercising real code paths.

To prevent specification drift, a continuous integration workflow cannot treat the generated artifacts under .cursor/skills/ as static documents. When a pull request touches code paths mapped to a formal harness, the pipeline must trigger /maintain-formal-verification-skill. This routine reads the recorded synchronization commit hash from the skill’s metadata, evaluates the diff against current application AST changes, and forces the agent to reconcile the statechart and formal model before running the verifier. If a developer introduces an early exit or alters a return status, the maintainer skill updates the transition guards in the specification. If the spec cannot be reconciled without violating an encoded invariant, the check halts the build.

The more dangerous hazard is the hollow green checkmark. An agent generating a verification harness under automated pressure will often introduce a vacuous proof—asserting safety over an unreachable branch or modifying the model's assertion rather than testing whether the model is sensitive to operational regressions.

To harden against this, I mandate automated mutation testing on the generated skill before ratifying it into CI. The pipeline must programmatically introduce at least two distinct failure mutations directly into the production code:

1. Stripping a critical synchronization barrier or concurrency lock.
2. Forcing an out-of-order transition or stale epoch write.

The generated skill is only valid if the underlying model checker flags both deliberate mutations with counterexample traces. If the solver reports a pass against mutated code, the harness is uncoupled from reality and rejected.

PR Diff Detected ──> Check Mapped Skills ──> Spec Sync Check (/maintain)
                                                    │
     ┌──────────────────────────────────────────────┘
     ▼
Automated Mutation Test ──> Inject Concurrency Flaw ──> Verifier Catches?
     │                                                        │
     ├── [Passes / No Flag] ──> Reject Skill (Tautology)      │ (Yes)
     └── [Counterexample Emitted] ────────────────────────────┴──> Run PR Proof

Finally, verifier toolchains must be strictly isolated. Running TLC, Z3, or Kani relies on runtime environments—such as specific JVM versions or SMT solver binaries—that rarely exist on standard ephemeral CI runners or teammate machines. Packaging the formal execution harness into a hermetic container or standardized GitHub Action ensures that the agent executes the formal check against fixed binaries. This architecture mirrors the sandboxed verification environments we explored when analyzing Durable AI Coding in Ephemeral Sandboxes: Dissecting Vercel Labs' durable-harness, isolating non-deterministic local system quirks from deterministic mathematical verification.

Practical Verification Blueprints for High-Consequence Systems

Applying statechart-driven formal verification across an entire codebase is an anti-pattern. Model checking an entire application will immediately choke the solver with state-space explosion. The discipline lies in scoping verification strictly to bounded, high-consequence subsystems where race conditions, deadlocks, or split-brain states carry severe operational costs.

A prime target is a Distributed Multi-Tenant Lease and Heartbeat Renewal Engine. Distributed locking mechanisms relying on Redis or Postgres advisory locks frequently suffer from split-brain scenarios when asynchronous heartbeat workers encounter delayed network I/O. In this blueprint, the agent extracts a Mermaid statechart capturing the renewal lifecycle, complete with monotonic fencing tokens and re-entrancy guards, compiling it into a PlusCal and TLC harness.

To keep the state space tractable, the harness bounds parameters to three worker nodes, an epoch counter capped at four, and a maximum of two network retry attempts. When engineering this system, the failure mode to watch for is unmodeled network latency during heartbeat renewals. If an asynchronous I/O timeout is treated as a transient error without revoking local execution rights, the master lease expires while the local worker continues processing work, allowing a newly elected worker to acquire the same partition concurrently.

Another resilient use case is Optimistic UI State Synchronization with Idempotent Offline Outbox. Client-side architectures managing an IndexedDB mutation outbox against a remote event log must handle offline transitions, optimistic UI renders, and rollback reconciliations. The agent synthesizes a statechart modeling transient, failed, and reconciled synchronization states, verified using an invariant harness powered by Kani or fast-check.

The state explosion hazard here stems from unconstrained mutation queues; the specification must bound the queue depth to three distinct operations. The critical race condition to flag occurs during slow server response rounds: if a rollback routine naively wipes local state upon receiving a server error, it can overwrite newer, concurrent local mutations enqueued by the user while the failed network request was in flight.

Finally, consider a Multi-Stage Saga Orchestrator for Multi-Service Checkout. This transaction coordinator manages distributed inventory reservations, payment processing, and shipment dispatch across isolated microservices. The agent extracts forward execution transitions and backward compensating actions into a statechart verified against TLA+ temporal logic invariants.

The primary trap in saga verification is settling for pure safety invariants. A model checker verifying [](InventoryOverallocated == FALSE) will report success if the saga abruptly halts on an unhandled payment gateway timeout. Because no inventory was double-sold, safety holds—yet the system is deadlocked, leaving inventory indefinitely reserved while the customer’s checkout process freezes. Specifying liveness and progress properties within the generated skill forces the verifier to prove that every saga sequence either terminates in a completed dispatch or fully unwinds every partial allocation back to baseline.

Resources

• cursor/plugins on GitHub
• cursor/plugins on GitHub