No Certificate, No Execution: Certified Traces as a Foundation for Trustworthy AI Agents

Agostino Capponi; Xiaodong Wang; Xiao-Yang Liu Yanglet

arxiv: 2605.24462 · v1 · pith:XDNOX4LW · submitted 2026-05-23 · cs.CE

No Certificate, No Execution: Certified Traces as a Foundation for Trustworthy AI Agents

Xiao-Yang Liu Yanglet , Xiaodong Wang , Agostino Capponi This is my paper

Reviewed by Pith T0 review T1 audit T2 compute T3 formal T4 reserved 2026-06-30 12:24 UTCgrok-4.3pith:XDNOX4LW record.json open to challenge →

**Figure 1.** Figure 1: The Proposal–Certification–Execution (PCE) architecture. A generating machine [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] reproduced from arXiv: 2605.24462

classification cs.CE

keywords trustworthy AI agentscertified tracespermissibility machinePCE architecturepolicy complianceexecution controlAI safety

0 comments

The pith

AI agents should execute traces only when they carry a verifiable certificate of permissibility under policy Π.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper argues that trustworthy AI agents in high-stakes domains need execution to be gated by certification rather than generation strength or post-hoc checks. A generating machine proposes candidate traces, a Permissibility Machine certifies them against a policy system, and execution occurs only for traces that receive a checkable certificate. This handles cases where individual steps are allowed yet the full sequence violates policy, or where an action is computable but impermissible. The executable language is defined strictly as the intersection of what can be generated and what can be certified.

Core claim

The Proposal-Certification-Execution architecture requires that an agent-generated trace executes only when it carries a checkable certificate witnessing permissibility under Π, with L_exec formed as the intersection L_G ∩ L_cert(M_Π) where M_Π is the Permissibility Machine.

What carries the argument

The Permissibility Machine M_Π, which inspects a proposed structured trace (steps, evidence, tool calls, credentials) and issues a certificate only if the trace satisfies the policy system Π.

If this is right

Execution is permitted solely for traces inside L_G ∩ L_cert(M_Π).
Agent performance is measured by the set of traces that can be safely certified rather than by output accuracy alone.
Trace certification extends proof-carrying execution, proof memory, and zero-knowledge techniques to agent behavior.
Visible reasoning aids detection but does not replace the need for full-trace certifiability.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Domain-specific policy languages would be needed to make M_Π practical across different regulated settings.
Certified traces could be stored and reused as a form of reusable proof memory for similar future proposals.
The architecture could apply to multi-agent interactions where one agent's output becomes another's input trace.

Load-bearing premise

A Permissibility Machine can be built that correctly certifies arbitrary traces under policy Π without blocking valid actions or permitting invalid ones.

What would settle it

A concrete case in which either a permissible trace is rejected by M_Π or an impermissible trace is accepted by M_Π.

Figures

Figures reproduced from arXiv: 2605.24462 by Agostino Capponi, Xiaodong Wang, Xiao-Yang Liu Yanglet.

**Figure 3.** Figure 3: Action-level geometry of the permissibility gap. The computable action set C is the operative universe of candidate actions available to the system. The permissible action set P ⊆ C contains actions permitted at the action level. The region C \ P is the permissibility gap: actions that are available to the system but not permitted. In the strict-separation setting considered here, P ⊊ C, so the gap is none… view at source ↗

**Figure 4.** Figure 4: Proof-memory classes of certifiers. The examples in Appendix F motivate a progression of certifier classes ordered by proof-memory support, from local checks to persistent proof memory: M (0) Π ⪯ M (1) Π ⪯ M (2) Π ⪯ M (3) Π . Level 0 performs deterministic checks and attaches source links; Level 1 constructs structured certificates and supports replay of evidence and computations; Level 2 supports proof-ca… view at source ↗

read the original abstract

