# Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis

arXiv: https://arxiv.org/abs/2410.19736 · HTML: https://mlsanity.com/paper/2410.19736/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Builds on 2 of its 19 references that are in the map.
- First posted on arXiv 18 Sep 2024.

## Builds on (most cited first, 2 of 2)

- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [The 5th Reactive Synthesis Competition (SYNTCOMP 2018): Benchmarks, Participants & Results](https://mlsanity.com/paper/1904.07736/) (2019)

## Built on by (most cited first, 7 of 7)

- [EditLord: Learning Code Transformation Rules for Code Editing](https://mlsanity.com/paper/2504.15284/) (2025)
- [Requirements Development and Formalization for Reliable Code Generation: A Multi-Agent Vision](https://mlsanity.com/paper/2508.18675/) (2025)
- [Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs](https://mlsanity.com/paper/2508.15878/) (2025)
- [NERFIFY: A Multi-Agent Framework for Turning NeRF Papers into Code](https://mlsanity.com/paper/2603.00805/) (2026)
- [Proof2Silicon: Prompt Repair for Verified Code and Hardware Generation via Reinforcement Learning](https://mlsanity.com/paper/2509.06239/) (2025)
- [Lifecycle-Aware code generation: Leveraging Software Engineering Phases in LLMs](https://mlsanity.com/paper/2510.24019/) (2025)
- [Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification](https://mlsanity.com/paper/2604.17010/) (2026)

## Abstract (arXiv)

In the past few years, Large Language Models (LLMs) have exploded in usefulness and popularity for code generation tasks. However, LLMs still struggle with accuracy and are unsuitable for high-risk applications without additional oversight and verification. In particular, they perform poorly at generating code for highly complex systems, especially with unusual or out-of-sample logic. For such systems, verifying the code generated by the LLM may take longer than writing it by hand. We introduce a solution that divides the code generation into two parts; one to be handled by an LLM and one to be handled by formal methods-based program synthesis. We develop a benchmark to test our solution and show that our method allows the pipeline to solve problems previously intractable for LLM code generation.