Pith. sign in

REVIEW 4 major objections 6 minor 47 references

An SMT solver, not the LLM, makes the final allow/block call for agent actions.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-01 10:54 UTC pith:GFWTRMOT

load-bearing objection A well-engineered agent authorization system with a serious evaluation, but the formal core has a hole: the pseudocode omits the obligation guards the text claims to encode. the 4 major comments →

arxiv 2607.27267 v1 pith:GFWTRMOT submitted 2026-07-29 cs.CR cs.AI

FAVA: Formal Authorization for Verified Agents with Evidence-Backed Permission Graphs

Yifan Zhang , Xinkui Zhao , Sai Liu , Hengxuan Lou , Guanjie Cheng , Chang Liu This is my paper
classification cs.CR cs.AI
keywords agent authorizationpermission graphSMT solverLLM agentstaint trackingruntime enforcementpermission IRaccess control
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

FAVA claims that agent authorization can be made formally checkable by separating semantic understanding from enforcement. An LLM parses natural-language tasks and runtime traces into a structured Permission IR; a deterministic lowering pass converts that IR into an evidence-backed permission graph; and an SMT solver decides, before every effectful action, whether any protected label can flow to a forbidden sink. The paper reports 90.5% decision compliance over 801 tasks, with 100% on structured trace-conditioned cases, and argues that the remaining failures stem from extraction misses, not from the solver. The broader claim is that this design converts the safety question into reachability on a graph that can be monotonically extended as new runtime events occur.

Core claim

The central discovery is that agent safety can be reduced to a satisfiability problem over a finite, evidence-backed permission graph. Each node carries security labels derived from evidence spans; each edge is typed as data, control, or parent; and policy rules are expressed as forbidden label-to-sink flows plus obligations encoded as Boolean guards over the execution prefix. The SMT authorizer propagates labels along edges unless a trusted sanitizer transforms them, checks that no protected-label node is granted a forbidden sink capability, and either returns a capability set or a counterexample trace. The paper's key claim is that, for a validated finite graph and fixed policy translation

What carries the argument

The evidence-backed permission graph (V,E) is the central object: nodes carry security labels and capability requests, edges encode data-flow, control-order, and parent-ancestry relations, and the SMT encoding (Algorithm 1) turns label propagation and forbidden label-to-sink rules into Boolean constraints over finite Boolean variables H[v,ℓ] and A[v,c]. Monotone runtime repair appends new nodes, edges, labels, and evidence, forcing re-authorization before each effectful action; because label propagation is monotonic and forbidden-flow checks are hard constraints, previously rejected actions stay rejected on taint-only extensions. The paper asserts two lemmas—Finite-Graph Soundness and Taint-

Load-bearing premise

The system is only as safe as the LLM's extraction: if a protected label, obligation, or data-flow edge is missed, the solver can certify a graph that permits a genuinely unsafe action; the paper also states but does not prove the soundness lemmas for the SMT encoding.

What would settle it

Construct a task where a file containing a secret is sent to a network endpoint, but the Permission IR omits the 'secret' label on that file; if the SMT authorizer returns an authorized capability set for the send action, the end-to-end guarantee is broken. Separately, to test the solver's soundness, construct a finite graph with a multi-hop path from a labeled node to a forbidden sink and check that Algorithm 1's local propagation actually detects it; a false negative here would refute the unproved Finite-Graph Soundness lemma.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • If the claim is correct, an agent gateway can provide a mathematically checkable binary decision before each effectful action, rather than relying on prompt-level instructions.
  • The approach implies that security policies expressible as label-to-sink reachability rules and prefix obligations are enforceable exactly, while other classes of policy require additional encoding.
  • Because the graph is monotonically extended, the system can detect when an action that was previously allowed becomes dangerous after sensitive data is accessed.
  • The reported per-call solver latency below 1 ms median suggests the formal check can sit in the real-time agent loop without dominating overhead.
  • The failure analysis implies that improving extraction quality (provenance-aware labeling and precise sink scoping) is the main lever for improving end-to-end compliance, not the decision rule.