We argue that trustworthy AI agents, especially in high-stakes and policy-governed domains, should make execution conditional on certified traces rather than rely only on stronger generative models, output-level guardrails, or post-hoc audits. A generative agent may propose recommendations, tool calls, reports, or actions, but generation is not permission: an action may be computable yet impermissible, and individually permissible actions may compose into an impermissible trace. We formalize trustworthy agency through a \textbf{Proposal--Certification--Execution (PCE)} architecture: a probabilistic generating machine $M_G$ proposes candidate execution traces, a \textbf{Permissibility Machine} $M_\Pi$ certifies proposed traces under a policy system $\Pi$, and execution proceeds only for certified traces. The executable trace language is $L_{\mathrm{exec}} = L_G \cap L_{\mathrm{cert}}(M_\Pi)$. Before execution, a trace is a structured pre-execution record submitted for certification: it specifies intended steps, evidence, proposed tool calls, approvals, replayable computations, credentials, and execution conditions. This perspective complements chain-of-thought monitorability: visible reasoning may help detect misbehavior, but monitorability is not certifiability, and reasoning is only one component of a broader execution trace. The formal principle is simple: an agent-generated trace should execute only when it carries a checkable certificate witnessing permissibility under $\Pi$: \textbf{no certificate, no execution}. We develop certified traces and Permissibility Machines as foundations for trustworthy AI agents, connect trace certification to proof-carrying execution, proof memory, privacy, and zero-knowledge certificates, and propose evaluating agents by what generated traces can be safely certified for execution, not by output accuracy alone.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper proposes gating AI agent execution behind trace certificates but provides no construction or definition for the Permissibility Machine that would make this work.

read the letter

The main thing to know is that this paper argues for an architecture where AI agents only execute traces that carry a certificate from a Permissibility Machine under some policy, but it never shows how such a machine could be built or even defined for anything beyond trivial cases.

The paper does lay out the distinction between generation and permission clearly. It notes that individual actions can be allowed while their combination is not, and that monitorable reasoning is not the same as certifiable traces. Framing this as Proposal-Certification-Execution with the executable language as the intersection of generated and certified sets is a straightforward way to state the point. Connecting the idea to proof-carrying code and zero-knowledge certificates is also reasonable and points to existing formal methods work.

The soft spot is the complete lack of substance on the Permissibility Machine itself. The paper introduces M_Π and L_cert(M_Π) as central objects but gives no formal definition, no example for a non-trivial policy, and no argument that the machine can avoid blocking valid traces or allowing invalid ones. The claim therefore rests on an assumption that remains unexamined. There are no proofs, no worked examples, and no discussion of implementation cost or error rates.

This is a position paper rather than a technical result. The citations to prior literature on certified execution are appropriate, but the paper does not derive anything new from them. Readers already working on policy enforcement for agents might find the slogan useful as a reminder, but anyone looking for mechanisms or guarantees will come away empty.

I would not bring this to a reading group. It does not deserve peer review in its current form because the core component is missing.

Referee Report

2 major / 1 minor

Summary. The manuscript proposes a Proposal--Certification--Execution (PCE) architecture for trustworthy AI agents in high-stakes domains. A generative machine M_G proposes candidate execution traces; a Permissibility Machine M_Π certifies them under policy system Π; and execution is permitted only for certified traces. The executable language is formalized as L_exec = L_G ∩ L_cert(M_Π), with the core principle that an agent-generated trace executes only when it carries a checkable certificate of permissibility under Π ("no certificate, no execution"). The work connects this to proof-carrying execution, proof memory, privacy, and zero-knowledge certificates, and advocates evaluating agents by certifiable traces rather than output accuracy alone.

Significance. If a correct Permissibility Machine M_Π can be realized, the PCE architecture would provide a structural foundation for trustworthy agency by enforcing execution conditional on verifiable certificates rather than generative strength, output guardrails, or post-hoc audits. It usefully distinguishes generation from permission and notes that monitorability (e.g., chain-of-thought) is not equivalent to certifiability. The manuscript supplies no formal definitions, constructions, proofs, or empirical results, so significance is prospective and depends on addressing the feasibility of M_Π.

major comments (2)

[abstract / PCE architecture description] The central claim rests on the existence and correctness of M_Π such that L_exec = L_G ∩ L_cert(M_Π) can be realized without unacceptable false negatives or errors that block valid actions or permit invalid ones. The manuscript states this definition and describes the PCE architecture but supplies neither a formal definition of M_Π, a construction for any non-trivial Π, nor an argument establishing feasibility (see abstract and the paragraph introducing the Permissibility Machine).
[description of Permissibility Machine M_Π and L_exec] No argument or example is given showing that M_Π can be constructed to correctly certify arbitrary proposed traces (pre-execution records specifying steps, evidence, tool calls, credentials, etc.) while avoiding implementation errors. This assumption is load-bearing for the claim that execution can be made conditional on certificates in policy-governed domains.

minor comments (1)

[final paragraph] The connection to zero-knowledge certificates and proof-carrying execution is mentioned but not developed with any concrete mapping or reference to existing literature on those topics.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive report. The manuscript is a conceptual position paper proposing the PCE architecture as a foundation rather than a complete technical solution with constructions. We will revise to clarify this scope explicitly and add discussion of feasibility challenges for M_Π.

