arXiv:2605. 09045v2 Announce Type: replace Abstract: Agentic frameworks are the software layer through which AI agents act in the world.
arXiv:2608. 14590v1 Announce Type: new Abstract: LLM agents increasingly perform irreversible real-world actions, including database updates, API calls, file operations, and autonomous use of tools.
arXiv:2608. 03609v1 Announce Type: new Abstract: Agentic systems driven by large language models (LLMs) are increasingly deployed in real-world workflows where they act on persistent operational data.
arXiv:2608. 11274v1 Announce Type: cross Abstract: The dominant paradigm treats AI safety as a property to be instilled during model training via RLHF, DPO, or Constitutional AI.
The paper introduces MAGS, a multi-agent framework that automatically generates executable programs with formal safety guarantees. MAGS translates LLM-generated code into the verification-aware language Dafny, repairs any safety violations using verifier feedback, and then compiles the verified code back into executable form. Evaluations on 220 diverse examples—including CUDA kernels, terminal scripts, and robotic-arm tasks—show a 100% success rate in producing programs that meet frozen safety specifications, with additional safety and functional tests confirming strong performance across domains.
arXiv:2602. 20064v2 Announce Type: replace-cross Abstract: Large language models are increasingly deployed as agents: they plan, call tools, read untrusted data, and act on the results.
Sapien is a policy engine that enforces stateful contextual policies for autonomous AI agents, specifying allowed tool‑call sequences with an extended regular expression that includes stateful predicates, deferred policy generation, and scoped semantic checks. The system maintains performance close to an unconstrained agent while significantly reducing malicious actions, ruling out 93‑95% of attacks on AgentDojo and 62‑85% on Toolathlon, outperforming traditional tool allowlists on long‑horizon tasks.
ContrAgent is a contract‑based framework that provides symbolic temporal supervision for large language model agents. It records an agent’s tool‑call sequence as a trace of checkable predicates and formalizes desired behaviors with assume‑guarantee contracts expressed in linear temporal logic over finite traces (LTLf). Each contract is compiled into a deterministic finite automaton that both gates actions online and evaluates recorded traces offline, enabling deterministic, reproducible verdicts and significantly lower per‑call latency compared to existing LLM‑judge and rule‑based guardrail baselines.
arXiv:2606. 26057v1 Announce Type: cross Abstract: AI agents are granted access to tools, APIs, and other infrastructure, making them active principals in those systems.
arXiv:2510. 12985v3 Announce Type: replace Abstract: We present SENTINEL, a framework for formally evaluating the physical safety of foundation model (FM)-based embodied agents.
arXiv:2607. 16266v1 Announce Type: cross Abstract: Existing approaches for reasoning about action and change provide expressive semantics for modeling dynamic systems, in most cases built on top of logic programming systems.
arXiv:2607. 03561v1 Announce Type: new Abstract: As AI models continue to develop powerful capabilities, it becomes critical that we are able to verify that their output is aligned with our intentions.
arXiv:2607. 17780v1 Announce Type: cross 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.