Where Pith is reading between the lines

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

  • The formal guarantee is exactly as strong as the upstream extraction: an LLM that misses a protected label or data-flow edge yields a graph on which the SMT authorizer can certify an unsafe action, so FAVA's true security boundary is the extractor, not the solver.
  • The two soundness lemmas are asserted without proof; a formal verification of the encoding itself would be needed before the mathematical claim can be taken as established.
  • The same graph-and-solver core could be reused with a different, non-LLM evidence source (e.g., a provenance-aware runtime that records syscall-level flows) to close the extraction gap.
  • The fail-closed posture means the framework's practical tradeoff is between false positives and false negatives; the reported 69 false blocks suggest a deliberate sacrifice of utility for safety.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

4 major / 6 minor

Summary. FAVA is an authorization framework for LLM agents. It uses an LLM to parse task text, execution contracts, and runtime traces into a structured Permission IR; a deterministic lowering pass converts that IR into a permission graph carrying labels, data-flow edges, and capability requests; an SMT-based authorizer then decides, before each effectful action, whether a candidate capability set is consistent with forbidden label-to-sink policies. A runtime gateway either grants the capability set or blocks the action, optionally with a counterexample. The paper reports experiments on 801 tasks from OpenAgentSafety, OctoBench, and ActPlane scenarios, with an aggregate 90.5% Decision Compliance Rate, ablation studies, model-replacement tests, latency measurements, and a failure analysis.

Significance. The architecture is attractive: it separates LLM-based semantic extraction from a deterministic, checkable authorization step, and it is evaluated on external benchmarks with internally consistent aggregate numbers. The paper is also honest about the main external limitation: the formal guarantee starts only after extraction, and missed labels or edges can cause false negatives (RQ5, Discussion). However, the manuscript's central formal claims are not yet backed by the presented material. The soundness and monotonicity statements are asserted without proof, and the algorithm as written omits the obligation constraints that are a stated motivation of the system. In addition, the trace-conditioned benchmark uses oracle-provided evidence attached to violating nodes, which inflates the headline DCR. These issues are fixable within the scope of a revision, but they are load-bearing for the claimed guarantee and evaluation.

major comments (4)
  1. [SMT Authorization; Algorithm 1] The prose formalization introduces obligation guards, e.g. A[v,commit] ⇒ Seen(tp,v), but Algorithm 1 contains only label propagation (step 1), capability allocation (step 2), and forbidden-sink enforcement (step 3); no obligation assertion is present. Consequently, for a policy P that includes temporal rules such as "commit only after tests_passed", a satisfiable capability assignment can grant commit even when Seen(tp,v) is false. The Finite-Graph Soundness claim that a satisfiable assignment "strictly satisfy all policy rules encoded in P" is therefore not established for obligations, despite temporal policies being a central motivation. Please either add obligation constraints to the encoding and proof, or narrow the formal theorem to the class of forbidden label-to-sink rules actually encoded.
  2. [SMT Authorization] Finite-Graph Soundness and Taint-Monotonic Safety are asserted as prose paragraphs without proof. Additionally, the propagation equation H[v,ℓ] = Explicit(v,ℓ) ∨ Source(v,ℓ,P) ∨ ⋁_{u∈Pred(v)} H[u,ℓ] is a Boolean equality that is not well-defined on cyclic graphs: a self-loop with no explicit label admits both H=true and H=false as satisfying assignments. The paper does not state a DAG or stratification condition on the permission graph. A precise graph-well-formedness assumption and a proof of the soundness lemma are needed; otherwise the formal guarantee is itself an unverified assumption.
  3. [RQ2; Table 3; Abstract] The paper states that edge ablation "minimally impacts the 190-trace setting because our current ingestion explicitly attaches benchmark-provided trace evidence to violating nodes, reinforcing this split as a labeled diagnostic rather than zero-shot discovery." Since 190 of the 801 cases receive oracle evidence tied to the violating nodes, the 100% DCR on ActPlane Traces and the aggregate 90.5% DCR do not demonstrate zero-shot dynamic interception. Excluding the trace split, the per-benchmark numbers in Table 2 give roughly 87.6% DCR on the remaining 611 cases. Please report the aggregate without the oracle split and qualify the abstract's "successfully intercepting dynamic violating traces" claim accordingly.
  4. [Introduction; Enforcement Gateway] The Introduction's central dichotomy — "FAVA returns either a counterexample to intercept forbidden flows or a capability set to authorize backend execution" — is contradicted by the gateway's deliberate fail-closed behavior: when no forbidden flow is found but the extracted risk posture is "sensitive, dangerous, or ambiguous", the action is blocked without producing a counterexample. This third outcome should be included in the formal statement, or the fail-closed path should be modeled as an explicit policy outcome rather than an unstated exception.
