Skills as Verifiable Artifacts: A Trust Schema and a Biconditional Correctness Criterion for Human-in-the-Loop Agent Runtimes

• URL: http://arxiv.org/abs/2605.00424v1
• Date: Fri, 01 May 2026 05:53:05 GMT
• Title: Skills as Verifiable Artifacts: A Trust Schema and a Biconditional Correctness Criterion for Human-in-the-Loop Agent Runtimes
• Abstract summary: We argue that a skill is emphuntrusted code until it is verified.<n>Without skill verification, a human-in-the-loop gate must fire on every irreversible call.<n>We give a trust schema that includes an explicit verification level on every skill manifest.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Agent skills -- structured packages of instructions, scripts, and references that augment a large language model (LLM) without modifying the model itself -- have moved from convenience to first-class deployment artifact. The runtime that loads them inherits the same problem package managers and operating systems have always faced: a piece of content claims a behavior; the runtime must decide whether to believe it. We argue this paper's central thesis up front: a skill is \emph{untrusted code} until it is verified, and the runtime that loads it must enforce that default rather than infer trust from a signature, a clearance, or a registry of origin. Without skill verification, a human-in-the-loop (HITL) gate must fire on every irreversible call -- which is operationally untenable and degrades into rubber-stamping at any non-trivial scale. With skill verification treated as a separate, gated process, HITL fires only for what is unverified, and the system becomes sustainable. We give a trust schema (§\ref{sec:schema}) that includes an explicit verification level on every skill manifest; a capability gate (§\ref{sec:gate}) whose HITL policy is a function of that verification level; a \emph{biconditional} correctness criterion (§\ref{sec:biconditional}) that any candidate verification procedure must satisfy on an adversarial-ensemble exercise (§\ref{sec:eval}); and a portable runtime profile (§\ref{sec:guidelines}) with ten normative guidelines abstracted from a working open-source reference implementation \cite{metere2026enclawed}. The contribution is harness- and model-agnostic; nothing here requires retraining, fine-tuning, or proprietary infrastructure.

Related papers

• 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)
• Agent Security Needs Redefinition through a Holistic Framework [46.88917910966891]
  Defenses ask whether an instruction looks malicious. Benchmarks ask whether an agent performs a harmful sounding action.<n>We operationalize contextual security through four properties that must hold jointly and be evaluated continuously across the agent's trajectory.
  arXiv  Detail & Related papers  (2026-07-24T06:43:09Z)
• Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis [14.825615940318038]
  ZkEVMs generate zero-knowledge that guarantee off-chain execution correctness.<n> subtle implementation bugs can lead to valid proofs certifying semantically faulty states.<n>Formal verification via SMT solvers can prevent this, but is bottlenecked by specification.<n>We propose Veri Synth, a framework that synthesizes executable Python/Z3 verification models from Rust.
  arXiv  Detail & Related papers  (2026-07-22T06:20:36Z)
• AEVAL: From Anecdotal to Deterministic Testing for Agentic Skill Workflows [1.6785141970297952]
  AEVAL (Agentic Evaluation) is a CI-integrated framework that replaces this practice with a deterministic, reproducible test pipeline for agentic skills.<n>Every skill change triggers a test event: the skill runs against a developer declared evaluation contract inside an automated executor.<n>A key ingredient is a structural separation between executor and grader, preventing a subtle but pervasive failure mode.
  arXiv  Detail & Related papers  (2026-07-16T21:33:05Z)
• 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)
• VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
  We introduce VASO, a framework for verification-guided self-evolution of robot skill contracts.<n>VASO verifies logically inconsistent skill contracts, then verifies plans induced by the skill against global and local temporal specifications.<n>On Clearpath Jackal and PX4 quadcopter tasks, VASO reaches 97.2% formal-specification compliance using fewer than 100 optimization samples.
  arXiv  Detail & Related papers  (2026-06-03T20:02:35Z)
• Securing LLM Agents Need Intent-to-Execution Integrity [49.490963596514185]
  We argue that securing LLM agents requires defining an end-to-end correctness property that specifies when an agent's execution faithfully reflects the user's intent.<n>We observe that LLM agents are structurally analogous to compilers, where security violations correspond to mis-executions that do not preserve user intent.<n>We derive four integrity properties that must hold simultaneously: emphTool Integrity, emphInstruction Integrity, emphJudgment Integrity, and emphData Flow Integrity.
  arXiv  Detail & Related papers  (2026-05-16T12:53:31Z)
