Spec-Skill: A Pluggable Coding-Agent Plugin for Neuro-Symbolic Program Specification Synthesis
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.