Neuroforger: certified violation witnesses for smart contracts verification via LLMs

• URL: http://arxiv.org/abs/2605.31389v1
• Date: Fri, 29 May 2026 14:54:51 GMT
• Title: Neuroforger: certified violation witnesses for smart contracts verification via LLMs
• Abstract summary: Recent large language models (LLMs) incorporate reasoning capabilities that allow them to perform well in predicting whether a smart contract respects a certain property.<n>We introduce a new formal specification language that extends Solidity with abstract types.<n>We design a workflow that combines LLMs with type checking and concrete execution to generate and validate violation witnesses.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Recent large language models (LLMs) incorporate reasoning capabilities that allow them to perform well in predicting whether a smart contract respects a certain property, suggesting a complementary approach to traditional formal-methods-based techniques for smart contract verification. However, the application of LLMs in such context has two major issues: 1) properties expressed in natural language are intrinsically ambiguous, and 2) answers returned by LLMs have no guarantee of correctness. In this paper, we address both issues simultaneously by: 1) introducing a new formal specification language that extends Solidity with abstract types, and 2) designing a workflow that combines LLMs with type checking and concrete execution to generate and validate violation witnesses (i.e., counterexamples). The key idea is to represent a specification as a Solidity test with (existentially quantified) variables of abstract type; finding an instantiation of these variables to concrete values (of the correct type) concretizes the test into an executable counterexample (PoC) for the target property. We implemented our procedure in the tool Neuroforger, experimentally evaluating it on a smart-contract verification dataset drawn from literature, obtaining promising results that demonstrate its potential applicability in the wild.

Related papers

• Faithful Autoformalization of Natural Language Assertions [2.8921494813790094]
  We present Monty: an autoformalization framework for assertions.<n>Our techniques are based on filtering formalizations using a novel conformance score metric.<n>We show that our technique produces the ground truth more reliably than when using LLMs naively to translate assertions.
  arXiv  Detail & Related papers  (2026-07-14T22:12:14Z)
• ClarifyCodeBench: Evaluating LLMs on Clarifying Ambiguous Requirements for Code Generation [54.788849448970154]
  We introduce ClarifyCodeBench, a novel interactive benchmark for evaluating Large Language Models' capability in resolving requirement ambiguity.<n>We conduct a systematic evaluation of six state-of-the-art LLMs using ClarifyCodeBench.<n>Our empirical results yield three critical insights: 1) Capability Decoupling: Strong code generation performance does not inherently translate to effective requirement clarification; 2) The Reasoning Paradox: While increased computational thinking enhances code correctness, it yields marginal gains in identifying ambiguities.
  arXiv  Detail & Related papers  (2026-07-01T09:58:59Z)
• 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)
• LLM-Based Static Verification of Code Against Natural-Language Requirements: An Industrial Experience Report [3.5867640049033054]
  This article presents a two-stage LLM-based workflow for addressing this challenge in an intelligent-vehicle cybersecurity case study.<n>In the first stage, an AI-based rule miner extracts verifiable rules from natural-language requirements.<n>In the second stage, an AI-based code auditor checks implementation evidence against the extracted rules.
  arXiv  Detail & Related papers  (2026-05-18T06:34:03Z)
• A2RBench: An Automatic Paradigm for Formally Verifiable Abstract Reasoning Benchmark Generation [59.98516959731531]
  Abstract reasoning ability reflects intelligence and capacity of LLMs to extract and apply abstract rules.<n>Existing benchmarks either rely on expensive manual annotation, limiting their scale, or risk measuring memorization rather than genuine reasoning.<n>We introduce an automated pipeline named A2RBench, encompassing generation, expansion, evaluation, and analysis.
  arXiv  Detail & Related papers  (2026-05-17T06:14:20Z)
• Small Language Model Helps Resolve Semantic Ambiguity of LLM Prompt [13.863963355859175]
  We propose a pre-inference prompt optimization mechanism via explicit prompt disambiguation.<n>We identify semantic risks in the prompt, check their multi-perspective consistency, and resolve any semantic conflicts.<n>Our method improves reasoning performance by 2.5 points at a cost of only $0.02.
  arXiv  Detail & Related papers  (2026-04-25T12:13:26Z)
• Improving Dynamic Specification Inference with LLM-Generated Counterexamples [3.555888578860533]
  This paper explores the use of large language models (LLMs) to automatically generate tests that attempt to invalidate generated assertions.<n>Our results show that state-of-the-art LLMs can generate effective counterexamples that help to discard up to 11.68% of invalid assertions inferred by SpecFuzzer.
  arXiv  Detail & Related papers  (2026-04-12T18:09:53Z)
• Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification? [1.9551668880584971]
  Large Language Models (LLMs) have shown promise in inferring formal postconditions from natural language hints.<n>We introduce NL2Contract, the task of employing LLMs to translate informal natural language into formal functional contracts.<n>We evaluate NL2Contract with different LLMs and compare it to the task of postcondition generation nl2postcond.
  arXiv  Detail & Related papers  (2025-10-14T16:37:39Z)
• Aligning Large Language Models for Faithful Integrity Against Opposing Argument [71.33552795870544]
  Large Language Models (LLMs) have demonstrated impressive capabilities in complex reasoning tasks.<n>They can be easily misled by unfaithful arguments during conversations, even when their original statements are correct.<n>We propose a novel framework, named Alignment for Faithful Integrity with Confidence Estimation.
  arXiv  Detail & Related papers  (2025-01-02T16:38:21Z)
• Aligning Language Models to Explicitly Handle Ambiguity [22.078095273053506]
  We propose Alignment with Perceived Ambiguity (APA), a novel pipeline that aligns language models to deal with ambiguous queries. Experimental results on question-answering datasets demonstrate that APA empowers LLMs to explicitly detect and manage ambiguous queries. Our finding proves that APA excels beyond training with gold-standard labels, especially in out-of-distribution scenarios.
  arXiv  Detail & Related papers  (2024-04-18T07:59:53Z)
• Uncertainty Quantification for In-Context Learning of Large Language Models [52.891205009620364]
  In-context learning has emerged as a groundbreaking ability of Large Language Models (LLMs) We propose a novel formulation and corresponding estimation method to quantify both types of uncertainties. The proposed method offers an unsupervised way to understand the prediction of in-context learning in a plug-and-play fashion.
  arXiv  Detail & Related papers  (2024-02-15T18:46:24Z)
• Which Syntactic Capabilities Are Statistically Learned by Masked Language Models for Code? [51.29970742152668]
  We highlight relying on accuracy-based measurements may lead to an overestimation of models' capabilities. To address these issues, we introduce a technique called SyntaxEval in Syntactic Capabilities.
  arXiv  Detail & Related papers  (2024-01-03T02:44:02Z)
• ReEval: Automatic Hallucination Evaluation for Retrieval-Augmented Large Language Models via Transferable Adversarial Attacks [91.55895047448249]
  This paper presents ReEval, an LLM-based framework using prompt chaining to perturb the original evidence for generating new test cases. We implement ReEval using ChatGPT and evaluate the resulting variants of two popular open-domain QA datasets. Our generated data is human-readable and useful to trigger hallucination in large language models.
  arXiv  Detail & Related papers  (2023-10-19T06:37:32Z)

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.