SkySynth

SkySynth (SkyDiscover-Synthesize) är en öppen motor som låter kodagenter bygga program skräddarsydda för en viss uppgift, till exempel en databas eller en inferensmotor för en viss AI-modell. Grundtanken är att kravspecifikationen måste utvecklas tillsammans med koden. Annars hittar agenterna luckor i kraven och fuskar sig till godkända tester.

Systemet har två lägen. När kraven går att formulera helt formellt skriver agenterna koden steg för steg tillsammans med maskinkontrollerade bevis i Lean eller Rocq, och den bevisat korrekta koden trimmas sedan för fart utan att korrektheten försvagas. När kraven inte går att formalisera helt bygger systemet en specifikation, och en planerare, en kodagent, en utvärderare och en kritiker arbetar i en slinga. En granskare letar efter fusk och gör om varje upptäckt till nya tester. Alla roller körs med Claude Opus 4.8.

Enligt teamet klarade SkySynth 95,2 % av testerna när det byggde distribuerade nyckel-värde-databaser med bevis, mot 33,3 % för Claude Code och 23,8 % för Codex, och varje databas tog ungefär 6,9 timmar och 106 dollar. En inferensmotor för Qwen3-4B fick ungefär 2,2 gånger så hög genomströmning som finjusterade vLLM och SGLang, och en modellväljare för tolv modeller blev 1,72 gånger billigare totalt. SkySynth kan användas som en färdighet (skill) för kodagenter, och koden ligger på GitHub.