After Acceptance: A Claim Graph for Residual-Machine Claims, Calibrated on eBPF

Preprint. Not peer reviewed. Language-theoretic security asks whether a boundary recognizes the language that downstream machinery actually interprets. At a program-verifier boundary, an accepted artifact may drive stateful runtime operations not described by an intended report relation. We introduce a five-node claim graph separating artifact acceptance (A), a same-suffix causal state distinction (C), bounded programmability (P), output-witnessed computed-report non-factorization (R), and a policy/threat obligation (W). A future-observation quotient and behavioral factorization criterion distinguish the accepted-artifact-indexed causal language from the report-relative residual language. The criterion is report-instance-relative, applies only under an explicit unique-cell report map on the chosen context fiber, and does not assert that every safety-sound incomplete verifier hosts a weird machine. We give proof obligations for a uniformly controlled, observable, resettable gate and one fixed accepted interpreter over a bounded circuit-description domain. Prefix induction yields bounded composition under exact scheduling, admissibility, serialization, and frame-preservation premises. In a Linux eBPF calibration, a dedicated preallocated non-LRU two-entry hash map realizes NAND: reset leaves one sentinel entry; input bits select existing- or fresh-key updates; and the second update’s success predicate supplies the output. One fixed accepted program consumes canonical NAND DAGs with at most 64 inputs, 512 gates, and 578 live wires. A source-snapshotted Linux/aarch64 run covers named and random circuits, joint bounds, serial reuse, mechanism controls, and malformed descriptors. A separate author-run semantic auditor reconstructs descriptors and circuit semantics, and a self-issued manifest checks bundle integrity. The case records A, gives a conditional C witness under the declared concrete-service/no-interference contract, and supports P under additional implementation premises. It does not establish Linux report non-factorization or a policy-level weird machine; that separation is the main methodological contribution.