Causal Inference

The branch of statistics and computer science that develops formal apparatus for reasoning about causes rather than mere associations: when can we conclude from observational or interventional data that X causes Y, that intervening on X would shift Y, or that Y would have been different had X been different? Two complementary traditions: Pearl’s graphical / structural-causal-model framework (DAGs + the do-Calculus + the ID Algorithm) and Rubin’s counterfactual / potential-outcomes framework (ignorability + positivity + propensity-score / IV / matching estimators). Formal mappings between the two are now standard (Pearl–Bareinboim 2009). For CBCL / CIVeX, causal inference is the substrate: CIVeX certificates carry causal DAGs and identifiability proofs, checked rather than re-derived — the causal analogue of PCC.

In this vault

Causal Diagrams for Empirical Research - Pearl — Pearl 1995, the modern graphical framework
Causality - Pearl — Pearl 2000/2009 textbook
Identification of Joint Interventional Distributions - Shpitser Pearl — complete ID algorithm
Potential Outcomes Framework - Rubin — Rubin 1974, the counterfactual framework
do-Calculus
Backdoor Criterion
Front-door Criterion
Structural Causal Model
Counterfactual
Identifiability
Causal DAG
Instrumental Variable
Mediation Analysis
Causal Influence of Communication
Causal Threat Graph
Causal Broadcast
CBCL - Safe Self-Extending Agent Communication

Backlinks

Linked Pages

CBCL - Safe Self-Extending Agent Communication

CBCL: Safe Self-Extending Agent Communication

Reference: O’Connor, H. (2026). LangSec Workshop, IEEE Security and Privacy Workshops (SPW 2026). arXiv:2604.14512v1 [cs.CR], 16 Apr 2026. Source file: oconnor-cbcl-langsec26.pdf. URL. Reference implementation: https://codeberg.org/anuna/cbcl-rs.

Summary

Building on McCarthy’s 1975/1982 Common Business Communication Language vision and the language-theoretic security programme of Sassaman, Patterson, Bratus and Locasto (Security Applications Of Formal Language Theory), this paper presents a contemporary CBCL: an agent communication language designed so that all messages — including runtime language extensions — remain within the deterministic context-free (DCFL) complexity class. The motivating diagnosis is that contemporary agent communication has slid up the Chomsky hierarchy without acknowledging the security cost: KQML and FIPA-ACL are CFL with informal extensibility, but MCP and LLM-based agent frameworks operate over inputs whose effective complexity is recursively-enumerable, where the validity of an arbitrary message is undecidable and “weird machines” (Exploit Programming - From Buffer Overflows To Weird Machines) become unavoidable. CBCL takes the opposite tack: minimal core (8 performatives — tell, ask, reply, hello, bye, ok, error, cancel) plus a homoiconic dialect mechanism that lets agents define, transmit, and adopt domain-specific vocabularies as first-class CBCL messages, with three machine-checked safety invariants — R1 (no recursion in dialect templates), R2 (declared resource bounds on depth, expansion size, verification time), R3 (core-vocabulary preservation) — that together guarantee DCFL preservation under arbitrary finite sequences of dialect installations.

The paper accompanies the design with a Lean 4 formalization (≈5,400 lines, 16 modules, 176 machine-checked theorems, zero sorry gaps, no custom axioms) covering parser correctness (soundness + completeness), R1–R3 verification, pipeline totality, and the central dcfl_preserved closure theorem; a verified parser binary cbcl-parse is extracted from the proofs. A separately-developed Rust reference implementation (cbcl-rs, ≈11,000 lines, no_std-compatible core) ships a hand-rolled O(n) parser, dialect verification engine, gossip-based dialect propagation (O(log n) convergence per Demers et al.), C FFI/WASM bindings, property-based and differential tests, and cargo-fuzz targets; differential tests cross-validate the Rust parser against the Lean-extracted binary, eliminating spec-implementation parser differentials. Five example dialects (precision agriculture, AI planning, cross-chain asset transfer, artifact management, email) are R1–R3-verified end-to-end. A draft IETF Internet-Draft specifying application/cbcl and a Nostr transport binding (cbcl-nostr) accompany the paper. The Discussion explicitly aligns the design with Singh’s social-agency programme: dialect installation is treated as a public commitment to the dialect’s declared semantics — semantic divergence becomes a breach of commitment, observable and accountable, rather than a hidden failure of shared mental state — sidestepping the unverifiable mentalistic semantics critique of Verifiable Semantics for ACLs.

Implementation status (post-paper, cbcl-rs). The reference implementation has shipped two further safety invariants the paper sketches as future work, plus a richer Lean formalisation: R4 (Integrity) — Ed25519-style signatures over canonical encodings via an algorithm-agnostic Signer trait, with three-valued install verdicts (Valid / Unsigned / Invalid) — and R5 (Contract Well-formedness) — optional (protocol …) and (shape …) clauses on a dialect, expressing causal Merkle DAG protocols and per-performative shape contracts; R5 enforces acyclicity, reachability from begin, performative definedness with ancestor closure for extends, step uniqueness, and depth-bound respect, all decidable in linear fuel at install time. The §VII-D structural-contracts vision is therefore live (SPEC-002, SPEC-003): verify_monotone, verify_all_is_meet, and verify_eventually_consistent are proved theorems showing causal-protocol verification is a lattice homomorphism that joins coordination-free under G-Set store merge — explicit CALM Theorem alignment. The Lean codebase has grown to 380+ declarations across 19 files (still zero sorry, only the standard axioms propext / Classical.choice / Quot.sound); the workspace ships 837 tests including 584 cbcl-core unit tests, 37 proptest cases, 21 differential integration tests against the Lean-extracted binary, libFuzzer harnesses, and cargo-mutants mutation testing at a 90% kill threshold. The crate layout has grown from the paper’s five to seven: the original cbcl-core / cbcl-parser / cbcl-cli / cbcl-wasm / cbcl-ffi plus cbcl-erl (Erlang/LFE binding, SPEC-009 — with SPEC-010 binding-conformance suite) and cbcl-arena (Agent Arena platform, SPEC-012 — composable referee on cbcl-lfe-router with capability-keyed message routing and signed receipt logs). A worked sealed-bid auction dialect (SPEC-004) demonstrates structural defence against false-claim manipulation — concrete evidence that the R5 contract layer is rich enough to encode mechanism-design integrity properties decidably. The earlier Scheme prototype (anuna-research/cbcl) is superseded; architecture decisions live as ADRs under .hence/ (purity boundary, parser library choice, error handling, WASM API surface, R4 adversarial review).

Key Ideas

