Elamur Research⌕
☰
home / papers / 2026 / Formally Specifying the Intended Behavior of the Program: LLM-Driven Neuro-Symbolic Program Specification Synthesis

Formally Specifying the Intended Behavior of the Program: LLM-Driven Neuro-Symbolic Program Specification Synthesis

Paper · 2026 · Cheng Wen, Hu Junjie, YiKun Hu et al.

Summary

Deductive verification can prove that C code meets its requirements, but only after someone writes formal annotations such as contracts and loop invariants. That work is slow, demands expertise, and limits adoption. The authors present AutoSpec+, an open-source, Dockerized demonstration system that automates this step for ACSL with Frama-C and its WP-plugin. Static analysis builds an extended call graph in which both loops and functions are nodes. The system then works bottom-up: an LLM receives only the relevant code slice plus callee specifications that have already been validated. Each proposed annotation goes to the verifier, which acts as a deterministic judge and drives rejection or repair until a proof succeeds or the budget runs out. The tool can combine several LLMs in an ensemble, handles verification across multiple files, and can generate loop variants to prove termination. Across seven benchmark suites, the ensemble verifies 91.05% of programs, ahead of learning-based and prompt-only baselines. This shows how checking LLM output with a symbolic tool makes it trustworthy enough for proof-ready specifications.

Key points

  • Benchmarks: seven suites were used: SyGuS, OOPSLA-13, Frama-C-problems, SV-COMP, the real-world X509 project, FM-bench-verified, and Live-FM-Bench. The last two form a dynamic set of 630 programs.
  • Main result: with the ensemble, overall pass@5 reaches 91.05%. Termination is proved for 93.42% of the intended-terminating programs that were already verified for partial correctness.
  • Ablation on Frama-C-Problems:
    • Prompt-only inference reaches 27.50% with GPT-4o and 43.13% with Gemini 2.5 Pro.
    • Adding decomposition gives a small gain.
    • Iterative refinement gives a large improvement.
    • The ensemble reaches 76.40%.
  • Backends and cost: five LLMs were tested: Gemini 2.5 Pro, DeepSeek-V3.1, Qwen3-235B (thinking), GPT-4o, and Kimi-K2. Each sample uses about 2k–6k tokens and costs roughly 0.2–3.6 cents. Verification time (typically under 100 s) outweighs LLM querying (under 10 s).
  • Case studies and release: the demos include an aerospace IP component from CAST and an inter-modular X.509 parser. Code, a Docker image, and full results are available on GitHub and Hugging Face.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Peking UniversityBeijing · China244 works · 39,359 citations🎓Xidian UniversityXi'an · China14 works · 1,357 citations🎓Shenzhen UniversityShenzhen · China16 works · 95 citations🎓Guangzhou Institute of TechnologyGuangzhou · China2 works · 5 citations

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 16,667 worksArtificial Intelligence · 16,194 worksArts and Humanities · 16,039 worksLanguage and Linguistics · 15,891 worksInformation Systems · 1,437 works

🧭 Topics 1Research subjects and languages the work is about.Language models & pretraining · 3,320 works

Cite

Cite as Cheng Wen, Hu Junjie, YiKun Hu, Jie Su, Bin Yu, Dugang Liu, Zhiwu Xu, Weidi Sun, Shengchao Qin and Cong Tian. 2026. Formally Specifying the Intended Behavior of the Program: LLM-Driven Neuro-Symbolic Program Specification Synthesis. Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 3: System Demonstrations).

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.18653/v1/2026.acl-demo.66

@inproceedings{wen2026formally,
  title = {{Formally Specifying the Intended Behavior of the Program: LLM-Driven Neuro-Symbolic Program Specification Synthesis}},
  author = {Cheng Wen, Hu Junjie, YiKun Hu, Jie Su, Bin Yu, Dugang Liu, Zhiwu Xu, Weidi Sun, Shengchao Qin and Cong Tian},
  booktitle = {Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 3: System Demonstrations)},
  year = {2026},
  doi = {10.18653/v1/2026.acl-demo.66},
  url = {https://doi.org/10.18653/v1/2026.acl-demo.66}
}

References

