# Non-Termination Proving: 100 Million LoC and Beyond

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 2 of its 22 references that are in the map.
- First posted on arXiv 5 Sep 2025.

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

- [Proving Non-termination by Program Reversal](https://mlsanity.com/paper/2104.01189/) (2021)
- [DynamiTe: Dynamic Termination and Non-termination Proofs](https://mlsanity.com/paper/2010.05747/) (2020)

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

- [CWM: An Open-Weights LLM for Research on Code Generation with World Models](https://mlsanity.com/paper/2510.02387/) (2025)

## Abstract (arXiv)

We report on our tool, Pulse Infinite, that uses proof techniques to show non-termination (divergence) in large programs. Pulse Infinite works compositionally and under-approximately: the former supports scale, and the latter ensures soundness for proving divergence. Prior work focused on small benchmarks in the tens or hundreds of lines of code (LoC), and scale limits their practicality: a single company may have tens of millions, or even hundreds of millions of LoC or more. We report on applying Pulse Infinite to over a hundred million lines of open-source and proprietary software written in C, C++, and Hack, identifying over 30 previously unknown issues, establishing a new state of the art for detecting divergence in real-world codebases.