DCFL as the Goldilocks complexity class: Regular is too weak for nested envelopes/dialects; general CFL admits ambiguous grammars and parser-differential attacks; context-sensitive is PSPACE-complete; Type-0 is undecidable. DCFL is the minimal class that supports nested structure with class-level unambiguity (parser equivalence under language evolution).
Homoiconic self-extension: Dialect definitions are themselves valid CBCL messages, parsed by the same recogniser used for ordinary communication — a single attack surface, no separate meta-language. Inspired by Racket’s #lang mechanism.
Three safety invariants R1–R3: declarative pattern-template substitution only (no recursion, no iteration, no reflection); declared resource bounds (depth ≤ 64, expansion ≤ 8192 chars, verification ≤ 1000 ms); the eight core performatives cannot be redefined.
DCFL preservation theorem: dialect invocations must appear inside a (lang name …) wrapper; the lang tag plus a unique dialect name forms a prefix-free partition that lets a deterministic pushdown automaton dispatch to the appropriate subgrammar without extra lookahead — circumventing the fact that DCFLs are not closed under union in general. Mechanised in Lean 4 as dcfl_preserved.
Lean 4 formalization with extraction: 176 theorems, 0 sorry gaps, no custom axioms; the verified parser binary cbcl-parse is extracted from the proofs and runs the same fuel-bounded recursive-descent parser as the model.
Rust reference implementation: cbcl-core (no_std, no unsafe), cbcl-parser, cbcl-cli, cbcl-ffi, cbcl-wasm. Differential tests against the Lean-extracted binary; cargo-fuzz over five entry points.
Eight core performatives (tell, ask, reply, hello, bye, ok, error, cancel) plus four message categories (simple, meta, lang-scoped, wrapped); keyword parameters in Common-Lisp style (:thread, :in-reply-to).
Single-pass template expansion: terminates in time linear in the template plus argument size; not Turing-complete; output is not fed back into the expander, ruling out unbounded re-expansion.
Epidemic dialect propagation: gossip-based with Demers et al.’s O(log n) convergence bound; agents independently verify R1–R3 and signatures before installing.
Canonical serialization per RFC 9804 for cryptographic operations — deterministic byte representation as a precondition for signature verification.
Dialect identity by content hash: name collisions resolved by canonical-form hash; downgrade attacks rejected at installation.
Self-expression vs self-adaptation (Zambonelli et al.): traditional ACLs support only parameter tuning within fixed structure; CBCL is a self-expressive protocol whose vocabulary structurally evolves under safety constraints.
Singh-aligned reading of dialect installation: a public commitment to declared semantics, with :examples clauses providing machine-checkable behavioural anchors — semantic divergence as observable breach rather than hidden mental-state mismatch.
Stated limitations: DCFL ceiling means no recursive transformations, no cross-field references (e.g. checksums over fields), no aggregation over variable-length collections, no context-sensitive validation. Standish-taxonomy paraphrastic only — no Orthophrase, no Metaphrase. Trust infrastructure (key distribution, revocation) and dialect-curation policy left to deployment.
Structural-contracts extension (sketched in §VII-D, shipped post-paper as R4 + R5): Ed25519-style dialect signatures plus protocol constraints as causal Merkle DAGs over performative-typed messages, with Visibly Pushdown Languages for shape constraints and coordination-free monotonic verification over an append-only store. Lean-mechanised lattice-homomorphism theorems (verify_monotone, verify_all_is_meet, verify_eventually_consistent) establish that replica verdicts join under G-Set merge.

Connections

Common Business Communication Language — McCarthy’s 1975/1982 origin; CBCL is the formally-verified realisation of that vision.
Security Applications Of Formal Language Theory — Sassaman et al.’s LangSec foundations.
Proof-Carrying Code - Necula — Necula 1997, the architectural ancestor of CBCL’s R4 split (host runs a small certified verifier; producer ships the proof).
Enforceable Security Policies - Schneider — Schneider 2000, the formal warrant for R5 monotone-verdict trace monitoring.
An Axiomatic Basis for Computer Programming - Hoare — Hoare 1969, root of the contract-based verification line CBCL inherits.
Authentication in Distributed Systems - Lampson Abadi Burrows Wobber — Lampson et al. 1992, the Speaks-For Calculus for delegated commitments.
Articulating Reasons - Brandom — Brandom 2000, the philosophical underwriting of Public Semantics (entry point).
Making It Explicit - Brandom — Brandom 1994, the full inferentialist treatise.
Empiricism and the Philosophy of Mind - Sellars — Sellars 1956, the Myth of the Given that makes Semantics-Without-Minds possible.
Philosophical Investigations - Wittgenstein — Wittgenstein 1953, Meaning As Use / language-games / rule-following.
Two Dogmas of Empiricism - Quine — Quine 1951, Semantic Holism.
Assertion - Stalnaker — Stalnaker 1978, Common Ground update semantics — operational analogue of CBCL’s verdict ledger.
Languages and Language - Lewis — Lewis 1975, Convention of Truthfulness picture of how an abstract language gets in force in a population.
Communicative Actions for Artificial Agents - Cohen Levesque — Cohen & Levesque 1995, the Mentalistic Semantics high-water mark CBCL deliberately is not.
FIPA-ACL Specifications — the engineering of FIPA-ACL (envelope, conversation-id, ontology slot) CBCL inherits; the semantics it replaces.
An Ontology for Commitments in Multiagent Systems - Singh — Singh 1999, the formal commitment ontology CBCL’s dialect contracts instantiate.
Jones-Sergot Normative Systems — Jones & Sergot 1993, the Counts-As Relation that gives wire events institutional meaning under a dialect contract.
Exploit Programming - From Buffer Overflows To Weird Machines — weird-machine analysis CBCL is designed to preclude at the parser layer.
PKI Layer Cake - Kaminsky Patterson Sassaman — concrete parser-differential attacks; CBCL’s class-level unambiguity rules these out at the grammar level.
The Halting Problems of Network Stack Insecurity
A Language-Based Approach To Prevent DDoS
LangSec
KQML as an Agent Communication Language
KQML - A Language And Protocol For Knowledge And Information Exchange
FIPA-ACL
ACL Rethinking Principles — Singh’s social-agency critique that CBCL’s “dialect installation as public commitment” inherits.
Agent Communication Languages - Rethinking the Principles
Verifiable Semantics for ACLs
A Common Ontology Of ACLs
Commitment-based Semantics
The State of the Art in Agent Communication Languages
Trends in Agent Communication Language
Toward Principles for the Design of Ontologies Used for Knowledge Sharing — Gruber’s ontological-commitment principle CBCL inherits.
Some Philosophical Problems from the Standpoint of Artificial Intelligence — McCarthy & Hayes’s representation/computation separation.
Elephant 2000 - A Programming Language Based on Speech Acts — McCarthy’s intra-program speech-act counterpart to CBCL’s inter-organisational vision.
Adjectival Modifiers
S-expression
Homoiconicity
Code as Data
Creating Languages in Racket — Flatt’s #lang mechanism that inspired CBCL’s homoiconic self-extension.
Extensibility in Programming Language Design - Standish
Language Extensibility Taxonomy
Paraphrase
Orthophrase
Metaphrase
Self-Expression
Self-Adaptation Self-Expression Self-Awareness ASCENS
Dialects and Idiolects
Keeping CALM - When Distributed Consistency is Easy — CALM theorem underwriting the forthcoming coordination-free contracts extension.
Visibly Pushdown Languages
MCP Landscape Security Threats And Future Research Directions
Survey Of AI Agent Protocols
Survey Of Agent Interoperability Protocols
ClawWorm Self-Propagating Attacks Across LLM Agent Ecosystems — concrete LLM-agent worm whose root-cause analysis CBCL’s lang-scoped provenance addresses.
Why AI Agents Communicate In Human Language
Why Do Multi-Agent LLM Systems Fail
Gossiping in Distributed Systems
Gossip-based Aggregation in Large Dynamic Networks