read point-by-point responses

Referee: [abstract / PCE architecture description] The central claim rests on the existence and correctness of M_Π such that L_exec = L_G ∩ L_cert(M_Π) can be realized without unacceptable false negatives or errors that block valid actions or permit invalid ones. The manuscript states this definition and describes the PCE architecture but supplies neither a formal definition of M_Π, a construction for any non-trivial Π, nor an argument establishing feasibility (see abstract and the paragraph introducing the Permissibility Machine).

Authors: We agree the manuscript provides no formal definition or construction of M_Π and does not argue feasibility for non-trivial Π. The paper's intent is to articulate the architectural principle that execution requires checkable certificates of permissibility, distinguishing it from monitorability or post-hoc methods, and to connect it to related ideas such as proof-carrying execution. We will revise the abstract and the section introducing M_Π to state explicitly that realizing a correct M_Π for complex policies remains an open challenge and is not claimed to be solved here. revision: partial
Referee: [description of Permissibility Machine M_Π and L_exec] No argument or example is given showing that M_Π can be constructed to correctly certify arbitrary proposed traces (pre-execution records specifying steps, evidence, tool calls, credentials, etc.) while avoiding implementation errors. This assumption is load-bearing for the claim that execution can be made conditional on certificates in policy-governed domains.

Authors: The manuscript does not supply arguments, examples, or constructions for building M_Π to certify arbitrary traces, nor does it address implementation errors. We accept this limitation and will add a dedicated subsection on open problems in realizing M_Π, including risks of false negatives/positives, the need for domain-specific policy formalizations, and potential use of techniques such as zero-knowledge proofs or verified monitors, while noting that these are directions for subsequent research rather than contributions of the present work. revision: yes

Circularity Check

0 steps flagged

No significant circularity; proposal is definitional and self-contained

full rationale

The paper advances a normative architectural proposal (PCE with M_G, M_Π, and the rule 'no certificate, no execution') together with the set-theoretic definition L_exec = L_G ∩ L_cert(M_Π). No derivation reduces a claimed result to fitted parameters, self-referential equations, or load-bearing self-citations. The central claim is an explicit stipulation of a new execution condition rather than a prediction extracted from prior inputs. The absence of a concrete construction for M_Π is a feasibility gap, not a circularity. The work is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 3 invented entities

The central claim rests on the unproven feasibility of building a correct Permissibility Machine and the assumption that policies can be encoded in a machine-checkable form; no free parameters or external benchmarks are used.

axioms (1)

domain assumption Policies Π can be formalized such that a machine M_Π can decide permissibility of traces in L_G.
Invoked in the definition of L_cert(M_Π) and the PCE architecture; no justification or reference to existing formal policy languages is given in the abstract.

invented entities (3)

Proposal--Certification--Execution (PCE) architecture no independent evidence
purpose: Framework separating generation from certified execution
New named structure introduced to organize the proposal; no independent evidence provided.
Permissibility Machine M_Π no independent evidence
purpose: Certifies proposed traces under policy Π
Core new component whose existence and correctness is assumed; no implementation or proof offered.
executable trace language L_exec = L_G ∩ L_cert(M_Π) no independent evidence
purpose: Defines the set of traces that may execute
Formal definition introduced without derivation or prior existence proof.

pith-pipeline@v0.9.1-grok · 5865 in / 1457 out tokens · 34144 ms · 2026-06-30T12:24:52.995194+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

25 extracted references · 4 canonical work pages · 4 internal anchors

[1]

ReAct: Synergizing reasoning and acting in language models

Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik Narasimhan, and Yuan Cao. ReAct: Synergizing reasoning and acting in language models. InInternational Conference on Learning Representations, 2023

2023
[2]

Toolformer: Language models can teach themselves to use tools

Timo Schick, Jane Dwivedi-Yu, Roberto Dessì, Roberta Raileanu, Maria Lomeli, Luke Zettle- moyer, Nicola Cancedda, and Thomas Scialom. Toolformer: Language models can teach themselves to use tools. InAdvances in Neural Information Processing Systems, 2023. 14

2023
[3]

AgentDojo: A dynamic environment to evaluate prompt injection attacks and defenses for LLM agents

Edoardo Debenedetti, Jie Zhang, Mislav Balunovi´c, Luca Beurer-Kellner, Marc Fischer, and Florian Tramèr. AgentDojo: A dynamic environment to evaluate prompt injection attacks and defenses for LLM agents. InAdvances in Neural Information Processing Systems, Datasets and Benchmarks Track, 2024

