SPLASH 2026
Sun 4 - Fri 9 October 2026 Oakland, California, United States
co-located with SPLASH/ISSTA 2026

Formal verification provides strong correctness guarantees, but its practical adoption is limited by the cost of writing precise formal specifications. While large language models can generate candi- date specifications, prompt-only generation and monolithic LLM pipelines often struggle with verifier feedback, iterative repair, cross-function consistency, and project-level orchestration. Modern coding agents offer a natural interface for such tool-mediated work- flows. We present Spec-Skill, a pluggable agent plugin for neuro- symbolic program specification synthesis. A host agent decomposes a C project into layered verification units and coordinates sub- agents that synthesize ACSL function contracts and loop invariants, verify them with Frama-C/WP, and repair failures using verifier feedback. A common CLI-based interface allows Spec-Skill to inte- grate with different coding-agent platforms, including Claude Code and Codex. We evaluate Spec-Skill on established specification- generation benchmarks and a project-scale X509-parser codebase. Spec-Skill achieves up to 98.8% Pass@5 on existing benchmarks and verifies 171 of 212 functions in X509-parser, demonstrating the effectiveness of agent-oriented orchestration for robust, project- level specification synthesis.