# BALI: Branch-Aware Loop Invariant Inference with Large Language Models

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 31 Dec 2025.

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

- [Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification](https://mlsanity.com/paper/2607.10291/) (2026)

## Abstract (arXiv)

Loop invariants are fundamental for reasoning about the correctness of iterative algorithms. However, deriving suitable invariants remains a challenging and often manual task, particularly for complex programs. In this paper, we introduce BALI, a branch-aware framework that integrates large language models (LLMs) to enhance the inference and verification of loop invariants. Our approach combines automated reasoning with branch-aware static program analysis to improve both precision and scalability. Specifically, unlike prior LLM-only guess-and-check methods, BALI first verifies branch-sequence-level (path-level) clauses with SMT and then composes them into program-level invariants. We outline its key components, present preliminary results, and discuss future directions toward fully automated invariant discovery.