{"ID":2864964,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2509.21793","arxiv_id":"2509.21793","title":"Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics","abstract":"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.","short_abstract":"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 c...","url_abs":"https://arxiv.org/abs/2509.21793","url_pdf":"https://arxiv.org/pdf/2509.21793v1","authors":"[\"Jianhong Zhao\",\"Everett Hildenbrandt\",\"Juan Conejero\",\"Yongwang Zhao\"]","published":"2025-09-26T02:49:08Z","proceeding":"cs.PL","tasks":"[\"cs.PL\",\"cs.CL\"]","methods":"[]","has_code":false}