Pramana: A Protocol-Layer Treatment of Claim Verification in Autonomous Agent Networks

• URL: http://arxiv.org/abs/2605.20312v1
• Date: Tue, 19 May 2026 17:00:33 GMT
• Title: Pramana: A Protocol-Layer Treatment of Claim Verification in Autonomous Agent Networks
• Abstract summary: Production verification today splits into two halves: Probabilistic verdict patterns (self-consistency voting, reviewer LLM ensembles) produce judgments, not artifacts.<n>Pramana defines the missing wire format. Every consequential agent output is wrapped in a typed ClaimAttestation with one of four variants.<n>Pramana exhaustively verified under TLC across three symmetry-reduced models: 38,563 distinct reachable states, zero invariant violations.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Autonomous agents deployed in regulated domains must produce a verification artifact per consequential output: a record an auditor can re-execute offline, capturing what was claimed, against what source, by whom, when, and how. Production verification today splits into two unstandardized halves. Probabilistic verdict patterns (self-consistency voting, reviewer LLM ensembles) produce judgments, not artifacts. Artifact-producing patterns (RAG, tool-augmented traces, generator-verifier loops) produce vendor-specific records no external auditor can reconstruct without bespoke integration. Pramana defines the missing wire format. Every consequential agent output is wrapped in a typed ClaimAttestation with one of four variants (measurement, inference, analogy, citation), each paired with a verify() operation against the recorded source. verify() is deterministic for MeasurementClaim and CitationClaim. For InferenceClaim and AnalogyClaim, determinism is conditional on the oracle (audit-replayable when LLM-backed). The four-way typology derives from classical Indian epistemology (pramana, valid means of knowledge). The lifecycle is specified in TLA+ and exhaustively verified under TLC across three symmetry-reduced models: 38,563 distinct reachable states, zero invariant violations. The Python reference implementation passes 84 tests. An A2A and MCP wire-extension manifest layers three deployment-grade invariants: reachability, SLA bound, and offline re-verifiability. An exploratory pilot (n=100, 2,275 reviewer calls) probes LLM-as-judge in code generation. The strongest observation is a 40-percentage-point raw FPR delta across corpora, consistent with reference-solution quality contributing significantly. The pilot does not validate Pramana on its own; the structural argument and formal verification do that.

Related papers

• AgentProv: Auditing Agentic LLM API Providers via Tool-use Policy Probes [38.37599802008238]
  Commercial LLM APIs advertise a specific foundation model, but the served backbone may be silently substituted, quantized, or wrapped.<n>All existing audits decide backbone identity from the text-output channel.<n>We introduce Agentic Provenance (AgentProv), the first action-based identity audit for agentic LLM APIs.
  arXiv  Detail & Related papers  (2026-08-30T08:22:12Z)
• Recognition Without Enforcement: Configuration-Dependent Failures in LLM Agent Instruction Arbitration and External Control [0.0]
  LLM agents arbitrate among instructions from system prompts, users, memory, and tools, but this arbitration cannot be assumed to enforce trust boundaries.<n>We identify a recognition-enforcement gap: source-format features are linearly decodable from model activations, and models can explicitly identify forged authority when prompted.<n>We treat model self-arbitration as a capability rather than a security boundary and implement an external reference monitor combining authenticated source routing with capability-gated tool execution.
  arXiv  Detail & Related papers  (2026-08-28T16:34:05Z)
• PluginEval: A Diagnostic Benchmark for Fine-Grained Error Attribution in Function Calling [11.1017602726296]
  Large Language Models increasingly operate as autonomous agents.<n>Current benchmarks face three structural limitations.<n>Eval is a benchmark constructed through a two-stage framework.
  arXiv  Detail & Related papers  (2026-08-09T13:25:54Z)
• Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering [40.048798975817924]
  Vibe coding is fast and may be adequate for low-criticality consumer software.<n>For safety-critical systems governed by DO-178C, IEC 61508, or ISO 26262, it offers no path to certification.<n>We present Forge, a closed-loop pipeline that guides vibe coding through formal verification.
  arXiv  Detail & Related papers  (2026-06-21T10:01:45Z)
• Domain-Validity-Gated Metamorphic Testing of Scientific ML Surrogates [6.691613382732758]
  We study how candidate metamorphic relations can be screened for domain validity and turned into executable test assets for SciML surrogates.<n>We propose a domain-validity that admits a candidate only when its tolerance dominates the operator's numerical floor and its preconditions hold.<n>The evidence spans two CFD tasks and a second PDE family, supporting a validity-aware bridge from candidate MRs to auditable SciML test assets.
  arXiv  Detail & Related papers  (2026-06-16T05:13:05Z)
