As AI agents increasingly write the deepest layers of production LLM infrastructure, the bottleneck is shifting from raw coding capability to rigorous verification. The Hao AI Lab has released vstack, a 5-stage formal verification workflow designed to prove the correctness of agent-generated code. Alongside vstack, the lab introduced veriserve, a prototype verifiable LLM serving engine that uses formal methods to eliminate silent concurrency bugs in Prefill-Decode disaggregated serving.

The Silent Bug Crisis In Distributed Serving

Modern inference engines like vLLM and SGLang have evolved into complex asynchronous distributed systems where requests can time out while RDMA transfers are still in flight. This creates race conditions where one user’s KV cache silently mixes with another’s, often returning an HTTP 200 OK despite corrupted data. Traditional CI tests and human code reviews fail to catch these rare interleavings, especially when a single engineer orchestrates thousands of parallel coding agents.

Vstack: Blocking Reward Hacking With Formal Gates

Vstack operates as a plugin for Claude Code and Cursor, enforcing a strict workflow that prevents agents from cheating the verification process. It pins specifications by hash, validates model fidelity against real code, and uses TLA+ and Z3 to prove safety invariants. This approach stops agents from weakening invariants or deleting timeout branches just to pass a model checker, ensuring that the proofs reflect the actual production logic.

Veriserve: Proving Safety With TLAPS And Z3

The veriserve engine centers on a formally verified PdLedger design model, backed by a massive 226-module, 516,973-obligation TLAPS safety proof. By tracking every physical page via a versioned ticket, the system decouples request cancellation from hardware DMA completion. This design resolves the trade-off between hanging requests and data corruption, adding only 0.18% mean p50 TPOT overhead on NVIDIA GB200 hardware.

Real Bugs Found In SGLang And vLLM

Applying vstack to production code uncovered three classes of real RDMA and cache concurrency bugs in both SGLang and vLLM. The team submitted six proposed upstream pull requests, including fixes for reclaiming transfer slots while RDMA is in flight and handling unrenewed transfer leases. These findings demonstrate that even mature open-source engines harbor subtle lifecycle failures that only formal verification can reliably expose.

Key Takeaways

  • Vstack enables coding agents to write and prove formal specifications, making verification scalable.
  • Veriserve proves that formal verification is practical for production LLM serving with minimal overhead.
  • Local CPU timeouts are fundamentally insufficient for guaranteeing isolation in asynchronous RDMA systems.
  • Six upstream PRs were submitted to SGLang and vLLM to fix critical concurrency bugs.

The Bottom Line

Verification is the new bottleneck for AI infrastructure; vstack proves that agents can handle the heavy lifting of formal proofs, making 'trust but verify' obsolete in favor of 'verify then trust'.