One-sentence Summary

René Thiemann's chapter surveys and contrasts the two principal approaches, certification and verification, for integrating automatic deduction tools such as theorem provers, SAT/SMT solvers, and termination analyzers with proof assistants, and reviews several successful applications of these methods.

Key Contributions

• The chapter reviews and compares certification and verification approaches for connecting automatic deduction tools (SAT, SMT, termination analyzers) with proof assistants.
• Verified certifiers have detected bugs in deduction tool implementations that had gone unnoticed for years, and they are now used to validate a large number of automatically generated proofs in tool competitions.
• Formal verification of core deduction techniques has corrected faulty published proofs and enabled safe exploration of extensions, and a verified SAT solver (IsaSAT) outperformed unverified competitors in the EDA-Challenge 2021.

Introduction

The authors examine the interplay between proof assistants and automatic deduction tools such as SAT, SMT, and termination analyzers. Reliable automation is critical for verifying complex properties, but manual certification of these tools’ outputs is error-prone, inefficient, and fails to scale beyond toy examples. The authors show how proof assistants can formally verify the inference rules and termination orderings that underlie deduction tools, using the lexicographic path ordering (LPO) and recursive path ordering with status (RPO) as a running example. This formal treatment not only increases the trustworthiness of automated reasoners—verified certifiers have uncovered long‑hidden bugs—but also allows developers to safely modify or extend core inference rules without fear of introducing errors.

Method

The authors propose certification as a method to validate results from unreliable deduction tools. To address the need for high reliability, they leverage proof assistants, which possess a small trusted code base. This approach allows for the formal verification of both the soundness of applied techniques and the correctness of their application.

One primary workflow is certification via proof script generation. As shown in the figure below:

This process involves three main steps. First, the authors develop a library that formalizes domain-specific notions and theorems, such as strong normalization and term rewriting, without including specific inputs. Second, a proof script generator transforms a given input certificate into a proof script for the proof assistant. This script defines the property of interest and provides a formal proof by encoding the certificate's proof. Third, the proof assistant checks the script. The generator can handle certificates in different ways: it can translate inference trees from extended certificates into introduction rules, reconstruct trees from basic certificates, or invoke tailor-made tactics. Alternatively, a deep embedding can be used to implement a verified algorithm within the proof assistant to ensure the ordering relation $\succ_r$≻r​ holds for all rules.

However, proof script generation can be slow due to the overhead of running the proof assistant. To address this, the authors introduce an alternative workflow: external certification. This method is applicable when proof scripts consist mainly of invoking verified algorithms that provide sufficient criteria for the desired property.

As shown in the figure below:

In this external certification workflow, the initial library development remains the same. The second step involves providing verified algorithms for each supported property and certificate type. These algorithms are proven to be sufficient conditions (e.g., if the algorithm accepts input $I$I and certificate $C$C, then property $P(I)$P(I) holds) and are exported into an executable program. The final step runs this executable program on the inputs and certificates, using a wrapper to select the appropriate algorithm.

External certification is significantly faster than the proof script approach, allowing more certificates to be handled in reasonable time, especially for tasks requiring heavy computations. To ensure efficiency, the authors often use a refinement approach, proving an abstract algorithm correct and then refining it into an executable version with efficient data structures. While external certification is less brittle to changes in the proof assistant, it has a larger trusted code base because it relies on the code generator and external compiler, and it precludes certain design decisions like creating specific datatypes for signatures.