Towards a Trustworthy Semantics-Based Language Framework via Proof Generation

This paper, authored by Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, and Grigore Rosu and published at CAV 2021 (Computer Aided Verification, 33rd International Conference), addresses a fundamental challenge in programming language tool development: how to ensure the correctness of tools that are automatically generated from formal language definitions. The work pursues the vision of an ideal language framework, where programming language designers need only define the formal syntax and semantics of their languages, and all language tools -- interpreters, compilers, debuggers, verifiers, and model checkers -- are automatically generated by the framework. The K semantic framework embodies this vision, but the complexity of such a framework makes it a significant challenge to ensure the trustworthiness of the auto-generated tools. Even if the formal semantics is correct, bugs in the framework itself could lead to incorrect tool behavior, undermining the guarantees that formal methods are supposed to provide.

The key idea proposed in the paper is to generate proof objects as correctness certificates for each individual task that the language tools perform, on a case-by-case basis. Rather than attempting to verify the entire language framework once and for all -- a daunting task given the framework's complexity and continuous evolution -- the authors propose that each execution step, each symbolic evaluation, and each verification result should be accompanied by a proof object that independently certifies its correctness. These proof objects can then be checked by a trustworthy proof checker that is small enough to be thoroughly verified. This approach shifts the trust from the complex framework to the simple proof checker: even if the framework contains bugs, any output accompanied by a valid proof object is guaranteed to be correct, because the proof checker independently verifies the reasoning.

The key insight is that generating proof objects is significantly easier than verifying the framework itself, because proof objects are concrete artifacts that can be mechanically checked, while framework verification requires reasoning about all possible inputs and execution paths.

The theoretical foundation for proof generation rests on matching logic, the logical foundation of the K framework. In matching logic, programming language semantics are expressed as rewrite rules that describe how program configurations transform during execution. Each rewrite rule $\varphi \Rightarrow \varphi'$ states that a configuration matching pattern $\varphi$ can transition to a configuration matching pattern $\varphi'$. A single step of program execution corresponds to the application of one rewrite rule, and a complete execution trace corresponds to a sequence of rule applications. The paper shows that each such rule application can be encoded as a valid proof step in the matching logic proof system (using rules including modus ponens: from $\varphi$ and $\varphi \to \psi$, derive $\psi$; framing: from $\varphi_1 \to \varphi_2$, derive $C[\varphi_1] \to C[\varphi_2]$; and the Knaster-Tarski rule: from $\varphi[\psi/X] \to \psi$, derive $\mu X.\, \varphi \to \psi$), and that the entire execution trace can be assembled into a complete matching logic proof that formally derives a reachability claim $\varphi_{\text{init}} \Rightarrow^\bullet \varphi_{\text{final}}$ establishing the relationship between the initial and final program configurations.

The paper addresses three major language tool tasks for which proof generation is developed: concrete execution (interpreting programs), symbolic execution (exploring program paths symbolically), and deductive program verification (proving program correctness properties). For concrete execution, the proof object certifies that a given program, when executed on a given input according to the formal semantics, produces a specific output. For symbolic execution, the proof object certifies that a symbolic execution tree correctly represents all possible execution paths of a program. For deductive verification, the proof object certifies that a program satisfies a given specification (e.g., a pre/post-condition pair $\{P\}\; C \;\{Q\}$, expressed as the reachability claim $\langle P, C \rangle \Rightarrow^\bullet \langle Q, \cdot \rangle$). In each case, the proof object is a matching logic derivation that can be independently checked.

The implementation of proof generation is built on top of the K framework. The authors extend the K framework's execution engine to emit proof hints alongside each execution step. A proof hint records which rewrite rule was applied, how pattern variables were instantiated, and what substitutions were performed. These hints are then processed by a proof generation module that constructs the full matching logic proof object. The proof objects are encoded in a format compatible with the Metamath proof verification system, which provides an independently verified proof checker. The choice of Metamath is deliberate: Metamath's proof checker is extremely simple (on the order of hundreds of lines of code), making it feasible to thoroughly audit and verify. The proof generation pipeline thus creates a chain of trust: the K framework generates the proof hints, the proof generation module constructs the proof, and Metamath independently verifies it.

The paper presents an evaluation of the proof generation approach using the IMP language, a simple imperative programming language commonly used as a benchmark in programming language research. IMP includes assignments, sequential composition, conditional statements, and while loops (where while (b) s is captured via the least fixpoint $\mu X.\, (\mathsf{if}\; b\; \mathsf{then}\; s \cdot X\; \mathsf{else}\; \cdot)$, with its dual greatest fixpoint $\nu$ applicable to infinite-trace reasoning) -- sufficient to exercise the core mechanisms of proof generation including variable binding, state manipulation, and fixpoint reasoning. The evaluation measures the size of generated proof objects, the time required for proof generation, and the time required for proof checking. The results demonstrate that proof generation is feasible in practice, with proof objects that grow linearly with the length of the execution trace and proof checking times that are practical for real-world use. While proof objects can be large for long executions, the linear growth rate ensures predictability, and the proof checking process is efficient because it involves only syntactic matching and substitution.

The trustworthiness argument of the approach is carefully analyzed in the paper. The trusted computing base (TCB) consists of only two components: the formal semantics of the programming language (which is provided by the language designer and is the definition of correctness), and the proof checker (which is small and independently verifiable). Notably, the K framework itself, the proof generation module, and the execution engine are all outside the TCB. If any of these components contain bugs, the worst that can happen is that proof generation fails or produces an invalid proof object; it cannot produce a valid proof object for an incorrect result. This property, known as soundness preservation, is the key security guarantee of the approach. The paper also discusses the completeness of proof generation: for any correct execution or verification result, the system should be able to produce a valid proof object.

By generating proof objects as correctness certificates, the approach separates the concern of efficient tool implementation from the concern of correctness verification, allowing each to be optimized independently.

The implications of this work extend far beyond academic language frameworks. The proof generation approach provides the theoretical and practical foundation for verifiable computing: any computation performed according to a formal semantics can produce a machine-checkable proof of its correctness. This is directly relevant to blockchain and smart contract verification, where the correctness of program executions has significant financial implications. The work laid the groundwork for Pi2 Labs's Proof of Proof technology, where the matching logic proof objects generated by this approach are further compiled into succinct cryptographic proofs (such as zero-knowledge proofs), enabling anyone to verify the correctness of a computation without re-executing it and without trusting the execution engine. The paper thus represents a crucial bridge between formal methods research and practical verifiable computing infrastructure.

In conclusion, the paper presents a principled and practical approach to ensuring the trustworthiness of semantics-based language frameworks through proof generation. By producing matching logic proof objects for each task and checking them with a minimal trusted proof checker, the approach provides strong correctness guarantees while accommodating the complexity and evolution of the underlying framework. The evaluation on the IMP language demonstrates feasibility, and the theoretical analysis establishes the soundness and completeness of the approach. The work is significant both as a contribution to formal methods -- showing how to make language frameworks trustworthy -- and as a foundational technology for verifiable computing applications in blockchain, smart contracts, and beyond.