# Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 25 of its 48 references that are in the map.
- First posted on arXiv 17 May 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

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

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [A Survey on Large Language Models for Code Generation](https://mlsanity.com/paper/2406.00515/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Large Language Models for Software Engineering: A Systematic Literature Review](https://mlsanity.com/paper/2308.10620/) (2023)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)
- [Lemur: Integrating Large Language Models in Automated Program Verification](https://mlsanity.com/paper/2310.04870/) (2023)
- [TacticToe: Learning to Prove with Tactics](https://mlsanity.com/paper/1804.00596/) (2018)
- [LeanAgent: Lifelong Learning for Formal Theorem Proving](https://mlsanity.com/paper/2410.06209/) (2024)
- [Proving Theorems Recursively](https://mlsanity.com/paper/2405.14414/) (2024)
- [The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq](https://mlsanity.com/paper/2008.00120/) (2020)
- [Four Principles for Physically Interpretable World Models](https://mlsanity.com/paper/2503.02143/) (2025)
- [PaMpeR: Proof Method Recommendation System for Isabelle/HOL](https://mlsanity.com/paper/1806.07239/) (2018)
- [On the Effectiveness of Large Language Models in Writing Alloy Formulas](https://mlsanity.com/paper/2502.15441/) (2025)
- [Provably Correct Automata Embeddings for Optimal Automata-Conditioned Reinforcement Learning](https://mlsanity.com/paper/2503.05042/) (2025)
- [A Proof Strategy Language and Proof Script Generation for Isabelle/HOL](https://mlsanity.com/paper/1606.02941/) (2016)
- [CoqPyt: Proof Navigation in Python in the Era of LLMs](https://mlsanity.com/paper/2405.04282/) (2024)
- [Learning Formal Specifications from Membership and Preference Queries](https://mlsanity.com/paper/2307.10434/) (2023)
- [Learning Minimal Neural Specifications](https://mlsanity.com/paper/2404.04662/) (2024)
- [Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces](https://mlsanity.com/paper/2501.13712/) (2025)
- [PAT-Agent: Autoformalization for Model Checking](https://mlsanity.com/paper/2509.23675/) (2025)
- [Do AI assistants help students write formal specifications? A study with ChatGPT and the B-Method](https://mlsanity.com/paper/2502.07789/) (2025)
- [Code Generation for Event-B](https://mlsanity.com/paper/1602.02004/) (2016)

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

- [Specula: Scaling formal specifications for autonomous model checking of system code](https://mlsanity.com/paper/2607.25333/) (2026)
- [Self-evolving network verifiers](https://mlsanity.com/paper/2608.11340/) (2026)
- [CAPRI: Contract-Aware Proof Repair for Isabelle](https://mlsanity.com/paper/2608.13459/) (2026)

## Abstract (arXiv)

Building software that is correct by construction is a long-standing goal in software engineering, as it ensures reliability during design and development rather than after deployment. Formal methods realize this vision by enabling the expression of system behavior and requirements in mathematics, thereby guaranteeing correctness through formal verification, including theorem proving and model checking. However, the steep learning curve and demand for mathematical expertise hinder the widespread adoption of formal methods. Large language models (LLMs) have recently shown promise in bridging this gap through autoformalization. However, existing LLM-based approaches are largely limited to isolated tasks, such as theorem proving without formalization or model synthesis with insufficient verification. While valuable, these efforts do not fully exploit the potential of a more comprehensive framework in which models and proofs evolve together, a process that closely reflects real-world development practice. To address this gap, we propose Event-B Agent, a novel framework inspired by the interleaved nature of software design. Given natural language requirements, Event-B Agent constructs an initial model and iteratively repairs and refines it using formal verification feedback. Refinement simplifies proof discharge, while repair of models and proofs ensures the soundness of each refinement step. Together, these two components reinforce each other to progressively improve the model quality. Evaluation across systems of varying complexity demonstrates that Event-B Agent substantially outperforms baselines in end-to-end formal model synthesis and repair, while maintaining reasonable efficiency. These results suggest that Event-B Agent is a promising step toward correct-by-construction formal model synthesis and repair.