# Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 2 of its 32 references that are in the map.
- First posted on arXiv 26 Sep 2025.

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

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Souper: A Synthesizing Superoptimizer](https://mlsanity.com/paper/1711.04422/) (2017)

## Abstract (arXiv)

Verification proofs encode complete program behavior, yet we discard them after checking correctness. We present compiling by proving, a paradigm that transforms these proofs into optimized execution rules. By constructing All-Path Reachability Proofs through symbolic execution and compiling their graph structure, we consolidate many semantic rewrites into single rules while preserving correctness by construction. We implement this as a language-agnostic extension to the K framework. Evaluation demonstrates performance improvements across different compilation scopes: opcode-level optimizations show consistent speedups, while whole-program compilation achieves orders of magnitude greater performance gains.