ETAS: An Effect-Typed Language for Agent Systems

• URL: http://arxiv.org/abs/2607.17780v1
• Date: Mon, 20 Jul 2026 10:11:53 GMT
• Title: ETAS: An Effect-Typed Language for Agent Systems
• Abstract summary: ETAS is a programming language for agent systems.<n>It treats model-backed agents, tool calls, prompts, typed memory, human approvals, policies, and execution traces as semantic program elements.
• Score: 3.1440390119576676
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: ETAS is a programming language for agent systems that treats model-backed agents, tool calls, prompts, typed memory, human approvals, policies, and execution traces as semantic program elements rather than library conventions. It separates deterministic computation from agentic nondeterminism and externally visible actions while preserving a direct programming style. We present the core design of ETAS. Its static semantics assigns ordinary types through spec conformance and tracks each computation with two behavioral indices: an escaping effect row and a persistent abstraction of the typed action trace it may request. Specs form a terminating compile-time constraint calculus: type specs provide evidence for polymorphism and resource facts, callable specs constrain function and stage shapes, and trace specs express allow, deny, and temporal constraints. Typing checks requested traces against compiled monitors and emits residual obligations when dynamic resources preclude a complete static proof. The dynamic semantics distinguish requested, handled, denied, and committed events; handlers interpret typed actions without making their requests invisible to authorization or audit. We formalize a core calculus and state preservation, progress, type/effect soundness, handler trace-transparency, and policy safety. We also implement ETAS in Rust with a command-line interface, typed HIR checks, effect and policy diagnostics, handler checks, and trace-aware execution hooks. ETAS provides a programming-language foundation for reasoning about authorization, nondeterminism, recovery, and audit evidence before and during agent execution.

Related papers

• From Natural Language Policies to Executable Obligations: A Verification Harness for Dependable In-Car LLM Agents [0.5352699766206808]
  We present AgentGuardUtil, our entry to CAR-bench Track1, which treats the AI planer (LLM) as a fallible proposer inside a grounded verify-and-revise loop.<n>The natural-language policy shipped with each conversation is compiled, once per policy, into typed machine-checkable rules.<n>A deterministic obligation engine interprets these rules against live tool results and the simulated post-write state of the draft itself.
  arXiv  Detail & Related papers  (2026-08-24T14:06:21Z)
• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  Agentic systems driven by large language models (LLMs) are increasingly deployed in real-world where they act on persistent operational data.<n>Existing approaches do not provide such system-level guarantees.<n>We study here the verification of agentic systems comprising a single LLM and a tool orchestration harness over relational operational data.
  arXiv  Detail & Related papers  (2026-08-04T13:01:30Z)
• PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
  We present PhyAgentOS, a foundation delivering scheduling, verification, memory, benchmarking, and safety as system-level services.<n>Its Session-Centered treats a session, not an action, as the minimum unit of scheduling, compatibility, supervised execution, evidence collection, and acceptance.<n>SessionVerifier distinguishes execution termination from semantic task completion via evidence-grounded verdicts of success, failure, or replan.<n> Benchmarking reuses the deployment session and verification path, so results trace to real execution.
  arXiv  Detail & Related papers  (2026-07-18T04:46:53Z)
• TTHE: Test-Time Harness Evolution [50.26245555541721]
  Existing approaches optimize such harnesses before deployment, searching training or development data for a fixed agent workflow that is then frozen at test time.<n>We ask whether the harness can instead be optimized during evaluation itself, using only the unlabeled execution traces the agent produces on the test inputs.<n>During evaluation, TTHE maintains a population of candidate harnesses and refines them through an agentic proposer that reasons over their execution traces.<n>A judge then commits an improved harness from execution-derived proxy signals, and the selected program persists to govern subsequent inputs.
  arXiv  Detail & Related papers  (2026-07-09T05:53:39Z)
• VIGIL: Runtime Enforcement of Behavioral Specifications in AI Agent Skills [13.980239249972819]
  VIGIL is an end-to-end runtime enforcement framework for agentic systems.<n>It checks an agent's actual execution trace against behavioral policies from skill specifications, operator-defined constraints, and global rules spanning multiple skills.<n>It detects policy violations with over 95% recall and a false-positive rate below 10%.
  arXiv  Detail & Related papers  (2026-06-25T01:58:44Z)
• A Physical Agentic Loop for Language-Guided Grasping with Execution-State Monitoring [5.437966695589128]
  We reformulate language-guided grasping as a bounded embodied agent operating over grounded execution states.<n>We introduce a physical agentic loop that wraps an unmodified learned manipulation primitive.<n>We validate the resulting loop on a mobile manipulator with an eye-in-hand D405 camera.
  arXiv  Detail & Related papers  (2026-04-08T08:01:35Z)
• Dynamic analysis enhances issue resolution [53.50448142467294]
  DAIRA (Dynamic Analysis-enhanced Issue Resolution Agent) is an automated repair framework that embeds dynamic analysis into the agent's reasoning cycle.<n> Driven by a Test Tracing-Driven methodology, DAIRA utilizes lightweight monitors to extract critical runtime data.<n>When powered by Gemini 3 Flash Preview, DAIRA establishes a new state-of-the-art (SOTA) performance, achieving a 79.4% resolution rate on the SWE-bench Verified dataset.
  arXiv  Detail & Related papers  (2026-03-23T14:48:54Z)
• Agentproof: Static Verification of Agent Workflow Graphs [0.0]
  Agent frameworks increasingly encode tool-using behavior as explicit workflow graphs, yet safety enforcement remains a runtime concern.<n>This paper presents Agentproof, a system that automatically extracts a unified abstract graph model from four major agent frameworks.<n>Unlike general-purpose model checkers, Agentproof requires no manual modeling.
  arXiv  Detail & Related papers  (2026-03-20T13:56:20Z)
• TriCEGAR: A Trace-Driven Abstraction Mechanism for Agentic AI [5.1181001367075]
  TriCEGAR is a trace-driven abstraction mechanism that automates state construction from execution logs.<n>We describe a framework-native implementation that captures typed agent lifecycle events and builds abstractions from traces.<n>We also show how run likelihoods enable anomaly detection as a guardrailing signal.
  arXiv  Detail & Related papers  (2026-01-30T14:01:47Z)
• Deriving Character Logic from Storyline as Codified Decision Trees [67.01182739162142]
  Role-playing (RP) agents rely on behavioral profiles to act consistently across diverse narrative contexts.<n>We propose Codified Decision Trees (CDT), a data-driven framework that induces an executable and interpretable decision structure from large-scale narrative data.
  arXiv  Detail & Related papers  (2026-01-15T05:12:43Z)
• DRIFT: Dynamic Rule-Based Defense with Injection Isolation for Securing LLM Agents [52.92354372596197]
  Large Language Models (LLMs) are increasingly central to agentic systems due to their strong reasoning and planning capabilities.<n>This interaction also introduces the risk of prompt injection attacks, where malicious inputs from external sources can mislead the agent's behavior.<n>We propose a Dynamic Rule-based Isolation Framework for Trustworthy agentic systems, which enforces both control and data-level constraints.
  arXiv  Detail & Related papers  (2025-06-13T05:01:09Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.