doc-verification-bridge: Theorem classification for specification-implementation refinement

About this technology

Overview

Doc-verification-bridge is a semantic documentation and verification coverage tool for Lean 4 that automatically classifies theorems according to their role in specification-implementation refinement. The tool addresses a critical gap in verified software development: while proof assistants guarantee that individual theorems are correct, they provide no systematic way to assess whether a specification is completely verified or to navigate the relationships between mathematical specifications and computational implementations. The software implements a Four-Category Ontology inspired by E.J. Lowe's metaphysical framework, organizing declarations into Mathematical Abstractions, Computational Datatypes, Mathematical Definitions, and Computational Operations. This categorization directly maps to the concerns of specification-implementation correspondence: proving that computable Bool-returning functions correctly decide Prop-valued mathematical predicates. The core contribution is automatic inference of semantic classification from theorem types. By analyzing the structure of hypotheses and conclusions, the tool identifies what each theorem assumes, proves, and validates-distinguishing bridging theorems (which connect specifications to implementations) from mathematical properties (internal to the specification layer) and computational properties (internal to the implementation layer). Bridging theorems are further classified by directionality: soundness proofs show implementations are conservative; completeness proofs show implementations are exhaustive. Doc-verification-bridge operates in two modes: automatic mode requires no source modifications and is suitable for analyzing existing codebases; manual mode provides precise control through Lean 4 attributes for production documentation. The software generates MkDocs-compatible documentation integrated with doc-gen4 API reference, enabling unified navigation between "what does this function do?" and "how do we know it's correct?" The tool is designed for safety-critical domains such as autonomous systems, where systematic verification coverage tracking is essential for regulatory compliance and assurance argumentation.