Towards Verifiable LLM Infra 🚀

Suppose coding agents can build a fast inference engine from scratch, and one engineer orchestrates 10,000 agents in parallel: how do we know the engine they wrote is actually correct? Having agents review other agents mostly wastes tokens compared to empirical and formal verification.

We introduce vstack, a 5-stage formal verification workflow for coding agents, and veriserve, a verifiable PD-disaggregated serving engine: uncovering 3 classes of real RDMA and cache races in production serving engines, and backing veriserve's KV-page lifecycle design model with a 226-module, 516,973-obligation TLAPS safety proof at +0.18% mean p50 TPOT overhead on GB200.

Blog: haoailab.com/blogs/verifiable…
veriserve: github.com/hao-ai-lab/veriser…
vstack: github.com/hao-ai-lab/vstack