Can Code Specify a System Precisely Enough to Formally Verify It?

• URL: http://arxiv.org/abs/2607.05076v1
• Date: Mon, 06 Jul 2026 13:39:00 GMT
• Title: Can Code Specify a System Precisely Enough to Formally Verify It?
• Abstract summary: This paper evaluates both on production software: the payment workflow of an operational restaurant point-of-sale system.<n>The core protocol is correct relative to a hand-built, line-cited model under a precisely stated failure model.<n>A single probe of the production payment sandbox exposed a response-shape divergence that makes an entire recovery ladder unreachable.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification is seldom applied to production software, because writing and maintaining a model has historically cost more than it returns. A companion study [1] extended SysMoBench [4] with a lower-cost alternative: specifications are graded against traces captured from the running system. It found that when large language models write the specifications, reliability is governed by the structure of the specification contract, not the language. This paper evaluates both on production software: the payment workflow of an operational restaurant point-of-sale system, which must keep the register, payment terminal, and payment processor in agreement. We report three results. First, the core protocol is correct relative to a hand-built, line-cited model under a precisely stated failure model. The audit found seven failure-handling gaps, nearly all with a common root cause; three were reproduced as real executions, and a patch closing them was re-checked with all failure gates enabled, after which a follow-up patch closed a defect the re-check itself exposed. Systematic extensions of the failure model (crash-restart, stale reads, two attempts) each found the windows they were designed to probe. Second, a single probe of the production payment sandbox exposed a response-shape divergence that makes an entire recovery ladder unreachable against the live API. The emulator-based audit could not detect it, because code and emulator share the same misreading: a correlated-oracle failure. Third, the companion study's central finding replicates across seven models from two vendors: contract structure, not language, governs what LLMs specify reliably. The replication concerns the ordering of contracts and the failure taxonomy, not the absolute level: only the strongest models reached the corpus ceiling, and the harder task restores discriminating power the benchmark had lost.

Related papers

• Rebuild Dossier: Mechanically-Enforced Specs for Agentic App Rebuilds, and What Model-Tier Failures Reveal [0.0]
  rebuild-dossier is an open-source tool that locks an application's real interface before any code is written.<n>It enforces one-test-at-a-time building through automated checks, not written instructions alone.
  arXiv  Detail & Related papers  (2026-08-22T01:26:56Z)
• From Subjective Judgments to Auditable Standards:Protocol-Guided AI Auditing of Website Redundancy [2.2917707112773593]
  Website redundancy does not have a single fixed meaning.<n>We introduce CORA, which measures repetition load, normal-use tax, and failure-domain recovery reserve separately.
  arXiv  Detail & Related papers  (2026-08-21T07:17:35Z)
• The Working Set of a Coding Agent: Coherence Debt in Repository-Scale Tasks [14.070053515623883]
  Repository-scale coding requires an agent to keep tests, imports, configuration, and migration rules consistent within a bounded context window.<n>We supply and withhold each channel and inject faults across seven models and five harnesses.<n>When a rename defeats what models memorized about a real library, all seven fail in the same place, passing and missing the same tests.
  arXiv  Detail & Related papers  (2026-08-17T14:30:41Z)
• Fantastic Adaptive Taxonomies and How to Use Them [100.20614173157708]
  AdaMAST converts execution traces into a compact, evidence-grounded failure taxonomy.<n>No code is hand-authored, no trace human-annotated.<n>In agent-system search, taxonomy-coded diagnoses of failed candidates outperform free-form.
  arXiv  Detail & Related papers  (2026-07-17T17:41:16Z)
• From Prompts to Contracts: Harness Engineering for Auditable Enterprise LLM Agents [0.24554686192257424]
  Productization adds requirements for source boundaries, entity routing, answer contracts, and reproducible traces.<n>We present a harness-engineering approach that reconstructs this pattern into a traceable, auditable LLM-agent architecture.<n>We instantiate it on a public-data slice of five Korean corporate groups and evaluate three research questions.
  arXiv  Detail & Related papers  (2026-07-09T01:08:33Z)
