# Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture

arXiv: https://arxiv.org/abs/2605.16407 · HTML: https://mlsanity.com/paper/2605.16407/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 63 references that are in the map.
- First posted on arXiv 13 May 2026.

## Builds on (most cited first, 12 of 12)

- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [Universal and Transferable Adversarial Attacks on Aligned Language Models](https://mlsanity.com/paper/2307.15043/) (2023)
- [Retrieval-Augmented Generation for Large Language Models: A Survey](https://mlsanity.com/paper/2312.10997/) (2023)
- [A Survey on Hallucination in Large Language Models: Principles, Taxonomy, Challenges, and Open Questions](https://mlsanity.com/paper/2311.05232/) (2023)
- [Sparse Autoencoders Find Highly Interpretable Features in Language Models](https://mlsanity.com/paper/2309.08600/) (2023)
- [Ignore Previous Prompt: Attack Techniques For Language Models](https://mlsanity.com/paper/2211.09527/) (2022)
- [Measuring Faithfulness in Chain-of-Thought Reasoning](https://mlsanity.com/paper/2307.13702/) (2023)
- [Conformal Language Modeling](https://mlsanity.com/paper/2306.10193/) (2023)
- [Attributed Question Answering: Evaluation and Modeling for Attributed Large Language Models](https://mlsanity.com/paper/2212.08037/) (2022)
- [NLP Verification: Towards a General Methodology for Certifying Robustness](https://mlsanity.com/paper/2403.10144/) (2024)
- [Lean4Lean: Verifying a Typechecker for Lean, in Lean](https://mlsanity.com/paper/2403.14064/) (2024)
- [Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline](https://mlsanity.com/paper/2604.18882/) (2026)

## Built on by (most cited first, 2 of 2)

- [When May an Agent Stop? Evidence-Carrying Termination for Tool-Using LLMs](https://mlsanity.com/paper/2608.23623/) (2026)
- [PAGR: Proof-Carrying Algebraic-Geometric Retrieval: A Quiver-, Provenance-, and Sheaf-Theoretic Framework for Grounded LLM Retrieval](https://mlsanity.com/paper/2609.06127/) (2026)

## Abstract (arXiv)

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.