Conceptual Contribution

Claim: Agent communication languages can be simultaneously expressive, runtime-extensible, and tractably verifiable iff every message — including those that extend the language — is constrained to the deterministic context-free language class; this constraint is compatible with first-class self-extension, can be machine-checked end-to-end, and converts the unverifiable-mental-state problem of mentalistic ACLs into a public-commitment problem at the protocol layer.
Mechanism: Eight-performative core grammar (LL(1), DCFL); homoiconic dialect mechanism — dialect definitions are valid CBCL messages with extend clauses describing pattern-template substitutions; three safety invariants R1–R3 enforced at installation (no recursion via DFS cycle detection, declared resource bounds, core-vocabulary preservation); (lang name …) wrapper providing prefix-free deterministic dispatch into per-dialect sub-grammars so the union remains DCFL. Lean 4 formalization (LeanCbcl, ~5,400 LoC, 176 theorems) covering parser soundness/completeness, R1–R3, pipeline totality, and dcfl_preserved; verified parser extracted to a runnable binary (cbcl-parse). Rust reference implementation (cbcl-rs, ~11,000 LoC) with a ResourceContext-tracked single-pass expander, gossip-based dialect propagation (O(log n) per Demers et al.), canonical RFC-9804 serialization for signing, algorithm-agnostic Signer trait, C FFI / WASM bindings, property-based + differential tests, fuzz targets. Draft IETF application/cbcl Internet-Draft and Nostr transport binding.
Concepts introduced/used: Deterministic Context-Free Language, LangSec, Homoiconicity, S-expression, Dialects and Idiolects, Performatives, Self-Expression, Paraphrase, Orthophrase, Metaphrase, Visibly Pushdown Languages, CALM Theorem, Commitment-based Semantics, Public Semantics, Verifiable Semantics, Adjectival Modifiers, Ontological Commitment, Lean 4, Property-Based Testing, Parser Differential Attack, Weird Machine, Gossip Protocols, Canonical Serialization, Nostr, hence
Stance: engineering / formal-methods, with explicit position-taking on the agent-communication design space
Relates to: Realises McCarthy’s Common Business Communication Language vision (1975/1982) by giving formal safety guarantees McCarthy could only gesture at. Sits squarely in the LangSec programme of Security Applications Of Formal Language Theory and Exploit Programming - From Buffer Overflows To Weird Machines, extending it from input-validation analysis to protocol design — claiming, plausibly, to be the first ACL designed from LangSec principles and the first to demonstrate that LangSec is compatible with runtime self-extension. Inherits the DCFL-vs-ambiguous-CFG argument from PKI Layer Cake - Kaminsky Patterson Sassaman and applies it at the message layer rather than the certificate layer. Builds explicitly on Singh’s social-agency critique (ACL Rethinking Principles) and Wooldridge’s verifiability programme (Verifiable Semantics for ACLs) by treating dialect installation as a public commitment whose semantics are anchored by the :examples clause — a machine-checkable analogue of the commitment-trace conformance that Flexible Protocol Specification and Execution (Yolum & Singh) and Commitment Machines - Yolum and Singh establish for protocol actions. Where Pact - A Choreographic Language for Agentic Ecosystems takes the individual-rationality fork to answer “why follow a protocol?”, CBCL takes the publicness/verifiability fork: the meaning of a message is fully determined by the formal grammar plus declared semantics, with no mental-state inference required. Inherits Gruber’s ontological-commitment architecture but replaces “out-of-band agreement” with in-protocol propose/query/teach. The extensibility design draws on Creating Languages in Racket (Flatt’s #lang) and respects the boundary set by Extensibility in Programming Language Design - Standish: paraphrastic only, deliberately excluding orthophrase/metaphrase to keep the attack surface bounded. The forthcoming structural-contracts extension uses Visibly Pushdown Languages for shape constraints and the CALM Theorem for coordination-free verification — a natural bridge to commitment-machine semantics. The LLM-agent threat-model framing (ClawWorm Self-Propagating Attacks Across LLM Agent Ecosystems, MCP Landscape Security Threats And Future Research Directions) positions CBCL as the structural alternative to MCP/JSON-RPC-with-natural-language: same extensibility, vastly tighter security envelope.

Causal Broadcast

A delivery discipline for distributed message-passing systems in which, if message m₁ causally precedes message m₂ (in the Lamport happened-before sense), then every recipient delivers m₁ before m₂. Birman and Joseph (1987) introduced the formalism in the ISIS toolkit; it is the standard prerequisite for op-based CRDTs (commutative operations need only commute pairwise given causal ordering) and the runtime correctness condition that makes a Merkle DAG of :caused-by references soundly executable. Causal broadcast is strictly weaker than total-order broadcast (it permits concurrent messages to be delivered in different orders at different recipients) and strictly stronger than FIFO (it respects cross-channel causality, not just per-channel sequence).

In this vault

Causal Threat Graph

SoK construct: a directed graph capturing how a single vulnerability cascades into downstream agentic harms — used for systematic attack-surface analysis.

In this vault

SoK The Attack Surface of Agentic AI

Causal Influence of Communication

Causal-intervention metric quantifying how much a message changed the recipient’s action distribution — a robust alternative to correlational measures.

In this vault

On the Pitfalls of Measuring Emergent Communication

Mediation Analysis

Decomposition of a total causal effect into direct and indirect components routed through one or more mediator variables; Pearl/Robins natural and controlled direct effects.

In this vault

Instrumental Variable

Variable that influences treatment but only affects outcome via treatment, and is independent of confounders. Classical econometric identification strategy under unobserved confounding.

In this vault

Causal DAG

Directed acyclic graph whose nodes are variables and whose edges encode direct causal influence. Substrate for d-Separation, Backdoor Criterion, Front-door Criterion, and the Structural Causal Model framework.

In this vault

Identifiability

In causal inference, a causal query — most commonly an interventional distribution P(Y | do(X = x)) — is identifiable from observational data over a variable set V iff it can be written as an expression in the observational distribution P(V). Identifiability is a graphical property: it depends only on the causal DAG, not on the parametric form of the distribution. Pearl’s Backdoor Criterion and Front-door Criterion give sufficient graphical conditions; Shpitser–Pearl 2006’s ID algorithm is sound and complete for identification — it finds an expression if and only if one exists. The Rubin / potential-outcomes counterpart uses the Ignorability + Positivity conditions to characterise when standardisation by covariates yields the average treatment effect. For CIVeX-style certificates, identifiability is the property the certificate establishes — the prover ships the DAG, assumptions, and ID derivation; the host checks the derivation rather than re-running the algorithm.

In this vault

Counterfactual

A statement about what would have happened had things been otherwise; central to causal reasoning and to McCarthy’s programme of representing actions formally.

In this vault

Some Philosophical Problems from the Standpoint of Artificial Intelligence

Structural Causal Model

Pearl’s framework for causal reasoning: a set of structural equations + a Causal DAG over endogenous and exogenous variables, supporting observational, interventional, and counterfactual queries via the three-rung ladder of causation.

In this vault

Front-door Criterion

Pearl’s alternative identification strategy when no admissible backdoor set is observable: route causal effect through a fully mediating variable that is itself unconfounded with the outcome. Surprising and powerful.

In this vault

Backdoor Criterion

Pearl’s graph-theoretic condition for identifying a sufficient adjustment set in a Causal DAG: block every non-causal path from treatment to outcome while opening no collider. Workhorse of observational causal inference.

In this vault

do-Calculus

Pearl’s three-rule deductive system for transforming expressions involving the do-operator — the formal representation of intervention in causal models. The three rules are: (R1) insertion / deletion of observations under appropriate d-separation in the modified graph; (R2) action / observation exchange when an action behaves like an observation under d-separation; (R3) insertion / deletion of actions when no causal paths exist. Together with the probability axioms, do-calculus is complete for non-parametric identification of interventional distributions (Shpitser–Pearl 2006): every identifiable effect is derivable by the three rules, and every unidentifiable effect is provably so. The do-calculus is essentially the rule-set the ID Algorithm mechanises into an automated decision procedure.

In this vault

Potential Outcomes Framework - Rubin

Estimating Causal Effects of Treatments in Randomized and Nonrandomized Studies

Reference: Rubin, D. B. (1974). Estimating Causal Effects of Treatments in Randomized and Nonrandomized Studies. Journal of Educational Psychology 66(5): 688–701. October 1974. APA PsycNet record (DOI 10.1037/h0037350) · ERIC index entry · See also Rubin’s later book with Imbens, Causal Inference for Statistics, Social, and Biomedical Sciences (Cambridge UP 2015) for the canonical textbook statement.

Summary

Rubin’s 1974 paper is the founding statement of the potential-outcomes framework (a.k.a. the Rubin causal model) — the alternative to Pearl’s graphical apparatus that has dominated statistics, econometrics, and biomedical inference. The central move: rather than thinking of causation in terms of mechanisms or structural equations, define a causal effect counterfactually. For each unit i and each treatment level t, posit a potential outcome Yᵢ(t) — the outcome unit i would have exhibited under treatment t. The unit-level causal effect of treatment t versus control c is Yᵢ(t) − Yᵢ(c). The fundamental problem of causal inference is that only one of Yᵢ(t) and Yᵢ(c) is ever observed for any single unit — the other is counterfactual. Causal inference is then statistical inference about the unobserved counterfactual.

The framework’s payoff comes from clarifying the role of randomization. Under random assignment to treatment, observed and counterfactual outcomes are exchangeable: the distribution of Yᵢ(t) in the treated group equals the distribution that would have obtained in the control group had they been treated. The average treatment effect (ATE) E[Y(t) − Y(c)] is then estimable as the simple difference in group means. The framework also clarifies what observational data lets us do: under stated ignorability (a.k.a. conditional exchangeability, no unmeasured confounders) and positivity assumptions, the ATE is identifiable by covariate adjustment — the same calculation Pearl’s backdoor adjustment formula yields, derived from the counterfactual side. Subsequent work (Rosenbaum–Rubin propensity scores 1983, matching, Imbens–Angrist instrumental-variables 1994) builds out the estimation toolbox.

The framework is now the dominant language of causal inference in applied statistics. For CBCL / CIVeX, knowing both languages matters: a CIVeX certificate may be written in either graphical or potential-outcomes notation, and the verifier may need to translate between them. The formal equivalence is established by Pearl–Bareinboim 2009 and Pearl 2010: any non-parametric causal effect expressible in one framework is expressible in the other under translation; the languages differ in ergonomics (graphs make assumptions visually inspectable; potential outcomes make assumptions algebraically inspectable) rather than expressive power. The paper is the place to cite to acknowledge the other half of the causal toolkit.

Key Ideas

Potential outcomes: for each unit i and treatment level t, posit Yᵢ(t) — the outcome unit i would exhibit under t. Both Yᵢ(treated) and Yᵢ(control) are well-defined, but only one is observed for any given unit.
Unit-level causal effect: Yᵢ(t) − Yᵢ(c). Defined for each unit, even though typically unobservable.
Fundamental problem of causal inference: only one potential outcome per unit is observable. Causal inference is statistical inference about the unobserved counterfactual.
SUTVA (Stable Unit-Treatment Value Assumption): implicit in defining Yᵢ(t) as a function of unit and treatment only — (i) no interference between units, and (ii) no multiple versions of treatment. SUTVA violations (peer effects, network spillovers, treatment heterogeneity) require explicit extension.
Ignorability / Conditional Exchangeability: (Y(t), Y(c)) ⫫ T | X — given covariates X, treatment assignment is independent of potential outcomes. The non-graphical statement of “no unmeasured confounders”.
Positivity / Common Support: 0 < P(T = t | X = x) < 1 for all x in the support. Required for ATE identification — must have some chance of either treatment at every covariate level.
Randomization: random assignment of T independent of (Y(t), Y(c)) makes ignorability hold without conditioning. The methodological justification for randomized experiments.
Average Treatment Effect (ATE): E[Y(t) − Y(c)]. The standard target estimand. Identifiable under ignorability + positivity by standardization (covariate adjustment), which yields the same formula as Pearl’s backdoor adjustment.
Successors: propensity score (Rosenbaum–Rubin 1983), matching, instrumental variables (Imbens–Angrist 1994), the Local Average Treatment Effect (LATE), doubly-robust estimation, the entire modern econometric/biostatistical causal-inference toolbox.

Connections

Conceptual Contribution

Claim: Causal effects can be defined and estimated by positing potential outcomes Yᵢ(t) for each unit-treatment pair and treating causal inference as statistical inference about unobserved counterfactuals. Random assignment guarantees identifiability of average effects without further assumptions; observational data require ignorability (no unmeasured confounders) and positivity (common support).
Mechanism: For each unit i and treatment level t, define Yᵢ(t) as the outcome i would exhibit under t. The fundamental problem: only one Yᵢ(t) is observed per unit. Define the unit-level effect Yᵢ(t) − Yᵢ(c) and population estimands (ATE, ATT). Identify the ATE under random assignment without further assumption; under observational data with measured covariates X, identify under ignorability (Y(t), Y(c)) ⫫ T | X and positivity. Estimate by direct standardization, propensity-score adjustment, matching, or instrumental variables when assumptions fail.
Concepts introduced/used: Potential Outcomes, Rubin Causal Model, Counterfactual, SUTVA, Ignorability, Positivity, Average Treatment Effect, Propensity Score (later), Instrumental Variable (later), Fundamental Problem of Causal Inference.
Stance: foundational technical paper.
Relates to: The complementary framework to Pearl 1995 / Causality 2000 — the same causal effects in different notation. Pearl–Bareinboim 2009 and Pearl 2010 establish formal mappings between the two; ignorability + positivity in the Rubin language correspond to the existence of an admissible covariate set in the Pearl backdoor sense. The languages differ in ergonomics: graphs make assumptions visually inspectable; potential outcomes make assumptions algebraically inspectable and integrate naturally with regression-based estimation. The 1974 paper is the seed; the canonical textbook statement is Imbens–Rubin 2015. For CBCL / CIVeX, the framework provides the other half of the causal toolkit: a CIVeX certificate may state its identification claim in either potential-outcomes or graphical language, and the verifier may need to translate. Knowing both is part of the technical literacy required for serious causal-claim verification. Shpitser–Pearl 2006’s completeness on the graphical side has no equally clean counterpart on the potential-outcomes side — the practical computational ground favours graphs.

Identification of Joint Interventional Distributions - Shpitser Pearl

Identification of Joint Interventional Distributions in Recursive Semi-Markovian Causal Models

Reference: Shpitser, I. & Pearl, J. (2006). Identification of Joint Interventional Distributions in Recursive Semi-Markovian Causal Models. In Proceedings of the 21st National Conference on Artificial Intelligence (AAAI-06), Boston, July 2006, pp. 1219–1226. URL (AAAI PDF) · Companion: What Counterfactuals Can Be Tested, UAI-07

Summary

Shpitser and Pearl give the complete identification algorithm for non-parametric causal effects in recursive semi-Markovian causal models — the result that finishes the project Pearl 1995 began. The headline: given a DAG with possibly hidden variables, and a target intervention distribution P(Y | do(X = x)), there is a sound and complete algorithm — ID — that either returns a closed-form expression in the observational distribution P(V) or proves that no such expression exists (the effect is unidentifiable). Where Pearl 1995 gave sufficient conditions (backdoor, front-door) leaving a grey zone of “we haven’t found an adjustment, but maybe one exists,” Shpitser–Pearl close the grey zone: the ID algorithm finds an expression if and only if one exists. The do-calculus of Causality (2000) turns out to be exactly the right deductive system — the ID algorithm is essentially a complete proof-search procedure for do-calculus derivations.

The mechanism is technical but compact. The algorithm operates on a semi-Markovian causal DAG (a DAG with hidden / latent variables represented by bidirected edges in the ADMG — acyclic directed mixed graph). It recursively decomposes the target distribution by c-component factorisation — a generalisation of chain-rule decomposition that respects the latent-variable structure — and at each step either reduces to an identified sub-problem or detects a hedge, a particular graphical pattern (the canonical obstruction to identifiability) that proves unidentifiability. The companion paper What Counterfactuals Can Be Tested (UAI-07) extends the framework to counterfactual queries (layer-3 in the Pearl ladder), characterising which counterfactuals are identifiable from interventional data.

For CBCL / CIVeX, the Shpitser–Pearl ID algorithm is the operational substrate. A CIVeX certificate states a target causal query, the assumed DAG, and the ID derivation that identifies the query in terms of observational data. The verifier — running a small implementation of ID — checks the derivation against the algorithm. If the certificate type-checks, the causal claim is provably identifiable under the stated assumptions; if it fails, the certificate is rejected. Completeness means the verifier never needs to ask the prover for a different formulation: if any identification exists, ID finds it. The classical pair with PCC is exact: PCC + ID together give the picture of “ship the causal proof, check the proof” for causal-inference artefacts. Shpitser–Pearl is therefore one of the most direct technical citations the CBCL / CIVeX discussion section needs.

Key Ideas

Recursive semi-Markovian causal model: an acyclic directed graph over observed and hidden variables, equivalently an acyclic directed mixed graph (ADMG) over observed variables with bidirected edges representing shared hidden parents. The standard formal substrate for causal identifiability when some confounders are unmeasured.
Joint interventional distribution: P(Y | do(X = x)) for Y a (possibly multivariate) target and X a (possibly multivariate) intervention set. The paper handles the joint multivariate case rather than just single-cause single-effect.
ID algorithm: a recursive procedure that either returns a closed-form expression for P(Y | do(X = x)) in terms of P(V) (the observational distribution over observed variables) or detects unidentifiability via a hedge obstruction.
Soundness and completeness: the ID algorithm is sound (every expression returned is correct) and complete (if any expression for P(Y | do(X = x)) exists, ID returns one). Together with the soundness/completeness of do-calculus, this fully resolves non-parametric identifiability.
c-component factorisation: the structural decomposition that drives ID. Each c-component is a maximal set of observed variables connected by paths of bidirected edges; the joint distribution factorises along c-components in a way that respects the latent-variable structure.
Hedge as canonical obstruction: a hedge is a particular graphical pattern (a pair of c-forests in a tree-like configuration) whose presence proves unidentifiability. Every unidentifiable case witnesses a hedge.
Completeness of do-calculus: a corollary — Pearl’s three-rule do-calculus is complete for non-parametric identification. The ID algorithm is, in effect, an automated do-calculus prover.
Companion: counterfactual identification: What Counterfactuals Can Be Tested (UAI-07) extends the framework to layer-3 (counterfactual) queries, characterising which counterfactuals can be identified from interventional distributions.

Connections

Conceptual Contribution

Claim: For non-parametric causal identification in recursive semi-Markovian models, there is a sound and complete algorithm: given a target intervention distribution and a DAG with hidden variables, the algorithm either expresses the target in observational quantities or proves unidentifiability via the hedge graphical pattern. As a corollary, Pearl’s do-calculus is complete for identification.
Mechanism: The ID algorithm operates on a semi-Markovian DAG (or equivalently an ADMG over observed variables). At each recursive step, it performs c-component factorisation to decompose the target distribution along the latent-variable-induced equivalence classes; it then either reduces the problem to identified subproblems or recognises a hedge obstruction and outputs unidentifiable. Soundness follows from each step being a do-calculus transformation; completeness follows from hedges being the only obstruction.
Concepts introduced/used: ID Algorithm, c-Component, Hedge (Causal Inference), Semi-Markovian Causal Model, Acyclic Directed Mixed Graph, Identifiability, Completeness of do-Calculus.
Stance: foundational technical paper.
Relates to: The algorithmic completion of Pearl 1995 / Causality 2000: where 1995/2000 gave sufficient graphical conditions and the deductive do-calculus, Shpitser–Pearl 2006 gives the complete decision procedure. The companion What Counterfactuals Can Be Tested (UAI-07) extends to layer-3 queries. The complementary framework is Rubin’s potential outcomes; the algorithmic completeness on the graphical side has no equally clean counterpart on the potential-outcomes side, which is part of why graphical methods have won the practical computational ground. For CBCL / CIVeX, this is the operational substrate: a CIVeX certificate carries a DAG, a target query, and an ID derivation; the verifier runs a small ID implementation to check the derivation. Pairs with PCC in the obvious way: PCC + ID = “ship the causal proof, check the proof” for causal-inference artefacts. The CBCL/CIVeX discussion section’s claim that causal certificates are decidably checkable leans on Shpitser–Pearl completeness; without it, the architecture would have to apologise for occasionally being too weak.

Causality - Pearl

Causality: Models, Reasoning, and Inference

Reference: Pearl, J. (2000, 2nd ed. 2009). Causality: Models, Reasoning, and Inference. Cambridge University Press. 384 pp (1st ed.) / 484 pp (2nd ed.). URL (ILLC Amsterdam, 2nd ed. PDF) · Cambridge UP page · Internet Archive

Summary

Causality is the book-length statement of Pearl’s graphical-causal-inference programme — the work that fixes a usable vocabulary for causation in the empirical sciences, replacing decades of philosophical regress with a constructive theory. The book extends the apparatus of Causal Diagrams for Empirical Research (1995) along three axes. (1) From interventional to counterfactual causal queries: the structural causal model (SCM) — a system of structural equations with exogenous error terms — supports queries about what would have happened if particular variables had taken different values, not only about intervention distributions. (2) From backdoor / front-door criteria to do-calculus: a complete deductive system (three rules: insertion/deletion of observations, action/observation exchange, and insertion/deletion of actions) for transforming do-expressions. Together with Shpitser & Pearl 2006’s completeness result, do-calculus is complete for non-parametric identifiability. (3) From identifiability to applied causal inference: chapters on confounding, mediation, instrumental variables, the actual-cause problem, and the foundations of legal-causal reasoning.

The technical core in three layers. Layer 1 (association): ordinary probabilistic conditional P(Y | X). Layer 2 (intervention): post-do distribution P(Y | do(X = x)), derived from the SCM by surgical replacement of X’s equation. Layer 3 (counterfactuals): queries like P(Y_{X=x} | X = x', Y = y') — “given that we observed X = x' and Y = y', what would Y have been if we had set X = x?” — derived by the abduction–action–prediction procedure: update exogenous-error distributions on the evidence, intervene on X, predict Y. Pearl calls this stratification the Ladder of Causation; the book argues that the climb from layer 1 to layer 3 is a matter of added assumptions (structural equations, then exogenous-error distributions), not of finer-grained statistical methodology.

For CBCL and CIVeX, the book is the textbook reference. CIVeX certificates carry a DAG, a stated set of structural assumptions, and a do-calculus derivation establishing identifiability of the target causal query. The host’s verifier checks the derivation against the do-calculus rules. The completeness of do-calculus (Shpitser & Pearl 2006) means that the verifier never has to apologise for being too weak: if the effect is identifiable at all, do-calculus derives it. The book also supplies the vocabulary for stating what CIVeX certificates are claiming: distinctions between association, intervention, and counterfactual; between identifiability and estimability; between confounding, mediation, and selection — all of which are needed to write precise threat models for causal claims in multi-agent settings.

Key Ideas

Structural Causal Model (SCM): a system of structural equations Vᵢ := fᵢ(PAᵢ, Uᵢ) over endogenous variables V with exogenous errors U, plus a distribution over U. The SCM is the formal carrier of all three causal layers.
Ladder of Causation: three layers of causal queries, each requiring strictly more assumptions. Layer 1 (seeing) — P(Y | X). Layer 2 (doing) — P(Y | do(X = x)). Layer 3 (imagining) — counterfactuals P(Y_{X=x} | E) for arbitrary evidence E.
do-calculus: three syntactic transformation rules over do-expressions: (R1) insertion/deletion of observations under d-separation; (R2) action/observation exchange under modified d-separation; (R3) insertion/deletion of actions under absence-of-causal-paths. Combined with probability axioms, the calculus is complete for non-parametric identifiability (Shpitser–Pearl 2006).
Identifiability under unobserved confounders: many effects are identifiable even when key confounders are unmeasured. The do-calculus discovers when, and the Shpitser–Pearl ID algorithm gives a complete procedure.
Counterfactual queries by abduction–action–prediction: (i) Update P(U) on observed evidence (abduction). (ii) Intervene on the SCM (action). (iii) Compute the distribution of the target variable (prediction). The procedure yields counterfactuals from the SCM.
Mediation analysis: natural direct, natural indirect, and total effects decompose causal influence along specific paths. Identification conditions are characterised by the mediation formula and the more general path-specific effects.
Instrumental variables: a classical econometric tool given a clean graphical characterisation — an instrument is a variable affecting X but not Y directly or via unmeasured confounders. The IV estimand is recoverable when the graphical conditions hold.
Actual cause / responsibility: chapter 10 develops a formal theory of actual causation — what actually caused the outcome in this token case? — built on counterfactuals and contingency. Foundational for legal and AI-ethics applications.
Transportability: under what conditions can a causal effect estimated in one population be transferred to another? Bareinboim–Pearl give graphical criteria.

Connections

Conceptual Contribution

Claim: Causal reasoning admits a precise, computable, non-parametric foundation built on structural causal models (SCMs), the do-operator for intervention, and the do-calculus for transforming causal queries. The three-layer Ladder of Causation (association / intervention / counterfactual) stratifies the assumptions required for each kind of causal claim.
Mechanism: Define SCMs as systems of structural equations with exogenous errors. Define interventions surgically (replace X’s equation by X := x). Define counterfactuals via abduction–action–prediction on the SCM. Give the do-calculus (three transformation rules) and show it is sound; later work (Shpitser–Pearl 2006) shows it is also complete for identification. Extend to mediation, instruments, actual causation, transportability across populations.
Concepts introduced/used: Structural Causal Model, Ladder of Causation, do-Calculus, Counterfactual, Mediation Analysis, Instrumental Variable, Actual Cause, Transportability, Identifiability.
Stance: foundational technical monograph / textbook.
Relates to: The book that the paper Causal Diagrams (1995) prefigures and that Shpitser & Pearl 2006 completes algorithmically. The complementary framework is Rubin’s potential outcomes (1974): the same causal effects in counterfactual notation, with explicit formal mappings between the two languages (Pearl–Bareinboim 2009). For CBCL / CIVeX, the book is the textbook reference: CIVeX certificates carry DAGs, structural assumptions, and do-calculus derivations of identifiability; the host’s verifier checks the derivation against the calculus. The PCC pairing is exact (Necula): PCC ships behavioural proofs over machine states; CIVeX ships causal-identification proofs over the DAG; both rely on small, generic verifiers that check rather than re-derive.

Causal Diagrams for Empirical Research - Pearl

Causal Diagrams for Empirical Research

Reference: Pearl, J. (1995). Causal Diagrams for Empirical Research. Biometrika 82(4): 669–688. December 1995. With discussion and rejoinder. URL (UCLA CogSys Lab) · DOI

Summary

Pearl’s Causal Diagrams is the paper in which the modern graphical apparatus of causal inference takes recognisable shape: directed acyclic graphs (DAGs) over observed and latent variables as the carrier of non-parametric causal assumptions, the do-operator as the formal representation of intervention, and the backdoor criterion as the first widely-usable graphical test for whether a causal effect is identifiable from observational data given a set of measured covariates. Where the early structural-equations and path-analysis tradition (Wright 1921, Haavelmo 1943) had given causal interpretations to specific parametric models, and where the do-then-randomise tradition (Rubin 1974) had given a counterfactual semantics to causal effects without graphs, Pearl unifies both: the DAG carries the structural assumptions, the do-operator gives the counterfactual semantics, and a small algebra of graphical operations decides identifiability.

The mechanism is precise. A causal model is a DAG G over variables V together with structural equations or, more generally, a non-parametric structural model. The do-operator do(X = x) represents the intervention that sets X to x regardless of X’s natural causes — graphically, by severing the incoming edges to X in G. A causal effect P(Y | do(X = x)) is identifiable from observational data over V iff it can be written as an expression in the observational distribution P(V). The backdoor criterion gives a sufficient condition: a set Z of measured covariates is admissible for adjustment iff Z blocks every backdoor path from X to Y (every path with an arrow into X) and contains no descendants of X. When Z is admissible, P(Y | do(X = x)) = ∑_z P(Y | X = x, Z = z) P(Z = z) — the backdoor adjustment formula. The paper also introduces the front-door criterion for cases where backdoor adjustment fails but a mediator can be exploited.

For the CBCL / CIVeX programme, Pearl 1995 is the foundation. CIVeX certificates carry a DAG of causal assumptions and a proof that the queried effect is identifiable from the available data under those assumptions; this is exactly what Pearl establishes is expressible and checkable. The paper is also a methodological complement to the PCC architecture in CBCL: where PCC ships behavioural proofs, CIVeX ships causal-identification proofs, and both are checked against a stated specification rather than re-derived. The completion of the graphical identifiability story — characterising exactly which causal effects are identifiable in the presence of unobserved confounders — is Shpitser & Pearl 2006’s complete-ID algorithm; Pearl 1995 is the place the story starts to look like an algorithm rather than a case-by-case analysis.

Key Ideas

Causal DAG as non-parametric structural model: a DAG G over V together with structural equations (or a non-parametric Markov-compatible distribution). The DAG carries the causal assumptions; the distribution is what is observed.
do-operator: do(X = x) represents intervention — setting X to x by external manipulation, severing the natural mechanisms that determine X. Graphically: delete incoming edges to X in G; semantically: replace X’s structural equation with X := x. The post-intervention distribution P(V | do(X = x)) is the central object of causal inference.
Identifiability: a causal query P(Y | do(X = x)) is identifiable from observational data over V iff it can be written as an expression in P(V). Identifiability is a graphical property — it depends only on the DAG, not on the specific distribution.
Backdoor criterion: Z ⊆ V is admissible for adjustment iff (i) no node in Z is a descendant of X in G, and (ii) Z blocks every backdoor path from X to Y (every path with an arrow into X). When Z is admissible, P(Y | do(X = x)) = ∑_z P(Y | X = x, Z = z) P(Z = z).
Front-door criterion: when no admissible Z for backdoor adjustment exists, identification may still be possible via a mediator M on the directed path from X to Y. The front-door formula uses M to identify the effect even in the presence of unobserved confounders.
Markov compatibility / d-separation: G constrains P(V) via conditional-independence statements encoded by d-separation — a purely graphical criterion. The empirical content of a causal DAG is exactly the d-separations it implies.
Bridge to interventions: causal effects can be defined purely structurally (no counterfactual ontology needed) by reference to the post-intervention distribution. Counterfactuals re-enter when finer-grained queries (mediation, attribution) are asked, handled by structural causal models in Pearl’s later work.

Connections

Conceptual Contribution

Claim: Causal effects can be represented graphically (as DAGs over observed and latent variables) and identified from observational data by a calculus of graphical operations. The do-operator gives the formal semantics of intervention; the backdoor and front-door criteria give algorithmic identifiability conditions.
Mechanism: Encode causal assumptions as a DAG G over V. Define interventions via the do-operator, semantically the surgical replacement of X’s structural equation by X := x and graphically the severing of incoming edges. State identifiability as the existence of an expression in P(V) for P(Y | do(X = x)). Give the backdoor criterion as a sufficient graphical condition (block all backdoor paths, no descendants of X) together with the backdoor adjustment formula. Give the front-door criterion for the harder case of unmeasured confounding. The result is a non-parametric, graph-driven, algorithmic theory of causal identification.
Concepts introduced/used: do-Calculus, Causal DAG, Structural Causal Model, Intervention, Backdoor Criterion, Front-door Criterion, d-Separation, Identifiability, Markov Compatibility.
Stance: foundational technical paper.
Relates to: Pearl’s compact statement of the apparatus developed at book length in Causality (2000/2009); the algorithmic completion is Shpitser & Pearl 2006. The complementary tradition is Rubin’s potential-outcomes framework (1974) — the same causal effects in counterfactual notation; later work (Pearl–Bareinboim, Imbens–Rubin) establishes formal mappings between the two. For CBCL and CIVeX, this is the substrate: a CIVeX certificate carries a DAG and a proof of identifiability under stated assumptions, checked by the host rather than re-derived. The pairing with PCC is exact: PCC ships behavioural proofs over machine states; CIVeX ships causal-identification proofs over the DAG. The d-separation / Markov-compatibility connection grounds the bridge to probabilistic graphical models more broadly.

Proof-Carrying Code - Necula

Proof-Carrying Code

Reference: Necula, G. C. (1997). Proof-Carrying Code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’97), Paris, January 1997, pp. 106–119. ACM. URL (author’s Berkeley page, original PostScript) · URL (Illinois course PDF mirror) · DOI (ACM)