• AuditWeave: A Tamper-Evident, Auditor-Navigable Evidence Layer for AI-Assisted and Data-Transformation Workflows [0.0]
  AuditWeave is a lightweight Python library that records the steps of AI-assisted and data-transformation into a single hash-chained ledger.<n>We describe the design and evaluate recording overhead, scalability, and tamper-detection correctness on the reference implementation.
  arXiv  Detail & Related papers  (2026-06-14T21:46:04Z)
• Deterministic Integrity Gates for LLM-Assisted Clinical Manuscript Preparation: An Auditable Biomedical Informatics Architecture [0.3823356975862005]
  We describe an architecture pairing generation with verification, resting on three principles.<n>This determinism-where-possible split, organized as an integrity-gate taxonomy, is the core contribution.<n> MedSci Skills is an open-source toolkit of 43 skills with a 21-detector deterministic tier, evaluated on three public-dataset pipelines.
  arXiv  Detail & Related papers  (2026-06-08T13:51:04Z)
• Agentic Model Checking [12.832868209928039]
  We propose a paradigm that couples LLM agents with a bounded model checking backend.<n>We instantiate the approach in BMC-Agent and evaluate it on LLM-generated kernel and compiler code in C and Rust.
  arXiv  Detail & Related papers  (2026-05-20T17:25:52Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• NANOZK: Layerwise Zero-Knowledge Proofs for Verifiable Large Language Model Inference [0.0]
  We present METHOD, a zero-knowledge proof system that makes LLM inference verifiable.<n>Our approach exploits the fact that transformer inference naturally decomposes into independent layer computations.<n>Compared to EZKL, METHOD achieves 70x smaller proofs and 5.7x faster proving time at d=128, while maintaining formal soundness guarantees.
  arXiv  Detail & Related papers  (2026-03-17T04:14:45Z)
• interwhen: A Generalizable Framework for Verifiable Reasoning with Test-time Monitors [47.363850513075356]
  We present a test-time verification framework, interwhen, that ensures that the output of a reasoning model is valid wrt. a given set of verifiers.<n> Verified reasoning is an important goal in high-stakes scenarios such as deploying agents in the physical world.
  arXiv  Detail & Related papers  (2026-02-05T08:35:01Z)
• DiFR: Inference Verification Despite Nondeterminism [5.879581944824945]
  Re-running the same inference process twice often leads to different results due to benign numerical noise.<n>We introduce Token-DiFR, a method for verifying inference outputs by comparing generated tokens against predictions made by a trusted reference implementation conditioned on the same random seed.<n>We additionally introduce Activation-DiFR, a scheme that uses random projections to compress activations into compact fingerprints for subsequent verification.
  arXiv  Detail & Related papers  (2025-11-25T18:44:22Z)
• Memory in Large Language Models: Mechanisms, Evaluation and Evolution [8.158439933515131]
  We propose a four-part taxonomy (parametric, contextual, external, procedural/episodic) and a memory quadruple (location, persistence, write/access path, controllability)<n>For updating and forgetting, we present DMM Gov: coordinating DAPT/TAPT, PEFT, model editing (ROME, MEND, MEMIT, SERAC), and RAG to form an auditable loop.<n>This yields a reproducible, comparable, and governable coordinate system for research and deployment.
  arXiv  Detail & Related papers  (2025-09-23T10:06:58Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  We develop CompassVerifier, an accurate and robust lightweight verifier model for evaluation and outcome reward.<n>It demonstrates multi-domain competency spanning math, knowledge, and diverse reasoning tasks, with the capability to process various answer types.<n>We introduce VerifierBench benchmark comprising model outputs collected from multiple data sources, augmented through manual analysis of metaerror patterns to enhance CompassVerifier.
  arXiv  Detail & Related papers  (2025-08-05T17:55:24Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  We present a holistic end-to-end solution for annotating the factuality of large language models (LLMs)-generated responses. We construct an open-domain document-level factuality benchmark in three-level granularity: claim, sentence and document. Preliminary experiments show that FacTool, FactScore and Perplexity are struggling to identify false claims.
  arXiv  Detail & Related papers  (2023-11-15T14:41:57Z)
• FactCHD: Benchmarking Fact-Conflicting Hallucination Detection [64.4610684475899]
  FactCHD is a benchmark designed for the detection of fact-conflicting hallucinations from LLMs. FactCHD features a diverse dataset that spans various factuality patterns, including vanilla, multi-hop, comparison, and set operation. We introduce Truth-Triangulator that synthesizes reflective considerations by tool-enhanced ChatGPT and LoRA-tuning based on Llama2.
  arXiv  Detail & Related papers  (2023-10-18T16:27:49Z)
• Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
  AuditAI bridges the gap between interpretable formal verification and scalability. We show how AuditAI allows us to obtain controlled variations for verification and certified training while addressing the limitations of verifying using only pixel-space perturbations.
  arXiv  Detail & Related papers  (2021-09-25T22:53:24Z)

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.