Show Me The Money: An Exercise in Proof-Driven Software Understanding

• URL: http://arxiv.org/abs/2607.16499v1
• Date: Fri, 17 Jul 2026 20:39:40 GMT
• Title: Show Me The Money: An Exercise in Proof-Driven Software Understanding
• Abstract summary: We focus on a formal analysis of the core algorithm that implements the Stellar blockchain's SDEX order book.<n>We produce artifacts that make it easy for code changes to be checked against established invariants.<n>This work demonstrates how the strategic combination of theorem proving and model checking provides a path for delivering robust assurance to legacy systems.
• Score: 1.678913049066618
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: We present a case study on proof-driven software understanding of mature, security-critical infrastructure. While formal methods are traditionally applied during the design phase, we present our experience applying formal reasoning onto a mature industrial C++ codebase. We focus on a formal analysis of the core algorithm that implements the Stellar blockchain's SDEX order book. By combining large language models (LLMs), Prototype Verification System (PVS), and SeaHorn, we are able to prove core properties of the production codebase. Our approach also identified an inconsistency in documentation related to the reachability of an exception location. Most importantly, however, we produce artifacts that make it easy for code changes to be checked against established invariants. This work demonstrates how the strategic combination of theorem proving and model checking provides a path for delivering robust assurance to legacy systems.

Related papers

• Learning to Reason with Insight for Informal Theorem Proving [50.054221663394195]
  In this work, we identify a primary bottleneck in informal theorem proving as a lack of insight.<n>We propose a novel framework designed to cultivate this essential reasoning skill and enable LLMs to perform insightful reasoning.<n>Our experiments on challenging mathematical benchmarks demonstrate that this insight-aware generation strategy significantly outperforms baselines.
  arXiv  Detail & Related papers  (2026-04-17T17:36:21Z)
• Reasoning Core: A Scalable Procedural Data Generation Suite for Symbolic Pre-training and Post-Training [2.62112541805429]
  Reasoning Core is a scalable suite that procedurally generates verifiable symbolic reasoning data across core formal domains.<n>Each task is paired with an external solver for rigorous verification and admits continuous difficulty control for curriculum design.<n>Experiments show that mixing Reasoning Core data into pre-training improves downstream reasoning while preserving, or slightly improving, language modeling quality.
  arXiv  Detail & Related papers  (2026-03-02T18:59:29Z)
• 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)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• Constant-Size Cryptographic Evidence Structures for Regulated AI Workflows [0.0]
  This paper introduces constant-size cryptographic evidence structures for audit evidence for AI in regulated environments.<n>Each evidence item is a fixed-size of cryptographic fields, designed to (i) provide strong binding to workflow events and configurations, (ii) support constant-size storage and uniform verification cost per event, and (iii) compose cleanly with hash-chain and Merkle-based audits.
  arXiv  Detail & Related papers  (2025-11-21T10:28:07Z)
• Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
  We show that the decoding mechanism of dLLMs can be used as a powerful tool for model attribution.<n>We propose a novel information extraction scheme called the Directed Decoding Map (DDM), which captures structural relationships between decoding steps and better reveals model-specific behaviors.
  arXiv  Detail & Related papers  (2025-10-02T06:25:10Z)
• Typed Chain-of-Thought: A Curry-Howard Framework for Verifying LLM Reasoning [0.0]
  Chain-of-Thought (CoT) prompting enhances the reasoning capabilities of large language models.<n>We propose a novel theoretical lens for this problem grounded in the Curry-Howard correspondence.<n>We operationalise this analogy, presenting methods to extract and map the informal, natural language steps of CoT into a formal, typed proof structure.
  arXiv  Detail & Related papers  (2025-10-01T16:06:40Z)
• What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus [2.8003002159083237]
  We conduct a user study involving the collection and analysis of fine-grained source code telemetry from eight experts working with two languages.<n>Results reveal interesting trends and patterns about how experts reason about proofs and key challenges encountered during the proof development process.<n>We translate these findings into concrete design guidance for AI proof assistants.
  arXiv  Detail & Related papers  (2025-08-01T22:16:30Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes are neither reliable nor scalable.<n>A promising yet largely uncharted alternative is formal language-based reasoning.<n>Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes.
  arXiv  Detail & Related papers  (2025-07-22T08:13:01Z)
• Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification [0.26763498831034044]
  We introduce a framework that generates whole proofs in a formal language to be used within systems that utilize the power of built-in tactics and off-the-shelf automated theorem provers.<n>To train the LLM, we employ a 2-stage finetuning process, where we first use SFT-based training to enable the model to generate syntactically correct Isabelle code.<n>We validate our framework using the miniF2F-test benchmark and the Isabelle proof assistant and design a use case to verify the correctness of the S3 bucket access policy code.
  arXiv  Detail & Related papers  (2025-04-23T18:04:38Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof.<n>Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)

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.