2024
[4]

OpenAI and PwC Collaborate to Reimagine the Office of the CFO.https://openai

OpenAI. OpenAI and PwC Collaborate to Reimagine the Office of the CFO.https://openai. com/index/openai-pwc-finance-collaboration/, 2026. Accessed: 2026-05-23

2026
[5]

American Express debuts Agentic Commerce Experiences (ACE) developer kit and announces industry-first protection for registered agent purchases

American Express. American Express debuts Agentic Commerce Experiences (ACE) developer kit and announces industry-first protection for registered agent purchases. American Express Newsroom, 2026. Accessed May 2026

2026
[6]

Agents for financial services

Anthropic. Agents for financial services. Anthropic, 2026. Accessed May 2026

2026
[7]

Q&A record for 2025 interim results announcement of industrial and commercial bank of China limited

Industrial and Commercial Bank of China. Q&A record for 2025 interim results announcement of industrial and commercial bank of China limited. ICBC Investor Relations, 2025. Accessed May 2026

2025
[8]

Chain of Thought Monitorability: A New and Fragile Opportunity for AI Safety

Tomek Korbak, Mikita Balesni, Elizabeth Barnes, Yoshua Bengio, Joe Benton, Joseph Bloom, Mark Chen, Alan Cooney, Allan Dafoe, Anca Dragan, et al. Chain of thought monitorability: A new and fragile opportunity for ai safety.arXiv preprint arXiv:2507.11473, 2025

work page internal anchor Pith review Pith/arXiv arXiv 2025
[9]

Evaluating chain-of-thought monitorability

OpenAI. Evaluating chain-of-thought monitorability. OpenAI Research, 2025

2025
[10]

Bran, Sam Cox, Oliver Schilter, et al

Andres M. Bran, Sam Cox, Oliver Schilter, et al. Augmenting large language models with chemistry tools.Nature Machine Intelligence, 2024

2024
[11]

Tang et al

X. Tang et al. Risks of AI scientists: Prioritizing safeguarding over autonomy.Nature Communications, 2025

2025
[12]

Identifying the risks of LM agents with an LM-emulated sandbox

Yangjun Ruan et al. Identifying the risks of LM agents with an LM-emulated sandbox. In International Conference on Learning Representations, 2024

2024
[13]

Watch out for your agents! investigating backdoor threats to LLM-based agents

Wenkai Yang, Xiaohan Bi, Yankai Lin, Sishuo Chen, Jie Zhou, and Xu Sun. Watch out for your agents! investigating backdoor threats to LLM-based agents. InAdvances in Neural Information Processing Systems, 2024

2024
[14]

Agent-SafetyBench: Evaluating the Safety of LLM Agents

Zhexin Zhang, Shiyao Cui, Yida Lu, Jingzhuo Zhou, Junxiao Yang, Hongning Wang, and Minlie Huang. Agent-SafetyBench: Evaluating the safety of LLM agents.arXiv preprint arXiv:2412.14470, 2024

work page internal anchor Pith review Pith/arXiv arXiv 2024
[15]

A Systematic Survey of Security Threats and Defenses in LLM-Based AI Agents: A Layered Attack Surface Framework

Kexin Chu. A systematic survey of security threats and defenses in LLM-based AI agents: A layered attack surface framework.arXiv preprint arXiv:2604.23338, 2026

work page internal anchor Pith review Pith/arXiv arXiv 2026
[16]

Shijie Han, Haoqiang Kang, Bo Jin, Xiao-Yang Liu, and Steve Y . Yang. XBRL Agent: Lever- aging large language models for financial report analysis. InProceedings of the 5th ACM International Conference on AI in Finance, pages 856–864, 2024

2024
[17]

An overview of the runtime verification tool java pathex- plorer.Formal Methods in System Design, 2004

Klaus Havelund and Grigore Rosu. An overview of the runtime verification tool java pathex- plorer.Formal Methods in System Design, 2004

2004
[18]

GuardAgent: Safeguard LLM Agents by a Guard Agent via Knowledge-Enabled Reasoning

Zhen Xiang, Linzhi Zheng, Yanjie Li, Junyuan Hong, Qinbin Li, Han Xie, Jiawei Zhang, Zidi Xiong, Chulin Xie, Carl Yang, Dawn Song, and Bo Li. GuardAgent: Safeguard llm agents by a guard agent via knowledge-enabled reasoning.arXiv preprint arXiv:2406.09187, 2024