28 references, 0 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. 360 c programs under verification together with the properties to be verified. https://huggingface.co/datasets/fm-universe/Live-FM-Bench. Accessed: 2026-02-27. ↗
  2. Rajeev Alur, Dana Fisman, Saswat Padhi, Rishabh Singh, and Abhishek Udupa. 2019. find
  3. Sygus-comp 2018: Results and analysis. CoRR, abs/1904.07146. — [arXiv:1904.07146](https://arxiv.org/abs/1904.07146) find
  4. ANSSI-FR. 2026. a rte-free x.509 parser: https://github.com/ANSSI-FR/x509-parser, accessed: 2026-02-27. ↗
  5. Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. 2021. Acsl: Ansi/iso c specification. find
  6. Dirk Beyer. 2022. Progress on software verification: Sv-comp 2022. In Tools and Algorithms for the Construction and Analysis of Systems, pages 375–402, Cham. Springer International Publishing. find
  7. Allan Blanchard. 2020. Introduction to c program proof with frama-c and its wp plugin. find
  8. Allan Blanchard, Claude Marché, and Virgile Prevosto. 2024. Formally expressing what a program should do: the acsl language. In Guide to Software Verification with Frama-C: Core Components, Usages, and Applications, pages 3–80. Springer. find
  9. Weining Cao, Guangyuan Wu, Tangzhi Xu, Yuan Yao, Hengfeng Wei, Taolue Chen, and Xiaoxing Ma. 2025. Clause2inv: A generate-combine-check framework for loop invariant inference. Proceedings of the ACM on Software Engineering, 2(ISSTA):1009–1030. find
  10. Zehan Chen, Long Zhang, Zhiwei Zhang, JingJing Zhang, Ruoyu Zhou, Yulong Shen, JianFeng Ma, and Lin Yang. 2025. Sld-spec: Enhancement llm-assisted specification generation for complex loop functions via program slicing and logical deletion. arXiv preprint arXiv:2509.09917. — [arXiv:2509.09917](https://arxiv.org/abs/2509.09917) find
  11. Isil Dillig, Thomas Dillig, Boyang Li, and Ken McMillan. 2013. Inductive invariant generation via abductive inference. In Proceedings of the 2013 ACM SIG-PLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA ’13, page 443–456, New York, NY, USA. Associ… find
  12. Arnaud Ebalard, Patricia Mouy, and Ryad Benadjila. 2019. Journey to a rte-free x. 509 parser. In Symposium sur la sécurité des technologies de l’information et des communications (SSTIC 2019), volume 186. fm universe. 2026a. Fm-bench-verified: a manual-cleaned and verified benchmark which contains 2… find
  13. Reiner Hähnle and Marieke Huisman. 2019. Deductive software verification: from pen-and-paper proofs to industrial tools. Computing and Software Science: State of the Art and Perspectives, pages 345–373. find
  14. John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, and Matthew Parkinson. 2012. Behavioral interface specification languages. ACM Comput. Surv., 44(3). find
  15. Junjie Hu, Cheng Wen, Jialun Cao, Yikun Hu, Dugang Liu, Zhi Ma, Zhiwu Xu, and Shengchao Qin. 2026. When large language models meet formal theorem proving: A survey. In International Conference on Knowledge Science, Engineering and Management. Springer. find
  16. Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. 2015. Frama-c: A software analysis perspective. Formal aspects of computing, 27:573–609. find
  17. Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023. Verus: Verifying rust programs using linear ghost types. Proceedings of the ACM on Programming Languages, 7(OOPSLA1):286–315. find
  18. Gary T Leavens, Albert L Baker, and Clyde Ruby. 2006. Preliminary design of jml: A behavioral interface specification language for java. ACM SIGSOFT Software Engineering Notes, 31(3):1–38. find
  19. Ruibang Liu, Minyu Chen, Ling-I Wu, Jingyu Ke, and Guoqiang Li. 2025. Enhancing automated loop invariant generation for complex programs with large language models. Science of Computer Programming, page 103387. find
  20. Zhi Ma, Xiao Liang, Cheng Wen, Chen Rui, Bin Gu, Shengchao Qin, Cong Tian, and Mengfei Yang. 2026a. Automated ltl specification generation from industrial aerospace requirements. In International Symposium on Formal Methods, pages 1–20. Springer. find
  21. Zhi Ma, Cheng Wen, Bin Yu, and Jie Su. 2026b. Integrating ensemble learning and large language models for efficient formal verification of ip-based aerospace systems. Information Fusion, 125:103466. find
  22. Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, and Suman Jana. 2020. Cln2inv: Learning loop invariants with continuous logic network. In International Conference on Learning Representations. find
  23. Xujie Si, Hanjun Dai, Mukund Raghothaman, Mayur Naik, and Le Song. 2018. Learning loop invariants for program verification. Advances in Neural Information Processing Systems, 31. find
  24. Kurt Sieber. 2013. The foundations of program verification. Springer-Verlag. find
  25. Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Cheung, and Cong Tian. 2024. Enchanting program specification synthesis by large language models using static analysis and program verification. In International Conference on Computer Aided Verification, pages 3… find
  26. Fanpeng Yang, Xu Ma, Shuling Wang, Xiong Xu, Qinxiang Cao, Naijun Zhan, Xiaofeng Li, and Bin Gu. 2025. Automated synthesis of formally verified multi-abstraction function summaries. arXiv preprint arXiv:2506.09550. — [arXiv:2506.09550](https://arxiv.org/abs/2506.09550) find
  27. Shiwen Yu, Ting Wang, and Ji Wang. 2023. Loop invariant inference through smt solving enhanced reinforcement learning. In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 175–187. find
  28. Yuchen Zhang, Cheng Wen, Zhiwu Xu, Dugang Liu, Jialun Cao, Yuwei Liu, Shengchao Qin, and Cong Tian. 2026. Enhancing llm-based proof synthesis for rust programs via semantic chunking and hierarchical context expansion. In International Symposium on Theoretical Aspects of Software Engineering. Springe… find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/wen-2026-formally-specifying-intended-behavior-program/