Boundary Discipline: Failure Modes in Chiplet-Scale Formal Verification

This document presents a mathematical framework for GPU verification that distin-guishes two fundamentally different types of abstraction boundary: algebraic boundaries,which are intrinsic to formal systems and across which correctness transfers by proof, andgeometric boundaries, which mark the interface between formal models and external realityand across which correctness requires empirical warrant. This distinction, grounded in thedifference between boundary operators in chain complexes and topological boundaries de-fined by closure operations, explains why verification claims compose reliably within formaldomains but fail unpredictably at model-world interfaces.The framework develops the algebraic structure of verification domains as a categorywith refinement morphisms, characterises the obstruction to extending this structure acrossgeometric boundaries, and derives adequacy criteria for warrant transfer at each boundarytype. Beyond the core functional verification boundaries, the framework addresses addi-tional boundary types that arise in industrial practice: specification boundaries (betweenarchitectural intent and formal models), toolchain boundaries (between verification theoryand tool implementation), temporal boundaries (between initial correctness and long-termreliability), information boundaries (between logical correctness and side-channel security),protocol boundaries (between standardised interface specifications and physical implementa-tions), heterogeneous composition boundaries (between independently verified componentswith different verification histories), configuration boundaries (between verified and deployedparameter settings), and supply chain boundaries (between verification artifacts from dif-ferent organisations). The result is a comprehensive account of what formal verificationcan and cannot establish, with particular application to chiplet-based GPU architectureswhere modular verification strategies depend critically on boundary discipline at inter-dieinterfaces.