work page internal anchor Pith review Pith/arXiv arXiv 2024
[19]

George C. Necula. Proof-carrying code. InProceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997

1997
[20]

Andrei Sabelfeld and Andrew C. Myers. Language-based information-flow security.IEEE Journal on Selected Areas in Communications, 2003

2003
[21]

The Standard for Reporting

XBRL International. The Standard for Reporting. https://www.xbrl.org/the-standard/ what/the-standard-for-reporting/, 2026. Accessed: 2026-05-23. 15

2026
[22]

Inline XBRL

XBRL International. Inline XBRL. https://www.xbrl.org/the-standard/what/ ixbrl/, 2026. Accessed: 2026-05-23

2026
[23]

Position: A safe harbor for AI evaluation and red teaming

Shayne Longpre, Sayash Kapoor, Kevin Klyman, Ashwin Ramaswami, Rishi Bommasani, Borhane Blili-Hamelin, Yangsibo Huang, et al. Position: A safe harbor for AI evaluation and red teaming. InInternational Conference on Machine Learning, 2024

2024
[24]

A brief account of runtime verification.The Journal of Logic and Algebraic Programming, 2009

Martin Leucker and Christian Schallhart. A brief account of runtime verification.The Journal of Logic and Algebraic Programming, 2009

2009
[25]

no more expressive than

Industrial and Commercial Bank of China. 2025 annual results announcement of industrial and commercial bank of China limited. ICBC Investor Relations, 2026. Accessed May 2026. A Formal Trace Model This appendix gives the formal trace model underlying the main text. Its purpose is to make explicit the objects, languages, and assumptions used by the proposa...

2025

[1] [1]

ReAct: Synergizing reasoning and acting in language models

Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik Narasimhan, and Yuan Cao. ReAct: Synergizing reasoning and acting in language models. InInternational Conference on Learning Representations, 2023

2023

[2] [2]

Toolformer: Language models can teach themselves to use tools

Timo Schick, Jane Dwivedi-Yu, Roberto Dessì, Roberta Raileanu, Maria Lomeli, Luke Zettle- moyer, Nicola Cancedda, and Thomas Scialom. Toolformer: Language models can teach themselves to use tools. InAdvances in Neural Information Processing Systems, 2023. 14

2023

[3] [3]

AgentDojo: A dynamic environment to evaluate prompt injection attacks and defenses for LLM agents

Edoardo Debenedetti, Jie Zhang, Mislav Balunovi´c, Luca Beurer-Kellner, Marc Fischer, and Florian Tramèr. AgentDojo: A dynamic environment to evaluate prompt injection attacks and defenses for LLM agents. InAdvances in Neural Information Processing Systems, Datasets and Benchmarks Track, 2024

2024

[4] [4]

OpenAI and PwC Collaborate to Reimagine the Office of the CFO.https://openai

OpenAI. OpenAI and PwC Collaborate to Reimagine the Office of the CFO.https://openai. com/index/openai-pwc-finance-collaboration/, 2026. Accessed: 2026-05-23

2026

[5] [5]

American Express debuts Agentic Commerce Experiences (ACE) developer kit and announces industry-first protection for registered agent purchases

American Express. American Express debuts Agentic Commerce Experiences (ACE) developer kit and announces industry-first protection for registered agent purchases. American Express Newsroom, 2026. Accessed May 2026

2026

[6] [6]

Agents for financial services

Anthropic. Agents for financial services. Anthropic, 2026. Accessed May 2026

2026

[7] [7]

Q&A record for 2025 interim results announcement of industrial and commercial bank of China limited

Industrial and Commercial Bank of China. Q&A record for 2025 interim results announcement of industrial and commercial bank of China limited. ICBC Investor Relations, 2025. Accessed May 2026

2025

[8] [8]

Chain of Thought Monitorability: A New and Fragile Opportunity for AI Safety

Tomek Korbak, Mikita Balesni, Elizabeth Barnes, Yoshua Bengio, Joe Benton, Joseph Bloom, Mark Chen, Alan Cooney, Allan Dafoe, Anca Dragan, et al. Chain of thought monitorability: A new and fragile opportunity for ai safety.arXiv preprint arXiv:2507.11473, 2025

work page internal anchor Pith review Pith/arXiv arXiv 2025

[9] [9]

Evaluating chain-of-thought monitorability

OpenAI. Evaluating chain-of-thought monitorability. OpenAI Research, 2025

2025

[10] [10]

