Making Formal Verification Trustworthy via Proof Generation

Formal deductive verification aims at proving the correctness of programs via logical deduction. However, the fact that it is usually based on complex program logics makes it error-prone to implement. This paper addresses the important research question of how we can make a deductive verifier trustworthy through a practical approach. We propose a novel technique to generate machine-checkable proof objects to certify each verification task performed by the language-agnostic deductive verifier of K—a semanticsbased language framework. These proof objects encode formal proofs in matching logic—the logical foundation of K. They have a small 240-line trust base and can be directly verified by third-party proof checkers. Our preliminary experiments show promising performance in generating correctness proofs for deductive verification in different programming languages.