Summary

Proof-Carrying Code (PCC) is the architectural ancestor of every “ship a proof with the artefact, verify the proof rather than re-deriving safety from scratch” pattern in the modern security stack — including CBCL’s R4 split (host runs a small certified verifier on each dialect contract proof), CIVeX certificates (causal-identifiability artefacts shipped from prover to host), BAN-style protocol soundness certificates, and TEE attestations. The premise is direct: untrusted code arrives at a host that must run it under a safety policy (no out-of-bounds memory access, no division by zero, no privilege escalation, only sanctioned syscalls). Re-deriving safety on every load is expensive (general program analysis is undecidable, conservative approximations reject too much real code) and shifts trust onto the host’s analyser. PCC inverts the burden: the code producer generates a machine-checkable proof that the code respects the policy, and the code consumer checks the proof. Proof checking is mechanical, syntactic, decidable, and cheap; proof finding (the work that produced the proof) is hard and lives on the producer’s side.

The technical content of the paper is the framework that makes this practical. Necula defines a safety policy as a set of rules in a first-order theory over machine states; programs come accompanied by a safety predicate whose proof in this theory entails the policy. Proofs are encoded in a logical framework (LF / Edinburgh Logical Framework), so the proof-checker is a single, small, generic LF type-checker independent of the safety policy. Necula demonstrates the architecture on a packet-filter benchmark: a Berkeley Packet Filter untrusted assembler program is verified to terminate, stay in bounds, and call no syscalls — by checking ~5 KB of LF proof against the BPF policy, in milliseconds. The signal is that the verifier is tiny and policy-parameterised; safety becomes a function of proof checkability rather than of expensive whole-program analysis.