minor comments (6)
  1. [Figure 2] Typos: "Execuite" should be "Execute" and "Monotinic" should be "Monotonic".
  2. [Motivation: Agent Constraints] The empirical study reports that 90% of repositories enforce temporal constraints and over 40% use nested conditional logic, but no sample size, repository-selection details, or annotation procedure are given. A brief methodological paragraph would help assess the motivation claim.
  3. [Experiments; Baselines] AuthGraph and SafeAgent are described as best-effort reimplementations over the FAVA interface because public implementations are unavailable. This is a significant caveat for head-to-head comparison; please state more prominently in the main text and avoid implying the original systems' exact behavior is being compared.
  4. [RQ2] The admission that benchmark-provided trace evidence is attached to violating nodes appears only in the ablation discussion. It should be stated in the dataset description, so readers can interpret the trace-conditioned results correctly.
  5. [Algorithm 1; Implementation] The secondary solver pass for counterexample extraction is described only in prose. If the constraints are unsatisfiable for reasons other than a forbidden flow (e.g., an obligation guard under a future encoding), it is unclear what the counterexample represents. Please clarify the extraction procedure.
  6. [RQ4; Table 4] Latency is measured on small graphs (the largest bucket contains only 3 observed cases). The claim that solving "naturally scales with topological complexity" would benefit from a stress test with larger permission graphs or synthetic scale-out experiments.

Circularity Check

1 steps flagged

Only minor disclosed evaluation circularity in the trace-conditioned diagnostic; formal core is not circular.

specific steps
  1. fitted input called prediction [RQ2 Component Ablations (ActPlane trace-conditioned split)]
    "our current ingestion explicitly attaches benchmark-provided trace evidence to violating nodes, reinforcing this split as a labeled diagnostic rather than zero-shot discovery."

    The 100.0% DCR reported for ActPlane Traces is achieved by attaching the benchmark's own ground-truth trace evidence to violating nodes before evaluation. The 'interception' outcome is therefore generated from the answer supplied in the input, not independently discovered. The authors explicitly disclose this and separate the split as a diagnostic, so it is a minor and acknowledged evaluation circularity rather than a load-bearing formal claim.

full rationale

FAVA's central formal claim is explicitly scoped to the permission graph: 'Under the stated graph, policy, gateway, and backend assumptions, FAVA returns either a counterexample to intercept forbidden flows or a capability set to authorize backend execution.' The SMT check is a satisfiability encoding of label propagation and forbidden sink collisions, so its soundness relative to the encoded graph is definitional rather than an empirical prediction. No fitted parameters are renamed as predictions, and no load-bearing result is imported solely from author self-citation. The main evaluation caveat is the trace-conditioned split, which uses benchmark-provided trace evidence attached to violating nodes; the paper discloses this and labels it a diagnostic, not zero-shot discovery. The skeptic's concern that Algorithm 1 omits obligation constraints is a correctness gap in the proof/encoding, not a circularity: the stated lemmas are asserted without proof, but that does not make the derivation equivalent to its inputs. Overall, the non-trivial engineering contribution—deterministic graph lowering plus SMT enforcement—is externally evaluated, and no central claim reduces to its own assumptions. Score is 2 due solely to the minor, acknowledged trace-conditioned evaluation circularity.

