A Minimal Executable Proof for Multi-Language Contract Traceability

• URL: http://arxiv.org/abs/2605.28546v1
• Date: Wed, 27 May 2026 14:37:26 GMT
• Title: A Minimal Executable Proof for Multi-Language Contract Traceability
• Abstract summary: This paper reports a deliberately small executable proof for a DAG-TOML contract.<n>It shows how a contract, implementation graph, traceability chain, and review gate can be checked against executable witnesses.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper reports a deliberately small executable proof for a DAG-TOML contract: six "Hello, world!" implementations in Rust, Go, C, Java, TypeScript, and AWK are linked to one observable-output contract, one implementation DAG, one traceability file, one readiness gate, and one evidence matrix. The load-bearing contract requires the exact UTF-8 byte sequence `Hello, world!\n`, zero stderr bytes, and exit code 0. On the runner used for this paper, the witness harness reported five PASS outcomes, one SKIP for Java because `javac/java` was not on `PATH`, and zero FAIL outcomes. Two sidecar witnesses exercise narrower source-analysis claims: a convoluted Go rewrite hides the contiguous greeting literal but remains visible to sqry at the declared AST symbol and simple-edge level, while an indirect AWK rewrite uses a declared source profile because AWK is not in the repository's sqry-backed validator language set. The contribution is not a benchmark, a claim of general semantic equivalence, or a production assurance system. It is a compact, falsifiable artifact that shows how a contract, implementation graph, traceability chain, and review gate can be checked against executable witnesses.

Related papers

• Lie to Me: Finding Bugs in ZK DSL Toolchains with Adversarial Witness Injection [3.6756416620917522]
  We present Liezz, a testing framework that generates ZK DSL programs and exposes bugs through adversarial witness injection.<n>For each generated deterministic program, Liezz executes two public input assignments with different outputs and splices their witnesses, combining the input of one execution with the output of the other.<n> Controlled divergence and multiple witness-splicing strategies preserve enough consistency to expose missing constraints.
  arXiv  Detail & Related papers  (2026-08-31T11:50:37Z)
• 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)
• SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations [0.8557392136621891]
  SEMBridge generates weakest-precondition and bounded-checking interpretations from the same executable object programs.<n>The Python prototype implements a loop-free imperative core with assignments, conditionals, assumptions, and assertions.
  arXiv  Detail & Related papers  (2026-05-29T18:00:06Z)
• SCDBench: A Benchmark for LLM-Based Smart Contract Decompilers [55.39407031861402]
  We introduce SCDBench, a dataset and benchmark methodology for smart contract decompilation.<n>The dataset contains 600 real-world Solidity contracts with paired bytecode inputs, ground-truth source code, and replayable semantic checkpoints.<n>We evaluate Claude Opus 4.7, GPT-5.3-Codex, and GLM-5 in a zero-shot decompilation setting, including GLM-5 variants with and without extended reasoning.
  arXiv  Detail & Related papers  (2026-05-27T20:08:47Z)
• An Execution-Verified Multi-Language Benchmark for Code Semantic Reasoning [10.815335026032377]
  TraceEval is the first execution-verified, multi-language benchmark for code semantic reasoning.<n>TraceEval consists of 10,583 real-world programs extracted from 1,600+ open-source repositories across Python, JavaScript, and Java.<n>The strongest model, Claude-Opus-4.6, reaches an average F1 of 72.9% across the three languages.
  arXiv  Detail & Related papers  (2026-05-10T07:17:00Z)
• Proof of Execution: Runtime Verification for Governed AI Agent Actions [0.0]
  Agent systems increasingly execute rather than advise.<n>We formalize this as runtime proof of execution.<n>PoE binds authorization, effect, history, and replay into a single runtime-checkable object.
  arXiv  Detail & Related papers  (2026-04-26T12:30:54Z)
• 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)
• CLEVER: A Curated Benchmark for Formally Verified Code Generation [53.5486188696892]
  $rm Csmall LEVER$ is a high-quality, curated benchmark of 161 problems for end-to-end verified code generation in Lean.<n>Each problem consists of (1) the task of generating a specification that matches a held-out ground-truth specification, and (2) the task of generating a Lean implementation that provably satisfies this specification.
  arXiv  Detail & Related papers  (2025-05-20T05:15:47Z)
• Verified invertible lexer using regular expressions and DFAs [0.0]
  In this project, we explore the concept of invertibility applied to serialisation and lexing frameworks.<n>While serialisation is the process of taking a data structure and writing it to a bit array, lexing is the process of reading a stream of characters and splitting them into tokens.
  arXiv  Detail & Related papers  (2024-12-18T08:03:17Z)
• Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study [0.0]
  ASN.1 is a language for describing data structures widely employed in ground and space telecommunications.<n>ACN can be used along ASN.1 to describe complex binary formats and legacy protocols.<n>We show how to port an ASN.1/ACN code generator to generate Scala code.<n>We then enhance the generator to emit not only the executable code but also strong enough pre-conditions, post-conditions, and lemmas for inductive proofs.
  arXiv  Detail & Related papers  (2024-12-10T06:54:42Z)
• Defending Large Language Models against Jailbreak Attacks via Semantic Smoothing [107.97160023681184]
  Aligned large language models (LLMs) are vulnerable to jailbreaking attacks. We propose SEMANTICSMOOTH, a smoothing-based defense that aggregates predictions of semantically transformed copies of a given input prompt.
  arXiv  Detail & Related papers  (2024-02-25T20:36:03Z)
• Precise Zero-Shot Dense Retrieval without Relevance Labels [60.457378374671656]
  Hypothetical Document Embeddings(HyDE) is a zero-shot dense retrieval system. We show that HyDE significantly outperforms the state-of-the-art unsupervised dense retriever Contriever.
  arXiv  Detail & Related papers  (2022-12-20T18:09:52Z)

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.