• Methods for Formal Verification of Agent Skills: Three Layers Toward a Mechanically Checkable Capability-Containment Proof [0.0]
  We give a precise semantics for skill behaviour faithful to how a skill is consumed by an LLM-driven runtime.<n>We present three composable methods that together raise a skill from declared or tested to formal.<n>All three methods plus the bundle producer and re-checker ship as zero-dependency JavaScript modules in the open-source enclawed framework.
  arXiv  Detail & Related papers  (2026-05-09T19:27:38Z)
• IMPACT-CYCLE: A Contract-Based Multi-Agent System for Claim-Level Supervisory Correction of Long-Video Semantic Memory [73.22944697933603]
  Existing pipelines produce opaque, end-to-end outputs that expose no intermediate state for inspection.<n>We present IMPACT-Cycle, a supervisory multi-agent system that reformulates long-video understanding as a multimodal iterative claim-level maintenance.
  arXiv  Detail & Related papers  (2026-04-22T03:03:33Z)
• Scaling Human-AI Coding Collaboration Requires a Governable Consensus Layer [22.42181408084751]
  Vibe coding produces correct, executable code at speed, but leaves no record of the structural commitments, dependencies, or evidence behind it.<n>We propose Agentic Consensus: a paradigm in which the consensus layer C, an operable world model, replaces code as the primary artifact of engineering.<n>We propose benchmark task families designed to measure whether consensus-based reduce human intervention compared to chat-driven baselines.
  arXiv  Detail & Related papers  (2026-04-20T06:53:32Z)
• Compiling Activation Steering into Weights via Null-Space Constraints for Stealthy Backdoors [48.881343993730844]
  Safety-aligned large language models (LLMs) are increasingly deployed in real-world pipelines.<n> adversaries can distribute backdoored checkpoints that behave normally under standard evaluation but jailbreak when a hidden trigger is present.<n>Recent post-hoc weight-editing methods offer an efficient approach to injecting such backdoors.
  arXiv  Detail & Related papers  (2026-04-14T06:48:33Z)
• Attesting LLM Pipelines: Enforcing Verifiable Training and Release Claims [2.0403981727850233]
  Modern Large Language Model (LLM) systems are assembled from third-party artifacts such as pre-trained weights, fine-tuning adapters, datasets, dependency packages, and container images.<n>This speed comes with supply-chain risks, including compromised dependencies, malicious hub artifacts, unsafe dedefaultization, forged provenance, and backdoored models.<n>We propose an attestation-aware promotion gate: before an artifact is admitted into trusted environments, the gate verifies claim evidence, enforces safe loading and static scanning policies, and applies secure-by-serial deployment constraints.
  arXiv  Detail & Related papers  (2026-03-30T20:37:48Z)
• Understanding Contextual Recall in Transformers: How Finetuning Enables In-Context Reasoning over Pretraining Knowledge [50.009682083079205]
  We investigate whether contextual recall emerges from pretraining alone.<n>We show that finetuning on tasks requiring implicit inference, distinct from the ICL evaluation, triggers the emergence of contextual recall.<n>For mechanistic insight, we derive a construction for an attention-only transformer that replicates the transition from factual to contextual recall.
  arXiv  Detail & Related papers  (2026-03-21T22:46:55Z)
• 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)
• Turn: A Language for Agentic Computation [0.0]
  We present textbfTurn, a compiled, actor-based programming language.<n>Turn is for agentic software: programs that reason and act autonomously by delegating inference to large language models.
  arXiv  Detail & Related papers  (2026-03-07T09:10:09Z)
• Proof-Carrying Numbers (PCN): A Protocol for Trustworthy Numeric Answers from LLMs via Claim Verification [0.0]
  We propose textbfProof-Carrying Numbers (PCN), a presentation-layer protocol that enforces numeric fidelity through mechanical verification.<n>PCN is lightweight and model-agnostic, integrates seamlessly into existing applications, and can be extended with cryptographic commitments.
  arXiv  Detail & Related papers  (2025-09-08T17:20:16Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  Large language models (LLMs) are increasingly integrated into real-world personalized applications.<n>The valuable and often proprietary nature of the knowledge bases used in RAG introduces the risk of unauthorized usage by adversaries.<n>Existing methods that can be generalized as watermarking techniques to protect these knowledge bases typically involve poisoning or backdoor attacks.<n>We propose name for harmless' copyright protection of knowledge bases.
  arXiv  Detail & Related papers  (2025-02-10T09:15:56Z)
• Self-regulating Prompts: Foundational Model Adaptation without Forgetting [112.66832145320434]
  We introduce a self-regularization framework for prompting called PromptSRC. PromptSRC guides the prompts to optimize for both task-specific and task-agnostic general representations.
  arXiv  Detail & Related papers  (2023-07-13T17:59:35Z)

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.