Axiom & Free-Parameter Ledger

0 free parameters · 6 axioms · 0 invented entities

No numeric parameters are fitted to data. The reported DCR values are measurements over fixed benchmark ground truth; the only tunable design choice is the fail-closed heuristic (blocking sensitive/dangerous/ambiguous actions), which is a policy default, not a fitted constant. The 69 false blocks and 57.7% benign allow rate are consequences of this fixed posture, not regression results. The Permission IR, permission graph, security labels, and capability sets are internal abstractions defined in the paper, not independently evidenced entities, so they are design artifacts rather than invented entities in the ledger's sense.

axioms (6)
  • domain assumption All security-relevant runtime effects are mediated by the gateway before execution.
    Explicitly stated in 'Security Assumptions and System Scope'; if the agent can execute an effect without gateway interception, the guarantee fails.
  • domain assumption Backends are capability-conformant: they may restrict more than the solver permits but never execute outside the granted capability set.
    Same section; the enforcement chain depends on backends honoring the granted capabilities.
  • domain assumption Policy translation and sanitizer specifications are treated as part of the trusted computing base.
    Same section; if sanitizer specs are wrong (e.g., a 'redact' that doesn't remove the secret), taint is cleared incorrectly.
  • domain assumption The LLM extraction of Permission IR is faithful enough to preserve all security-relevant labels, obligations, and edges.
    The formal guarantee begins after lowering; the paper admits false negatives from extraction misses (RQ5, 26.6% of failures) and that FAVA does not prove end-to-end safety from natural language.
  • ad hoc to paper Algorithm 1's label propagation and capability allocation correctly encode reachability and policy semantics.
    The 'Finite-Graph Soundness' paragraph asserts soundness without a proof or machine-checked verification; the encoding's correctness is assumed rather than demonstrated.
  • standard math Z3 SMT solver is sound for the emitted formulas.
    Standard tooling assumption; relies on Z3's published correctness.

pith-pipeline@v1.3.0-daily-deepseek · 12288 in / 17904 out tokens · 140299 ms · 2026-08-01T10:54:33.245478+00:00 · methodology

0 comments
read the original abstract

Large language model (LLM) agents autonomously interleave semantic reasoning with complex system operations. In these dynamic environments, static tool-level permissions are fundamentally insufficient; safe authorization is highly context-dependent and heavily reliant on evolving runtime states and data flows. We present FAVA (Formal Authorization for Verified Agents), a permission-carrying authorization framework for agent execution. FAVA utilizes an LLM-guided Permission Intermediate Representation (IR) to translate ambiguous natural-language tasks into structured constraints. A deterministic lowering pass then converts this IR into an evidence-backed permission graph that explicitly tracks data flows, dependencies, and contextual labels. To provide strict security guarantees, a Satisfiability Modulo Theories (SMT) authorizer mathematically verifies the current graph against security policies before any effectful action executes. A runtime gateway then enforces the solver's result, either authorizing the execution or intercepting it with a precise counterexample. We evaluate FAVA across OpenAgentSafety, OctoBench, and ActPlane scenarios. Our evaluation demonstrates that FAVA achieves a 90.5% Decision Compliance Rate (DCR) over the aggregate dataset, successfully intercepting dynamic violating traces in the evaluated trace-conditioned scenarios.

Figures

Figures reproduced from arXiv: 2607.27267 by Chang Liu, Guanjie Cheng, Hengxuan Lou, Sai Liu, Xinkui Zhao, Yifan Zhang.

Figure 1
Figure 1. Figure 1: Frequency of dynamic constraints extracted from [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: FAVA architecture. The system extracts inputs into a Permission IR, lowers it into an evidence-backed graph, and enforces security via an SMT authorizer and runtime gateway. The graph is monotonically updated with new observations. Graph Lowering To enforce sequence-dependent temporal constraints, flat permission lists are structurally insufficient. Instead, a de￾terministic lowering pass maps the Permissi… view at source ↗
Figure 3
Figure 3. Figure 3: Model replacement results. Bars show DCR per [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figure 5
Figure 5. Figure 5: Failure buckets for the mismatched cases. [PITH_FULL_IMAGE:figures/full_fig_p007_5.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

47 extracted references · 11 linked inside Pith

  1. [1]

    Communication, Simulation, and Intelligent Agents: Implications of Personal Intelligent Machines for Medical Education

    Clancey, William J. Communication, Simulation, and Intelligent Agents: Implications of Personal Intelligent Machines for Medical Education. Proceedings of the Eighth International Joint Conference on Artificial Intelligence (IJCAI-83)

  2. [2]

    arXiv preprint arXiv:2605.26497 , year=

    Aligning Provenance with Authorization: A Dual-Graph Defense for LLM Agents , author=. arXiv preprint arXiv:2605.26497 , year=

    Pith/arXiv arXiv

  3. [3]

    arXiv preprint arXiv:2606.25189 , year=

    ActPlane: Programmable OS-Level Policy Enforcement for Agent Harnesses , author=. arXiv preprint arXiv:2606.25189 , year=

    Pith/arXiv arXiv

  4. [4]

    ICML 2025 workshop on computer use agents , year=

    Guardagent: safeguard LLM agents via knowledge-enabled reasoning , author=. ICML 2025 workshop on computer use agents , year=

    2025

  5. [5]

    arXiv preprint arXiv:2503.18666 , year=

    Agentspec: Customizable runtime enforcement for safe and reliable llm agents , author=. arXiv preprint arXiv:2503.18666 , year=

    Pith/arXiv arXiv

  6. [6]

    and Hashimoto, Tatsunori , year = 2024, eprint =

    Ruan, Yangjun and Dong, Honghua and Wang, Andrew and Pitis, Silviu and Zhou, Yongchao and Ba, Jimmy and Dubois, Yann and Maddison, Chris J. and Hashimoto, Tatsunori , year = 2024, eprint =. Identifying the Risks of

    2024

  7. [7]

    AgentDojo : A Dynamic Environment to Evaluate Prompt Injection Attacks and Defenses for LLM Agents

    Debenedetti, Edoardo and Zhang, Jie and Balunovi. AgentDojo : A Dynamic Environment to Evaluate Prompt Injection Attacks and Defenses for LLM Agents. 2406.13352 , archivePrefix =

    Pith/arXiv arXiv

  8. [8]

    OpenAgentSafety : A Comprehensive Framework for Evaluating Real-World AI Agent Safety

    Vijayvargiya, Viraj and Soni, Sarthak and others , year = 2025, eprint =. OpenAgentSafety : A Comprehensive Framework for Evaluating Real-World AI Agent Safety

    2025

  9. [9]

    Securing

    Costa, Manuel and Kopf, Boris and Kolluri, Aashish and Paverd, Andrew and Russinovich, Mark and Salem, Ahmed and Tople, Shruti and Wutschitz, Lukas and Zanella-B. Securing. 2505.23643 , archivePrefix =

    Pith/arXiv arXiv

  10. [10]

    Agent-SafetyBench : Evaluating the Safety of LLM Agents

    Zhang, Zhexin and Cui, Shiyao and Lu, Yida and Zhou, Jingzhuo and Yang, Junxiao and Wang, Hongning and Huang, Minlie , year = 2025, eprint =. Agent-SafetyBench : Evaluating the Safety of LLM Agents

    2025

  11. [11]

    InjecAgent : Benchmarking Indirect Prompt Injections in Tool-Integrated Large Language Model Agents

    Zhan, Qiusi and Liang, Zhixiang and Ying, Zifan and Kang, Daniel , booktitle =. InjecAgent : Benchmarking Indirect Prompt Injections in Tool-Integrated Large Language Model Agents. doi:10.18653/v1/2024.findings-acl.624 , url =

    doi:10.18653/v1/2024.findings-acl.624 2024

  12. [12]

    Agent Security Bench (ASB) : Formalizing and Benchmarking Attacks and Defenses in LLM -based Agents

    Zhang, Hanrong and Huang, Jingyuan and Mei, Kai and Yao, Yifei and Wang, Zhenting and Zhan, Chenlu and Wang, Hongwei and Zhang, Yongfeng , year = 2024, eprint =. Agent Security Bench (ASB) : Formalizing and Benchmarking Attacks and Defenses in LLM -based Agents

    2024

  13. [13]

    VIGIL : Runtime Enforcement of Behavioral Specifications in AI Agent Skills

    Li, Ying and Chen, Yanju and Wen, Hongbo and Zhang, Bosi and Liu, Hanzhi and Wang, Peiran and Feng, Yu and Tian, Yuan , year = 2026, eprint =. VIGIL : Runtime Enforcement of Behavioral Specifications in AI Agent Skills

    2026

  14. [14]

    AgentMonitor : A Plug-and-Play Framework for Predictive and Secure Multi-Agent Systems

    Naihin, Arsenii and Choi, Seungwook and Yi, Ren and Suciu, Octavian and Doyuran, Bora and Kwon, Yongdae and others , year = 2023, eprint =. AgentMonitor : A Plug-and-Play Framework for Predictive and Secure Multi-Agent Systems

    2023

  15. [15]

    R-Judge : Benchmarking Safety Risk Awareness for LLM Agents

    Yuan, Tong and others , year = 2024, eprint =. R-Judge : Benchmarking Safety Risk Awareness for LLM Agents

    2024

  16. [16]

    International conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=

    Z3: An efficient SMT solver , author=. International conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=. 2008 , organization=

    2008

  17. [17]

    Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) , pages=

    Octobench: Benchmarking scaffold-aware instruction following in repository-grounded agentic coding , author=. Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) , pages=

  18. [18]

    2024 , note =

    Docker. 2024 , note =

    2024

  19. [19]

    IEEE Transactions on Computers , year=

    UKFaaS: Lightweight, High-Performance and Secure FaaS Communication With Unikernel , author=. IEEE Transactions on Computers , year=

  20. [20]

    arXiv preprint arXiv:2409.16427 , year=

    Haicosystem: An ecosystem for sandboxing safety risks in human-ai interactions , author=. arXiv preprint arXiv:2409.16427 , year=

    Pith/arXiv arXiv

  21. [21]

    International Conference on Learning Representations , volume=

    Identifying the risks of lm agents with an lm-emulated sandbox , author=. International Conference on Learning Representations , volume=

  22. [22]

    34th USENIX Security Symposium (USENIX Security 25) , pages=

    Unsafe \ LLM-Based \ Search: Quantitative Analysis and Mitigation of Safety Risks in \ AI \ Web Search , author=. 34th USENIX Security Symposium (USENIX Security 25) , pages=

  23. [23]

    arXiv preprint arXiv:2508.18765 , year=

    Governance-as-a-service: A multi-agent framework for ai system compliance and policy enforcement , author=. arXiv preprint arXiv:2508.18765 , year=

    Pith/arXiv arXiv

  24. [24]

    arXiv preprint arXiv:2606.15508 , year=

    ToolMenuBench: Benchmarking Tool-Menu Filtering Strategies for Reliable and Efficient LLM Agents , author=. arXiv preprint arXiv:2606.15508 , year=

    arXiv

  25. [25]

    International Conference on Learning Representations , volume=

    Agentharm: A benchmark for measuring harmfulness of llm agents , author=. International Conference on Learning Representations , volume=

  26. [26]

    arXiv preprint arXiv:2307.15043 , year=

    Universal and transferable adversarial attacks on aligned language models , author=. arXiv preprint arXiv:2307.15043 , year=

    Pith/arXiv arXiv

  27. [27]

    arXiv preprint arXiv:2604.28138 , year=

    Crab: A Semantics-Aware Checkpoint/Restore Runtime for Agent Sandboxes , author=. arXiv preprint arXiv:2604.28138 , year=

    Pith/arXiv arXiv

  28. [28]

    arXiv preprint arXiv:2602.09345 , year=

    AgentCgroup: Understanding and controlling OS resources of AI agents , author=. arXiv preprint arXiv:2602.09345 , year=

    Pith/arXiv arXiv

  29. [29]

    Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) , pages=

    Followbench: A multi-level fine-grained constraints following benchmark for large language models , author=. Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) , pages=

  30. [30]

    md Files on the Efficiency of AI Coding Agents , author=

    On the Impact of AGENTS. md Files on the Efficiency of AI Coding Agents , author=. arXiv preprint arXiv:2601.20404 , year=

    arXiv

  31. [31]

    International Conference on Product-Focused Software Process Improvement , pages=

    On the use of agentic coding manifests: An empirical study of claude code , author=. International Conference on Product-Focused Software Process Improvement , pages=. 2025 , organization=

    2025

  32. [32]

    arXiv preprint arXiv:2511.12884 , year=

    Agent READMEs: An Empirical Study of Context Files for Agentic Coding , author=. arXiv preprint arXiv:2511.12884 , year=

    arXiv

  33. [33]

    Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security , pages=

    Poster: Agentic Shell Honeypot Using Structured Logging , author=. Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security , pages=

    2025

  34. [34]

    Companion Proceedings of the ACM on Web Conference 2025 , pages=

    Sortinghat: Redefining operating systems education with a tailored digital teaching assistant , author=. Companion Proceedings of the ACM on Web Conference 2025 , pages=

    2025

  35. [35]

    Advances in Neural Information Processing Systems , volume=

    Swe-agent: Agent-computer interfaces enable automated software engineering , author=. Advances in Neural Information Processing Systems , volume=

  36. [36]

    International Conference on Learning Representations , volume=

    Openhands: An open platform for ai software developers as generalist agents , author=. International Conference on Learning Representations , volume=

  37. [37]

    Classification Problem Solving

    Clancey, William J. Classification Problem Solving. Proceedings of the Fourth National Conference on Artificial Intelligence

  38. [38]

    , title =

    Robinson, Arthur L. , title =. 1980 , doi =. https://science.sciencemag.org/content/208/4447/1019.full.pdf , journal =

    1980

  39. [39]

    New Ways to Make Microcircuits Smaller---Duplicate Entry

    Robinson, Arthur L. New Ways to Make Microcircuits Smaller---Duplicate Entry. Science

  40. [40]

    Clancey and Glenn Rennels , abstract =

    Diane Warner Hasling and William J. Clancey and Glenn Rennels , abstract =. Strategic explanations for a diagnostic consultation system , journal =. 1984 , issn =. doi:https://doi.org/10.1016/S0020-7373(84)80003-6 , url =

    doi:10.1016/s0020-7373(84)80003-6 1984

  41. [41]

    and Rennels, Glenn R

    Hasling, Diane Warner and Clancey, William J. and Rennels, Glenn R. and Test, Thomas. Strategic Explanations in Consultation---Duplicate. The International Journal of Man-Machine Studies

  42. [42]

    Poligon: A System for Parallel Problem Solving

    Rice, James. Poligon: A System for Parallel Problem Solving

  43. [43]

    Transfer of Rule-Based Expertise through a Tutorial Dialogue

    Clancey, William J. Transfer of Rule-Based Expertise through a Tutorial Dialogue

  44. [44]

    The Engineering of Qualitative Models

    Clancey, William J. The Engineering of Qualitative Models

  45. [45]

    2023 , eprint=

    Attention Is All You Need , author=. 2023 , eprint=

    2023

  46. [46]

    Pluto: The 'Other' Red Planet

    NASA. Pluto: The 'Other' Red Planet

  47. [47]

    arXiv preprint arXiv:2604.17562 , year=

    SafeAgent: A runtime protection architecture for agentic systems , author=. arXiv preprint arXiv:2604.17562 , year=

    Pith/arXiv arXiv