AI agents can write code, but can we trust the systems they build? With SkySynth, we co-evolve code with tests and formal proofs to generate specialized, just-in-time infrastructure. The result: formally verified KV stores 2.3× faster than Redis and custom inference engines with 2.2× the throughput of vLLM/SGLang!
Agents let us build systems for different workloads and requirements. But… can we trust what they build? We release 🌟SkySynth🌟: an engine for synthesizing high-performance, just-in-time (JIT) systems we can trust, by co-evolving formal proofs and tests alongside the code. Results: 💿 KV stores up to 2.3× faster than Redis and FASTER + formally verified stores with 2.9× Claude Code's pass rate 🚏 Model routers up to 48% cheaper than a general router ⚡ Specialized inference engine with 2.2× the throughput of vLLM/SGLang 🧵👇

Sep 11, 2026 · 6:55 PM UTC

11
11
163
21,199
Sort replies: Relevant Recent Liked
Replying to @istoica05
Co-evolving tests with code helps. The trap is the agent writing tests that match what it built, so both agree and both are wrong. Who writes the spec matters more than who writes the proof.
1
142
Replying to @istoica05
Totally agree with this
14
Replying to @istoica05
But the below stats to improve the infra the performance scale metrics like TTFT , invocation latency etc how does it improve quality accuracy and reduce cost
52
Replying to @istoica05
what's inside the proof boundary for the KV store: just get/put behavior, or crash recovery too?
95
Replying to @istoica05
pairing the proof with the code instead of writing it after the fact is the part that actually matters, a proof bolted on later just checks whatever the code happened to do
41
Replying to @istoica05
Co-evolving tests with the code closes the gap I kept falling into from the other side: my suite passed while the thing it tested meant something else. It verified the mapping ran, never that the mapping was right. github.com/soul-sol/ai-code-…
1
173