• PairCoder++: Pair Programming as a Universal Paradigm for Verified Code-Driven Multimodal and Structured-Artifact Generation [51.92442051257354]
  PairCoder improves essentially every benchmark whose artifact is verifiable, on full official metric suites rather than execution alone.<n>TikZ compile rate up 10 to 30 points on every model, at 2.9 to 9.2 times single model cost.
  arXiv  Detail & Related papers  (2026-07-02T08:36:02Z)
• Maestro Order: A Model-Agnostic Orchestration Harness [0.5414847001704247]
  We present a model-agnostic orchestration harness that turns unreliable solvers into reliable problem-solving systems.<n>We give the architecture, the message and state schema, the controller algorithm, and the engineering that makes it deterministic, observable, and fault-tolerant.<n>We report results from a faithful Monte Carlo simulation of the harness over a parameterized solver/verifier model.
  arXiv  Detail & Related papers  (2026-06-22T22:21:59Z)
• A Topology-Aware, Memory-Centric Architecture that Separates Root-Cause Derivation from Root-Cause Explanation [0.0]
  We argue that the missing ingredient in autonomous operations is not a better anomaly detector or a larger language model, but operational memory.<n>We present O PS C ORTEX, a working multi-agent prototype that organizes this memory into four tiers and uses it to separate two tasks the field usually conflates: deriving a root cause and explaining it.
  arXiv  Detail & Related papers  (2026-06-18T09:20:20Z)
• A Universal Cliff and a Design Fingerprint: Cross-Section Defect Detection Under LLM Orchestration [0.0]
  Production language-model systems answer a request byspanning it across an invisible orchestration of worker agents.<n>We ask what this does to a class of defect no single worker can see.<n>We vary only the model -- ten systems across five generations from one developer and five providers from distinct alignment paradigms.
  arXiv  Detail & Related papers  (2026-05-25T05:09:48Z)
• Pramana: A Protocol-Layer Treatment of Claim Verification in Autonomous Agent Networks [0.0]
  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.
  arXiv  Detail & Related papers  (2026-05-19T17:00:33Z)
• Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols [1.5229705287183657]
  SPECA is an audit framework that derives explicit, categorized security properties from natural-language specifications and reuses them across implementations.<n>On the RepoAudit benchmark, SPECA reaches 88.9% precision at 100% recall (F1=0.94) and surfaces 12 author-validated bugs beyond ground truth.<n>On the Sherlock Fusaka Audit Contest (10 targets, 366 submissions), SPECA recovers all 15 vulnerabilities expert-augmented and surfaces 4 fix-confirmed bugs.
  arXiv  Detail & Related papers  (2026-04-29T09:57:07Z)
• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  Existing benchmarks test only individual languages/tools, so the performance numbers are not directly comparable.<n>We address this gap with AlgoVeri, a benchmark that evaluates vericoding of $77$ classical algorithms in Dafny, Verus, and Lean.
  arXiv  Detail & Related papers  (2026-02-10T06:58:26Z)
• Where LLM Agents Fail and How They can Learn From Failures [62.196870049524364]
  Large Language Model (LLM) agents have shown promise in solving complex, multi-step tasks.<n>They amplify vulnerability to cascading failures, where a single root-cause error propagates through subsequent decisions.<n>Current systems lack a framework that can comprehensively understand agent error in a modular and systemic way.<n>We introduce the AgentErrorTaxonomy, a modular classification of failure modes spanning memory, reflection, planning, action, and system-level operations.
  arXiv  Detail & Related papers  (2025-09-29T18:20:27Z)
• Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs [71.7892165868749]
  Commercial Large Language Model (LLM) APIs create a fundamental trust problem.<n>Users pay for specific models but have no guarantee that providers deliver them faithfully.<n>We formalize this model substitution problem and evaluate detection methods under realistic adversarial conditions.<n>We propose and evaluate the use of Trusted Execution Environments (TEEs) as one practical and robust solution.
  arXiv  Detail & Related papers  (2025-04-07T03:57:41Z)
• Do Large Language Model Benchmarks Test Reliability? [66.1783478365998]
  We investigate how well current benchmarks quantify model reliability.<n>Motivated by this gap in the evaluation of reliability, we propose the concept of so-called platinum benchmarks.<n>We evaluate a wide range of models on these platinum benchmarks and find that, indeed, frontier LLMs still exhibit failures on simple tasks.
  arXiv  Detail & Related papers  (2025-02-05T18:58:19Z)

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.