For the security agenda this vault tracks, PCC is foundational in three respects. First, it generalises capability-secure thinking (Dennis & Van Horn 1966, Shapiro et al.) from access control to behavioural conformance: the proof is a behavioural capability the producer holds, the verifier is the gatekeeper. Second, it operationalises Rice’s theorem in a constructive direction — Rice says semantic properties of arbitrary programs are undecidable, but PCC shows that with a proof in hand, checking that the proof establishes the semantic property is trivial. Third, it is the architectural pattern that CBCL’s R4 split inherits literally: a CBCL dialect contract is the code, a Lean 4 proof that the contract is well-formed and policy-respecting is the certificate, and the host’s small Lean kernel check is the PCC verifier. The discussion section of any CBCL/CIVeX paper should cite PCC explicitly.

Key Ideas

Ship the proof with the artefact: the code producer (who knows why the code is safe) generates a proof; the code consumer checks the proof. Proof-checking is cheap, mechanical, syntactic, and decidable; the finding of proofs is hard and lives on the producer’s side.
Safety policy = first-order theory: a safety policy is a set of inference rules in a first-order theory over machine states and operations. Programs come with a safety predicate; a proof of the predicate in the theory entails the policy.
Logical Framework as the proof carrier: proofs are LF terms (Edinburgh Logical Framework). The verifier is an off-the-shelf LF type-checker — small, generic, policy-parameterised. Trusted code base: the LF type-checker plus the policy rules.
Asymmetry of effort: producer effort scales with program complexity; consumer effort scales with proof size, which is bounded by program size in practice but does not depend on the difficulty of the underlying analysis.
Decoupling of policy from verifier: changing the safety policy means changing the inference-rule set; the LF checker is reused unchanged. New policies can be deployed without re-validating the verifier.
No trust in the producer: a malicious producer can submit malicious code, but cannot generate a verifiable proof for it (under soundness of the policy). The producer is untrusted; the verifier is the trust anchor.
Packet-filter benchmark: BPF programs, originally trusted via interpretation in a kernel sandbox, are PCC-verified to be safe to run as native code. Verification cost drops from microseconds-per-packet (interpreter) to a one-time millisecond proof check at load time.
Generalises to many policies: type safety, memory safety, resource bounds, information-flow control, even fine-grained behavioural contracts — all expressible as PCC safety policies.