Bran, Sam Cox, Oliver Schilter, et al

Andres M. Bran, Sam Cox, Oliver Schilter, et al. Augmenting large language models with chemistry tools.Nature Machine Intelligence, 2024

2024

[11] [11]

Tang et al

X. Tang et al. Risks of AI scientists: Prioritizing safeguarding over autonomy.Nature Communications, 2025

2025

[12] [12]

Identifying the risks of LM agents with an LM-emulated sandbox

Yangjun Ruan et al. Identifying the risks of LM agents with an LM-emulated sandbox. In International Conference on Learning Representations, 2024

2024

[13] [13]

Watch out for your agents! investigating backdoor threats to LLM-based agents

Wenkai Yang, Xiaohan Bi, Yankai Lin, Sishuo Chen, Jie Zhou, and Xu Sun. Watch out for your agents! investigating backdoor threats to LLM-based agents. InAdvances in Neural Information Processing Systems, 2024

2024

[14] [14]

Agent-SafetyBench: Evaluating the Safety of LLM Agents

Zhexin Zhang, Shiyao Cui, Yida Lu, Jingzhuo Zhou, Junxiao Yang, Hongning Wang, and Minlie Huang. Agent-SafetyBench: Evaluating the safety of LLM agents.arXiv preprint arXiv:2412.14470, 2024

work page internal anchor Pith review Pith/arXiv arXiv 2024

[15] [15]

A Systematic Survey of Security Threats and Defenses in LLM-Based AI Agents: A Layered Attack Surface Framework

Kexin Chu. A systematic survey of security threats and defenses in LLM-based AI agents: A layered attack surface framework.arXiv preprint arXiv:2604.23338, 2026

work page internal anchor Pith review Pith/arXiv arXiv 2026

[16] [16]

Shijie Han, Haoqiang Kang, Bo Jin, Xiao-Yang Liu, and Steve Y . Yang. XBRL Agent: Lever- aging large language models for financial report analysis. InProceedings of the 5th ACM International Conference on AI in Finance, pages 856–864, 2024

2024

[17] [17]

An overview of the runtime verification tool java pathex- plorer.Formal Methods in System Design, 2004

Klaus Havelund and Grigore Rosu. An overview of the runtime verification tool java pathex- plorer.Formal Methods in System Design, 2004

2004

[18] [18]

GuardAgent: Safeguard LLM Agents by a Guard Agent via Knowledge-Enabled Reasoning

Zhen Xiang, Linzhi Zheng, Yanjie Li, Junyuan Hong, Qinbin Li, Han Xie, Jiawei Zhang, Zidi Xiong, Chulin Xie, Carl Yang, Dawn Song, and Bo Li. GuardAgent: Safeguard llm agents by a guard agent via knowledge-enabled reasoning.arXiv preprint arXiv:2406.09187, 2024

work page internal anchor Pith review Pith/arXiv arXiv 2024

[19] [19]

George C. Necula. Proof-carrying code. InProceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997

1997

[20] [20]

Andrei Sabelfeld and Andrew C. Myers. Language-based information-flow security.IEEE Journal on Selected Areas in Communications, 2003

2003

[21] [21]

The Standard for Reporting

XBRL International. The Standard for Reporting. https://www.xbrl.org/the-standard/ what/the-standard-for-reporting/, 2026. Accessed: 2026-05-23. 15

2026

[22] [22]

Inline XBRL

XBRL International. Inline XBRL. https://www.xbrl.org/the-standard/what/ ixbrl/, 2026. Accessed: 2026-05-23

2026

[23] [23]

Position: A safe harbor for AI evaluation and red teaming

Shayne Longpre, Sayash Kapoor, Kevin Klyman, Ashwin Ramaswami, Rishi Bommasani, Borhane Blili-Hamelin, Yangsibo Huang, et al. Position: A safe harbor for AI evaluation and red teaming. InInternational Conference on Machine Learning, 2024

2024

[24] [24]

A brief account of runtime verification.The Journal of Logic and Algebraic Programming, 2009

Martin Leucker and Christian Schallhart. A brief account of runtime verification.The Journal of Logic and Algebraic Programming, 2009

2009

[25] [25]

no more expressive than

Industrial and Commercial Bank of China. 2025 annual results announcement of industrial and commercial bank of China limited. ICBC Investor Relations, 2026. Accessed May 2026. A Formal Trace Model This appendix gives the formal trace model underlying the main text. Its purpose is to make explicit the objects, languages, and assumptions used by the proposa...

2025