Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture
George Koomullil
cs.LO
May 13, 2026 · v1
TL;DR
Extends a Lean 4 trust-boundary architecture producing kernel-type-checked certificates for LLM pipelines.
Abstract
We present a framework for verifying the deterministic structured computations surrounding a large language model rather than the model itself, extending a Lean 4 trust-boundary architecture to the generic interfaces of modern LLM pipelines. Certificate validity is a Lean 4 kernel type-check plus a sorry-free transitive axiom audit against the trusted set {propext, Classical.choice, Quot.sound}; other assumptions are declared and partitioned by tier (mathematical placeholders, cryptographic assumptions, ML/human oracles). The technical contribution comprises three local certificate families and two operators. The families are conflict-aware bilattice grounding (with an emission-gate soundness lemma), embedding sensitivity and paraphrase stability, and Hoare-style agent action. The operators are a Maximal Certifiable Residue, which turns abstention into the maximum-weight certifiable residue with audit-logged dropped claims, and a Compositional Stability theorem, which yields a closed-form pipeline-wide perturbation budget from per-layer gains and margins. The three families plus a Universal Assurance Card consolidator form the per-call deliverable for high-stakes deployments: patent and legal retrieval, regulated finance, clinical decision support, and agentic systems with irreversible side effects. A compiled Lean 4 reference artifact (Lean v4.30.0-rc2, Mathlib) covers all 22 certificate types, with 17 of 46 kernel-audited declarations axiom-free, the rest depending only on the trusted set and declared assumptions, and zero uses of sorryAx or Lean.ofReduceBool. The three families are empirically tested through four registered pilots: bilattice grounding on adversarially perturbed HotpotQA, embedding sensitivity in short- and long-form settings, and Hoare-style agent action on a filesystem sandbox with adversarial prompt injection.
Problem
LLM pipelines produce probabilistic outputs without audit-grade guarantees. Embedding similarities can be unstable under paraphrase, grounding can miss contradictions, and agent actions may be semantically unsafe. No existing framework provides machine-checkable certificates for the structured computations surrounding an LLM.
Approach
A Lean 4 trust-boundary architecture is extended to generic LLM pipeline interfaces. Three local certificate families are formalized: conflict-aware bilattice grounding (with emission-gate soundness), embedding sensitivity and paraphrase stability, and Hoare-style agent action. Two operators are provided: Maximal Certifiable Residue (turning abstention into maximum-weight certifiable output) and a Compositional Stability theorem yielding a closed-form pipeline-wide perturbation budget.
Results
A compiled Lean 4 reference artifact (v4.30.0-rc2, Mathlib) covers all 22 certificate types. 17 of 46 kernel-audited declarations are axiom-free; the rest depend only on the trusted set {propext, Classical.choice, Quot.sound} and declared assumptions, with zero uses of sorryAx. Four registered pilots test the families on adversarially perturbed HotpotQA, embedding sensitivity settings, and a filesystem sandbox with adversarial prompt injection.
