Spec-Skill: A Pluggable Coding-Agent Plugin for Neuro-symbolic Program Specification Synthesis

Abstract

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 candidate 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 workflows. 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 integrate 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 an overall Pass@5 of 98.8% across the established benchmarks and verifies 171 of 212 functions in X509-parser, demonstrating the potential of agent-oriented orchestration for project-level specification synthesis.