Compiling by Proving in \({K}\) : From All-Path Reachability Proofs to Single-Step Semantic Rules

The \({K}\) framework generates language tools from formal semantics and hosts comprehensive semantics for real-world languages including C, Java, JavaScript, and the Ethereum Virtual Machine, with industrial adoption in blockchain verification. However, the generated executors interpret programs by applying semantic rules step by step, causing performance overhead that limits practical scalability. We present compiling by proving , a language-agnostic mechanism that eliminates this overhead. Given a code unit, we use symbolic execution to prove that its specification holds across all execution paths, generating a proof graph that encodes the complete input-output behavior. We compile this proof graph into a single-step rule that directly maps inputs to outputs, replacing step-by-step interpretation with one-step execution. Because the pipeline is language-agnostic, it benefits any language formalized in \({K}\) . We evaluate on EVM and Rust MIR semantics, showing speedups in concrete and symbolic execution, and demonstrate applications to semantic equivalence verification and compositional smart contract verification.