Expecto: Extracting Formal Specifications from Natural Language Description for(…)
summary
Expecto converts natural language intents into a concise DSL and uses a neuro-symbolic pipeline with GPT-4.1 Mini for synthesis and Z3 for validation, building modular specs via top-down spec synthesis and iterative checking with continuous spec validation. On algorithmic benchmarks Expecto yields 1.2–1.4× more correct specs on HumanEval+ and 2.1–2.8× on harder Apps problems, and on Defects4J it produces 3–7× more sound (bug-detecting) specs than a monolithic LLM baseline. Artifacts and code are available.
AI-written summary · about
chapters (12)
- 0:00Expecto and spec-driven dev
- 2:08Natural language spec problems
- 3:56Generating modular specs
- 5:03Expecto's workflow
- 6:07Top-down spec synthesis
- 7:35Continuous spec validation
- 9:20Types of validators
- 10:26Benchmarks and setup
- 11:30Correctness metrics
- 12:33Detecting real-world bugs
- 14:00Summary and contributions
- 14:47Q&A
related talks
35mExtracting Specifications from Legacy Software with Elixir
23mStop Making LLMs Deterministic: A Spec-Driven Software Factory
17mThe New Frontend Stack: Humans, AI, and Prompts
56mIs Spec Kit the future for software development
47mSpec-Driven Development with AI Agents From High-Level Requirements to Working SW
53mNavigating AI Native Development
37mSpec Driven Development: AI Assisted Coding With Doc at the Core
22mThe New Code