Skip to content
Preprint

SkillEffect: Checked Lowering for Memory-Bounded Agent Tools

Aug 2026 · 0 citations · 33 references
Computer Science

TL;DR

SkillEffect is presented, a checked-lowering runtime for computations with a recoverable source relation, an audited bounded implementation, and a registered output postcondition that shows that one checked-lowering architecture can enforce heterogeneous registered memory relations at Agent tool dispatch.

Abstract

Agent Skills can specify procedural and resource obligations for tool use, and language models instantiate them as concrete programs. However, when models turn this guidance into code for existing tool interfaces, even a semantically correct program may load an entire input and exceed the memory available to one tool call. We present SkillEffect, a checked-lowering runtime for computations with a recoverable source relation, an audited bounded implementation, and a registered output postcondition. Before granting execution authority, an independent checker rebuilds each proposed lowering from the submitted program and immutable input. Every relation plugin supplies a source recognizer, input-fact extractor, bounded-IR constructor, arena-bound function, and postcondition; one common runtime provides checked selection, bounded-VM execution, atomic capacity leasing, and staged publication. Generality in SkillEffect is architectural rather than automatic: each supported computation requires an audited relation plugin, while the dispatch, resource-control, execution, and publication mechanisms are shared across plugins. Across six operator families, bounded access substantially reduces peak memory and improves completion under externally fixed caps. Six plugins instantiate the same contract across five execution patterns, from streaming reduction to bounded-heap Top-k. The XLSX onboarding study and Top-k extension show that a new relation and a new retained-state pattern reuse the same trust boundary, while the checker accepts all evaluated legal configurations and rejects all adversarial proposals. Together, these results show that one checked-lowering architecture can enforce heterogeneous registered memory relations at Agent tool dispatch.

View source

Similar papers

Jul 2026

SIGIL: Compiling Agent Skills into Typed Harnesses

These results show that compiling procedural structure improves the reliability and efficiency of skill execution while retaining model judgment where it is needed, and shows that compiling procedural structure improves the reliability and efficiency of skill execution while retaining model judgment where it is needed.

Jayanaka L. Dantanarayana, Savini Kashmira, Lingjia Tang et al. · 1 citation
Preprint Jul 2026

SIGIL: Compiling Agent Skills into Typed Harnesses

Skill Compilation is introduced, realized in SIGIL, which compiles a prose skill into an executable harness, and is model-independent: the harness holds at 86% across two model generations while prose swings from 56% to 68%.

Jayanaka L. Dantanarayana, Savini Kashmira, Lingjia Tang et al. · 0 citations
#artificial intelligence Preprint Aug 2026

CEDAR: Automata as Verifiable Interfaces for Language-Guided Embodied Action

CEDAR is presented, a counterexample-guided framework that grounds instructions as regular languages over environment event traces and represents both skills and specifications as deterministic finite automata, suggesting that regular languages offer a practical verification layer between natural-language instructions and embodied-agent policies.

Le Chen, Alvaro Velasquez, Ashutosh Trivedi · 0 citations
Jul 2026

ETAS: An Effect-Typed Language for Agent Systems

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.

Huiri Tan, Yi-Kun Wang, Puyang Zhang et al. · 0 citations
Preprint Jul 2026

Verified Tool Calls Improve LLM Agent Reliability Under Non-Atomic Failures

The findings suggest that strengthening tool interaction semantics is a promising direction for improving LLM agent reliability without requiring modifications to the underlying language model.

Isham Kalappurackal Mansoor, Abhishek Phadke, Pratip Rana · 3 citations
Jul 2026

SLBench: Evaluating How LLM Agents Follow Logical Relations in Skills

This work introduces SkillLogic, a framework for analyzing logical relations in skill files and constructing executable tests from them, and establishes logical-relation following as a distinct reliability challenge for skill-guided agents.

Xuan Chen, Chengpeng Wang, Lu Yan et al. · 0 citations

We use cookies to run the site and, with your consent, for analytics and to show ads. See our Cookie Policy.