Connections

Conceptual Contribution

Claim: Safe execution of untrusted code under a stated safety policy can be achieved by having the code producer ship a machine-checkable proof of policy compliance with the code, and having the code consumer check the proof rather than re-derive safety. This inverts the standard burden: hard-to-derive properties become trivial-to-check given the right artefact.
Mechanism: Express the safety policy as a first-order theory over machine states; require submissions to include a proof of the program’s safety predicate; encode proofs in a Logical Framework (LF) so the consumer-side checker is a generic LF type-checker independent of the policy. The trusted code base is the LF checker plus the policy rules; the producer is untrusted. Demonstrated on the Berkeley Packet Filter, where PCC verification runs in milliseconds at load and replaces interpreter-based sandboxing.
Concepts introduced/used: Proof-Carrying Code, Safety Policy, Safety Predicate, Logical Framework (LF), Producer-Consumer Asymmetry, Verifier, Trusted Code Base, Behavioural Capability.
Stance: foundational technical paper / architectural pattern.
Relates to: The architectural ancestor of CBCL’s R4 split — dialect contracts are shipped with Lean 4 proofs of well-formedness and policy compliance; the host’s small Lean kernel check is the PCC verifier. PCC is the citation for “ship the proof, check the proof.” Operationalises Rice’s theorem in a constructive direction: undecidable in general, decidable with the producer’s proof in hand. The natural pair is Schneider 2000 — Schneider characterises which policies are enforceable by trace monitoring; PCC characterises how a code consumer can verify static policies without re-deriving them. The verification heritage runs through Hoare 1969 / Floyd (axiomatic semantics and inductive assertions) to PCC’s LF-encoded proofs. The LangSec tradition (Sassaman et al.) is the dual move: restrict the input language so safety becomes decidable without a producer-side proof. CBCL combines both: a DCFL surface (LangSec) with proof-carrying dialect contracts (PCC).

ID Algorithm

Tian–Pearl complete algorithm for identifying causal effects from observational data on a Semi-Markovian Causal Model: returns an estimand if and only if the effect is identifiable, otherwise reports a hedge.