Formal specifications used in program verification were always treated as locked once written. This paper argues that's exactly what causes cascading failures. Title: SpecAgent: Empowering Program Verification with Agentic Synthesis of Formal Program Specifications URL: 📝 Overview SpecAgent synthesizes ACSL specifications (preconditions, postconditions, loop invariants) for C program verification through coordinated specialized agents, reframing specification synthesis as an iterative agentic process of planning, retrieval-augmented generation, verification, repair, and critique. ❓ Problem Solved Existing approaches follow a forward-only workflow where once a specification is generated it stays fixed, so when downstream verification fails, they repeatedly attempt ineffective local repairs instead of revisiting the upstream specification that's the actual root cause. 💡 Method & Approach A planning agent identifies targets and dependencies; a retrieval-augmented generation agent injects similar examples from a 184-entry knowledge base to produce ACSL; a verification gate runs Frama-C/WP; a repairing agent diagnoses root causes; and a critique agent judges specification strength as ACCEPT, IMPROVE, or REPLAN. 📊 Results SpecAgent with DeepSeek-V4 hits 96.82% precision and 88.95% recall, beating every baseline. Ablations show the repair stage drives a big precision gain, and the full pipeline lifts recall by 8.02 points over generation alone. It discharges 604 of 811 real-world verification targets (74.5%) at lower cost than both Preguss and Codex. #ProgramVerification# #AIAgents#