When is LLM-Based Program Reasoning Correct? A Completion Semantics for LLM-Based Code Inference

Teaching Code LLMs to Reason with Intermediate Formal Specifications

Unlike natural-language specifications, executable formal specifications provide machine-checkable constraints for verifying, debugging, and repairing code. However, writing such specifications is labor-intensive, and existing LLM-based methods mainly infer whole-program pre/postconditions, missing the intermediate semantic commitments that programmers rely on when reasoning about an algorithm. Our study further shows that prompting current CodeLLMs often produces executable assertions that are syntactically invalid, trivial, or too weak to reject behavior-changing faults. In this paper, we study executable checkpoint specification generation, where assertions are inserted at meaningful internal program points to describe expected intermediate states. We introduce SpecCoder, a verification-guided CodeLLM training framework that learns from validated reference programs, behavior-changing mutants, and multi-turn specification-refinement traces. SpecCoder selects specifications that hold on correct executions while rejecting faulty executions, turning specifications from passive annotations into executable evidence. To evaluate this setting, we introduce HumanExec, a benchmark built from recent Codeforces competitive programming problems with test suites, reference solutions, and human buggy submissions, supporting three tasks: specification generation, program correctness checking, and program repair. Experiments on HumanExec show that SpecCoder substantially improves checkpoint-specification quality over base CodeLLMs. Across Qwen2.5-Coder models, SpecCoder improves inline-specification correctness by up to 55.8%, completeness by up to 358.1%, and executable assertion validity by up to 26.6%. These gains further translate to downstream correctness reasoning and repair, showing that executable checkpoints provide fine-grained evidence for reliable verification.

Euclid-MCP: A Model Context Protocol Server for Deterministic Logical Reasoning via Prolog

Large Language Models (LLMs) excel at natural language understanding and generation but remain unreliable for multi-step logical reasoning, especially in safety-critical or compliance-sensitive domains. Recent neuro-symbolic approaches address this gap by coupling neural models with external symbolic engines, yet most integrations are bespoke and lack a standardized interface for tool-augmented agents. This paper presents Euclid-MCP, an open-source MCP server that provides deterministic logical reasoning via SWI-Prolog. Euclid-MCP introduces Euclid-IR, an engine-agnostic intermediate representation for Horn-clause logic that is human-readable, easy for LLMs to generate, and straightforward to compile into Prolog or alternative backends. The server exposes a compact tool interface that supports a translate-run-inspect-repair loop, enabling LLM clients to delegate inference while retaining full access to proof traces and derivation logs. We evaluate Euclid-MCP on a realistic IT security and compliance use case. Results show that while LLMs alone are sufficient on small knowledge bases, they hallucinate systematically on larger problems, whereas Euclid-MCP delivers exact answers with lower latency and more compact outputs. We argue that semantic RAG is fundamentally unsuited for rule enforcement, and that Euclid-MCP can serve as a stable, shared reasoning substrate for both RAG-based assistants and agentic systems.

Mizzle: A Complete Concurrent Incorrectness Logic for Preventing False Alarms in Agentic Bug Finding

Large language models are increasingly used to find bugs in real-world programs, but they also produce a flood of false alarms that waste developers'time. We propose a method to prevent these false alarms by requiring an LLM to accompany each bug report with a machine-checked proof, in a program logic, that the reported bug is real. We follow the approach of incorrectness logics, whose under-approximate reasoning establishes that a claimed behavior is genuinely reachable, and hence a true positive. In our case, however, the logic must model a realistic programming language, have a mechanization so that proofs can be checked, and be complete, so that no real bug is ruled out for want of a derivation. We present Mizzle, an incorrectness separation logic for concurrent programs written in a substantial subset of OCaml, parametric in the notion of incorrectness. We mechanize Mizzle in the Rocq proof assistant on top of the Iris framework, and we prove that it is both sound (that is, it never justifies a false alarm) and complete (that is, every incorrect execution admits a derivation). We instantiate Mizzle with three notions of incorrectness: stuckness (triggering undefined behavior), the non-linearizability of a data structure, and the presence of a race. As a proof of concept, we illustrate how an LLM can use Mizzle in order to certify the existence of a bug.

SAT Modulo Well-Founded Semantics

AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language

AoA lifts the agent off source text and onto the abstract syntax tree (AST): the model supplies proofs as JSON representations of Minilang's AST and drives the prover through a tree-edit model that fuses proof operations and states into one proof tree, so each operation carries its own subgoal's state, readable directly off the tree.

BeSpec: Behavior-Level Specification Alignment for Code Generation

LLMs have made substantial progress on automated code generation from natural-language descriptions of desired behavior (intent). Most existing methods improve generated programs through execution-guided code refinement: they generate a candidate solution, execute it, and patch the implementation using feedback, while leaving the underlying specification unchanged. This workflow implicitly assumes that the LLM's understanding of the intent is already correct and complete. In practice, however, intents are often ambiguous or underspecified. As a result, even a capable model may produce a correct implementation of the wrong intent, making specification mismatch a central bottleneck. This paper presents BeSpec, a behavioral model-based approach to specification alignment. BeSpec treats the task description as partial evidence about the intended behavior of the correct program. It first builds an explicit behavioral model, which are checkable properties that valid outputs must satisfy. BeSpec then generates candidate programs, executes them on probe inputs, and compares their observed behavior with the predicted behaviors. When observed behavior does not match the predicted behaviors, BeSpec either refines the specification or rejects the candidate program. We evaluate BeSpec with three LLMs on four benchmarks: CodeContests, xCodeEval, APPS, and the contamination-free LiveCodeBench. Against nine baselines, BeSpec achieves the highest Pass@1 and average pass rate across all settings, improving average Pass@1 over the strongest baseline by 8.1%--25.3% relative across the three LLMs. A failure analysis shows that after alignment, most remaining errors stem from algorithmic difficulty rather than misunderstood specifications, while ablation studies confirm that each major component of BeSpec contributes positively.