AI 速览：提出一个基于 SMT 的可扩展 Lean 证明自动化框架 crush，用去函数化桥接高阶构造与一阶求解器，并支持可扩展的翻译与证明重建。
Lean's rich expressiveness supports higher-order functions, inductive datatypes, and user-defined abstractions, making it challenging to translate proof obligations into first-order Satisfiability Modulo Theory (SMT) queries and reconstruct kernel checked proofs. We present crush, an extensible SMT-backed proof automation framework for Lean. To bridge the gap between Lean's higher-order constructs and the solver's first-order logic, crush uses defunctionalization to encode function values and their applications. We formalize this translation for a supported higher-order fragment and prove its soundness. Moreover, crush provides metaprogramming interfaces for extending both Lean-to-SMT translation and the reconstruction of Lean proofs from solver certificates without modifying the translation pipeline. We implement crush as both a tactic and a backend for other third-party automation systems. We show that across four such use cases that target verification and general proof automation, crush discharges more obligations than the competing backends and reconstructs more kernel-checked proofs than the baselines.
Sebastian Körner, Oliver Emil Bøving, Christoph Matheja
Weighted programming is a framework by Batz et al. for describing mathematical models or optimization problems as imperative programs parametrized over semirings and then analyzing them with program verification techniques like weakest precondition calculi. Applications include reasoning about expected outcomes of probabilistic programs and competitive analysis of online algorithms. We extend weighted programming with (1) countable nondeterminism and (2) user-defined additive rewards, where programs are parametrized over modules instead of semirings. The resulting framework enables reasoning about expected resource consumption of probabilistic programs and about optimal scores of combinatorial games. A technical challenge is that wp-calculi for weighted programs with (1) and (2) over arbitrary modules can be unsound, because it is well-known that continuity properties commonly used in program semantics break in the presence of countable nondeterminism. We study conditions under which a wp-style transformer for reasoning about weighted programs is sound with respect to an operational ground truth defined in terms of weighted decision processes (WDPs) - transition systems that generalize Markov decision processes by drawing transition weights and state rewards from a module. Based on those conditions, we show that a range of concrete instances of the weighted programming framework enjoy sound weakest precondition reasoning. We demonstrate the usefulness of our wp-semantics through case studies for different modules. We mechanized our extended weighted programming framework and our main soundness results in the interactive theorem prover Lean. Instantiating these results for probabilistic programming yields, to the best of our knowledge, the first mechanized proof of a fixed point characterization of minimal expected rewards in Markov decision processes with countable nondeterminism.
We present, to the best of our knowledge, the first fully automated verification framework for QSP-based Hamiltonian simulation. Our framework exploits the structure of the simulation algorithm: Hamiltonians are given as weighted sums of Pauli strings, embedded into larger unitaries through block encodings, and transformed into time-evolution operators by quantum signal processing (QSP). Using a symbolic Pauli-sum semantics for ancilla-indexed circuit blocks, our verifier proves that the distinguished all-zero ancilla block is proportional to the target Hamiltonian and infers the subnormalization factor automatically. It then verifies the QSP layer by extracting the implemented polynomial transformation and certifying its approximation error. This structure-aware abstraction is essential for scalability. Composing our verified block encoding and QSP wrapper yields an estimated macro-expanded size of about 1.52 million gates. The verifier certifies the block encoding once and checks the QSP layer through its abstract interface, without expanding the oracle calls. Our implementation verifies block encodings of structured Pauli-sum Hamiltonians with up to 256 system qubits and verifies QSP Hamiltonian-simulation instances by extracting their implemented polynomials and checking the resulting approximation bounds. These results show that fully automated verification can handle common Hamiltonian-simulation circuits at substantial scale when it exploits their algorithmic structure.
Although decades of research have yielded sophisticated mechanisms for enforcing memory safety, speculative execution can subvert these protections through transient memory operations. Conversely, defenses designed specifically for speculative safety, such as Speculative Load Hardening (SLH), cannot enforce memory safety during non-speculative execution. A naive combination of defenses from both domains raises two fundamental challenges: (1) which combination of otherwise fragmented defenses can ensure dual memory safety under speculative and non-speculative executions? (2) whether such combinations introduce redundant protections that incur unnecessary performance overhead? We present DualGuard, a unified framework for dual memory protection under non-speculative and speculative executions. DualGuard systematically analyzes memory behaviors, classifying them into four categories, and further identifies the minimal composition requirements for dual memory safety, which allow us to strategically combine existing mitigations and design new ones to avoid redundant or excessive protections. We implement DualGuard through a combination of static analysis and runtime enforcement within the LLVM infrastructure. Our evaluation demonstrates that DualGuard reduces overhead by 3%-72% compared to naive compositions of fragmented defenses. In some cases, it even incurs lower overhead than approaches that guarantee memory safety solely under either non-speculative or speculative execution.
Low-precision GPU kernels are commonly tested against a reference using hand-picked absolute and relative tolerances. Legitimate numerical error varies with the input, format and precision plan, so a fixed tolerance trades false alarms for missed faults. We present numoracle, which derives per-element acceptance regions from precision-annotated reference programs. Its calculus tracks shared rounding errors, provenance-ordered products, block-scaled quantizers and calibrated math-library errors. A rounding-interval check detects faulty stores that symmetric bounds can admit. Soundness is conditional on explicit rounding, hardware, domain and implementation assumptions; a fixed-input mode removes the zero-mean rounding assumption. We evaluate 13 Triton operators from Liger-Kernel, Unsloth and vLLM on two GPU generations. The main campaigns produce no false alarm on 33,960 correct-kernel and behavior-preserving-variant runs per GPU. Under input shift, the GPU campaigns record no false alarm while tuned tolerances flag up to 30% of correct runs; final-version reference checks identify inputs without complete finite-range certificates. On the RTX PRO 6000, numoracle kills 116 of 124 effective mutants, versus 59-83 for four fixed baselines. Among 400 tuned tolerance configurations, requiring at most 1% false alarms in every evaluated Liger input group permits at most 31 of 53 main-mutant kills, versus numoracle's 50. Historical replays expose accuracy faults in eight change pairs without rejecting their matched corrected controls; a ninth change concerns rounding parity.
Elizabeth Gilbert, Chris Fallin, Heather Miller, Ben L. Titzer
Monitoring and debugging deployed software is crucial for scalability, performance, and robustness. Cross-cutting concerns are pervasive across software ecosystems, yet engineers must address them with a fragmented toolbox. While high-level frameworks exist to offer application-level types and semantics, they often lock a solution into specific languages, runtimes, or hardware architectures. Portability often forces engineers to choose lower-level instrumentation mechanisms. For example, in-language frameworks can trace a request across processes, but multi-language contexts require instrumentation at the boundary, for example using eBPF. While these frameworks provide powerful capabilities, they often result in 1) a tradeoff between application-level types or low-level bytes and packets, 2) non-composable domain-specific tools, 3) feature fragmentation across frameworks, and 4) tools that often run with unrestricted access to the program and its environment. We address these problems with Splicer, a WebAssembly component interposition framework that 1) provides semantically rich application-level types, 2) enables pluggable tooling with powerful capabilities, 3) reduces ecosystem fragmentation through porting across languages and hardware, and 4) confines each tool to a sandbox with explicitly granted permissions. We evaluate Splicer on a suite of benchmarks demonstrating the pluggability of non-trivial tooling written in multiple source languages and their performance.
Frontier large language models write correct CUDA kernels for most single-operator benchmark tasks, yet their accuracy collapses on accelerators whose architecture and programming language they have rarely seen. We present a case study of an LLM agent loop built for such accelerators. Our example is the FuriosaAI RNGD NPU, programmed in a recent, sparsely documented Rust DSL, where the loop optimized three Gemma-4-12B decode kernels over 12 days on a shared, scarce device. The loop builds its own target knowledge: it writes and checks a summary of the DSL documentation, measures the chip with microbenchmarks, records compiler-derived legality rules, and revisits this knowledge when the toolchain changes, rechecking rules and measurements where it can. A role-based search over per-kernel Design Trees explores whole-kernel designs and accumulates small accepted changes in the best version of each kernel. Because device time is scarce and readings are noisy, cheap checks screen new designs before any device run, and late in the run a change was accepted only after repeated comparisons with the best kernel on the device. The final kernels reach a 9.293x geomean speedup over the official baseline, each within 1.25x of the cycles needed just to move its weights. Our prompts, profiler and acceptance test are available at https://github.com/bgchun-fs/multi-agent-kernel-gen-loop.
Carmine Abate, Kleio Liotati, František Farka, Sebastian Ertel
Program specifications in separation logic describe ownership of resources and serve as logical interfaces for local reasoning. Compiler correctness, expressed as semantics preservation, does not by itself supply such an interface for compiled code, because it does not explicitly relate source and target resources and assertions. We investigate WP-preserving compilation: when a compiler translates a source program, the weakest preconditions that the program satisfies in a separation logic carry over to the compiled program. Our proof technique consists of a resource-aware simulation over interaction trees: it relates the resources required by corresponding source and target events, and tracks ownership through target operations, such as register accesses, that have no source counterpart. We apply the approach to a compiler from a structured imperative language to an assembly-like language, first for closed programs and then extended with modules and function calls. In the extended setting, each module can be verified in the source logic and compiled separately; its specifications carry over to the compiled module and are preserved when compiled modules are linked. All results are mechanized in Rocq.
Marco Campion, Isabella Mastroeni, Michele Pasqua, Caterina Urban
We introduce Abstract Lipschitz Continuity (ALC), an extensional property of functions, in particular of program semantics, requiring that bounded differences between properties of two inputs yield proportionally bounded differences between properties of the corresponding outputs. ALC explicitly discerns between two complementary forms of approximation: property-based (or qualitative) approximations, which retain a property of the data and are formalized by upper closure operators as in abstract interpretation, and quantitative approximations, which measure the closeness of data and are formalized by pre-metrics, a weakening of metrics that covers the distances arising in program analysis. Keeping the two forms of approximation explicit has two main benefits. First, it allows us to precisely relate ALC to established extensional properties: ALC is a sufficient condition for partial completeness in abstract interpretation, for partial abstract non-interference in language-based security and, with a null Lipschitz constant, for abstract robustness in machine learning. Second, it supports reasoning about ALC of program semantics by induction on the syntax of programs: we present a sound deductive system, parametric in the property-based approximations and in the pre-metric of interest, that reduces a proof of ALC for a program to proofs for its basic commands and to some explicit side conditions, which isolate what makes ALC compositional across sequential composition, non-deterministic choice and iteration.
Jinhao Tan, Jam Kabeer Ali Khan, Bruno C. d. S. Oliveira
First-class environments expose runtime environments as ordinary values and support a substitution-free, environment-based operational semantics. They also support applications such as first-class modules, dynamic composition of environment fragments, and sandboxing via local environments. Existing environment-based calculi, however, are mostly studied in a simply typed setting and stop short of System F and polymorphism. We present $F_E$, a polymorphic calculus with first-class environments that conservatively extends System F with a small-step environment semantics. $F_E$ eliminates all forms of substitution in System F. Term and type abstractions evaluate to closures, boxes run code under local environments, and box types expose the local typing assumptions of both. Manifest types, together with a two-sided type equivalence, play a dual role: they model type-level instantiation, and enable transparent type components in environments and modules. We prove type soundness, normalization, decidability, and standard properties of type equivalence, and conservativity over System F. The metatheory of $F_E$ is based on instantiation lemmas rather than substitution lemmas. This foundation supports polymorphic first-class modules with dynamic composition and sandboxing. We study $F_E$ in two forms. Our main presentation is an explicit, type-passing calculus that follows conventional System F. We also develop an implicitly-typed variant aligned with the semantics of polymorphic functional languages. All metatheory is mechanized in the Rocq theorem prover.
E. G Plante, Eric Paul, Cosmo Viola, G. A. Kavvos, Talia Ringer
Maintaining formal proofs in response to breaking changes in their dependencies is a major challenge of proof engineering. Proof repair is a kind of proof automation that lessens the burden of this challenge by automatically adapting proofs in response to those changes. While proof repair is well understood through an algorithmic lens, it has, until now, been poorly understood through a theoretical lens. We address this gap by giving the first foundational treatment of proof repair, focusing in particular on type-theoretic proof repair in response to changes in datatypes. Our key insight is that the core component of a proof repair algorithm---a ``configuration''---is exactly an algebra isomorphism. We formalize and prove this insight, answering open questions from prior work. We then take this one step further and show that, by taking the dual of this representation, we obtain proof repair over coinductive types. All of our results are formalized in Agda.
Aditya Ranjan Jha, Jason Zhijingcheng Yu, Umang Mathur, Prateek Saxena
Hardware components communicate through clock-cycle-sensitive protocols. Hardware Description Languages (HDLs), however, provide limited support for expressing these protocols or for checking that independently developed components agree on them. When components disagree, the composed design can perform unsynchronized exchanges or stop making progress. We call these failures communication-safety violations. Communication safety is thus a global property, determined by interactions between components. This makes it difficult to check modularly. This paper presents Pact, a typed extension of Anvil for modular verification of communication safety in synchronous hardware. Pact types describe message-passing, control-flow, and clock-cycle behaviour. Each component is checked against its type. Compatible types guarantee that the components compose into a communication-safe system. Pact also supports incremental design. It can check a subsystem before the rest of the system exists. The check produces a summary type that captures the communication behaviour left for future compositions. To reduce annotation burden, Pact infers types by abstracting payload values while preserving communication, timing, control, and fairness. These inferred types are optimal for the checker: whenever some checker-accepted types can prove compatibility, the inferred types can prove it as well. Type inference and type checking are decidable, and compatibility is decided by a sound and complete algorithm. We implement Pact by extending the Anvil compiler and evaluate it along five dimensions: detecting communication errors in incremental design, expressiveness on ten clock-cycle-accurate translations of open-source hardware IPs, compatibility-checking time, generated hardware overhead, and annotation burden. Pact expresses realistic protocols and verifies all ten benchmarks in reasonable time.
We present \tool, a query-efficient framework for black-box probabilistic verification. Given a fixed, sampleable input distribution and a binary property oracle, \tool assesses the property's violation probability $p$ against a threshold $θ$. Under independent sampling and stateless oracle behavior, acceptance asserts $p\leθ$, rejection asserts $p>θ+η$ for a user-specified separation margin, and an inconclusive verdict indicates insufficient evidence for either conclusion. The probability of each type of erroneous verdict is bounded by its specified error budget. To support this three-valued contract efficiently, \tool uses a single sequential test, eliminating the interval family required by the baseline. The test accounts for repeated sampling checks through either corrected exact binomial confidence intervals or an anytime-valid confidence sequence. We apply \tool to probabilistic local model semantic consistency, where the property oracle detects decision-level inconsistencies between reference and compiled executions under a specified perturbation distribution. Our evaluation covers 24 tasks across TorchInductor and TensorRT and examines sampling efficiency, conclusiveness, and diagnostic behavior. For sampling efficiency, we use paired one-model clean-label radius searches: the baseline requires 3.6-4.2 times as many unique samples under matched numerical parameters while providing a weaker decision contract. For model semantic consistency, checks at $θ=10^{-3}$ yield 817 acceptances, 19 inconclusive verdicts, and 4 rejections across 840 input--backend instances from 21 tasks. Case studies of two documented compiler faults further demonstrate what these local verdicts can diagnose.
Early AI programs were often also theories of how people think, and programs that wrote programs were, in part, theories of how people program. Here we report on the reanimation of two such programs that offer two seemingly different theories of programming and were developed for quite different purposes. The first, Herbert Simon's Heuristic Compiler (1961), was an experimental model of programming as problem-solving, applying the means-ends analysis methods of the General Problem Solver to investigate the nature of the programming task. The second, KBEmacs (1984), was a working prototype of an intelligent programming assistant developed by MIT's Programmer's Apprentice project, built on the view that expert programmers recognize and combine familiar patterns, or "cliches." It let a programmer build up programs by combining cliches through a stylized English command language. We approach both through the methodology of Executable Archaeology, the study of historical computational systems by running their original code, a process we call "reanimation." Our reanimation of the Heuristic Compiler reproduces the compiled code appearing in Simon's 1963 paper, and our reanimation of KBEmacs reproduces the SQRT sequence of its December 1984 self-test. Examined side by side, the two theories turn out to have much in common: the Heuristic Compiler also works by adapting existing routines, and Simon later argued that search alone requires a large body of programming knowledge. To highlight the reflexivity of this project, we deliberately used a modern AI-assisted programming tool, Anthropic's Claude Code (Opus 5.5), to carry out much of the detailed reanimation work, building on a significant base of existing software. The explicit, executable theories of programming that both systems embodied are largely absent from today's far more capable AI coding assistants.
Classical panic-mode recovery skips a failed scan forward by convention, promising progress but no repair-universal boundary guarantee for where it lands. We choose the resume position by theorem, via a committed-prefix lemma over certificates posted for parallel lexing (arXiv:2608.03473, arXiv:2608.09761): a position is a sound recovery point when every prefix repair whose scan commits through the certificate's returned evidence places a token boundary there. This quantifier is strictly stronger than its complete-repair special case, and at a sound recovery point the inclusion is strict precisely when no repair completes while some scan commits through the evidence. The evidence-returning interface pairs each answer with the interval it rests on, so a caller who knows what the scanner cannot check decides whether the boundary transfers to the intended input. The search provably terminates; the guarantee is relative to the active mode's automaton. For an automaton of n states the quantifier is decided exactly from the preserved tail by at most n + 1 representative repairs, and a shortest reaching repair has at most n - 1 symbols and a shortest counterrepair at most n, both tight. Every anchor of an m-byte input is profiled in $O(nm + n|Σ|)$ time. The shipped repair routines are the complete-repair case, which proves their contracts. In a deterministic corruption study of munch's procedure beside skip-one and delimiter recovery, every certified answer whose evidence survives the damage passes its landing check on every move, 40,885 of 40,885, while the 5,595 first answers resting on evidence the damage reached land 1,589 times, reported, not asserted. Of the 16,808 trials labeled beyond repair, 13,522 resume on a suffix that tokenizes whole, where both quantifiers are provably empty, and 3,286 stay undetermined, their damaged inputs not archived.
Ritika Poddar, Aidan Fennelly, Deirdre Murphy, Eric Wolos, Corre L. Steele, Michael Doyle
Large Language Models (LLM) are increasingly applied to Reverse Engineering (RE) workflows. RE, however, differs from common LLM coding tasks as it requires models to reason about low-level program behavior. Furthermore, the deployment of tooling in resource-constrained sandboxed RE environments limits the ability to use frontier-scale solutions. We examine whether a targeted LLM training approach can transfer distinct RE skills to open models via inverse basic-block execution: given an x86-64 basic block and a desired output register state, the model predicts the input register values that produce it. Fine-tuning \texttt{Qwen3-1.7B} and \texttt{Nemotron-3-Nano} with Group Relative Policy Optimization (GRPO) raises knowable-register prediction accuracy from 73.2\% to 85.3\% and from 63.3\% to 95.2\%, respectively. Frontier models still score highest (up to 99.2\%), but our fine-tuned \texttt{Nemotron-3-Nano} comes within four points at a fraction of the parameter count. We release both fine-tuned models and the training dataset.
Rajan Maghera, Asher Tempest Arya, Aren A. Babikian, Marsha Chechik, Maryam Mehri Dehnavi
Large language models (LLMs) are increasingly used for code generation, motivating techniques that guarantee the structural and semantic correctness of generated programs. Constrained decoding enforces correctness during generation by restricting token choices to those that admit at least one valid completion. While existing approaches can enforce syntactic constraints and selected semantic properties such as type safety, they either target specific properties or rely on operational pruning mechanisms that are difficult to generalize to data-dependent, inductive program properties. We present AGDecode, a programmable framework for semantic constrained decoding based on least-fixed-point semantics. AGDecode extends attribute grammars to partially constructed syntax trees, and reduces semantic constrained decoding to a realizability problem over such trees. The framework compiles semantic specifications into systems of relational constraints that are discharged by external verification oracles, such as SMT and CHC solvers, cleanly separating language semantics from constraint-solving machinery. We prove that our approach is sound and complete relative to an ideal verification oracle. In practice, solvers inevitably encounter uncertain queries; conservatively, our system can reject tokens for soundness or speculatively continue to generate until later queries resolve the entire generation. We mechanize the core metatheory in Rocq and evaluate the framework on semantic-constrained generation of C programs, enforcing path-sensitive safety properties including null-pointer safety, division-by-zero freedom, and initialized-variable usage. Our results demonstrate that solver-backed semantic constrained decoding can enforce rich semantic guarantees while incurring modest computational overhead at regular program boundaries.
Adrienne Lancelot, Giulio Manzonetto, Guy McCusker, Gabriele Vanoni
The relational semantics of linear logic is a powerful framework for defining resource-aware models of the $λ$-calculus. However, its quantitative aspects are not reflected in the preorders and equational theories induced by these models. Indeed, they can be characterized in terms of (in)equalities between Böhm trees up to extensionality, which are qualitative in nature. We employ the recently introduced checkers calculus to define a quantitative contextual preorder on $λ$-terms, and demonstrate that it coincides with the preorder associated to the relational semantics.
Microkernels provide good features such as high security, safety, and flexibility, but their reliance on hardware-based isolation leads to heavy performance overhead, limiting their widespread adoption. Although constructing single-address-space microkernels based on safe language-based isolation is a promising approach to addressing the performance issue, this approach still faces challenges in maintaining the principle of minimality and enforcing capability-based, fine-grained access control over system resources. We propose safeL4, an approach to constructing microkernels based on safe languages. It guarantees minimality through low-level abstractions for unsafe operations, and implements a capability system based on the safe language's object capabilities to achieve fine-grained access control over all operations on system resources. We implement a prototype system in Rust, and our evaluation results show that the primitives provided by safeL4 are, on average, 1.9$\times$ faster than those of seL4.
React is currently the most popular JavaScript library for front-end web development. It endows UI components with state via the useState construct, through a mechanism that we name hook-indexed state. However, React's implementation of hook-indexed state is both fragile and poorly understood. Programmers frequently experience unexpected behavior, and the benefits of programming in this paradigm are wholly unclear. We define $λ^\mathsf{react}_\mathsf{hook}$, a core calculus that captures the essence of hook-indexed state, and give it a type system to statically rule out unexpected behavior. We then translate $λ^\mathsf{react}_\mathsf{hook}$ into a calculus $λ^\mathsf{react}_\mathsf{ref}$ based on ML-style references, and prove that this translation preserves typability and semantics, thus showing that hook-indexed state is expressible in terms of standard references. The translation is local and admits a compositional definition, but involves significant code duplication. As well as illuminating the essence of state in React, our observations can inform the design of future reactive programming systems.
Tanaka et al. proposed a type system for verifying functional correctness properties of programs that use arrays and pointer arithmetic. Their system extends ConSORT--a type system combining fractional ownership and refinement types for imperative program verification--with support for pointer arithmetic. Their idea was to extend fractional ownership so that it can depend on an array index. Their formulation, however, does not handle nested arrays, which are essential for representing practical data structures such as matrices. We extend Tanaka et al.'s type system to support nested arrays by allowing ownership to depend on the indices of enclosing arrays. We formalize the extended calculus in Rocq using a mixed embedding and provide a machine-checked proof of type soundness. We have implemented a verifier based on the proposed type system and demonstrated that it can verify the correctness of programs that manipulate nested arrays, which were beyond the reach of Tanaka et al.
Verifying quantum programs today requires specialized proof systems built on interactive theorem provers such as Rocq, Lean, Isabelle, or Why3, and even modest quantum algorithms cost substantial human effort to verify. Because quantum programs cannot be effectively checked by runtime testing, formal verification is the only viable path to correctness, making the cost of these bespoke systems the chief barrier to scalable quantum software assurance. We show that verifying a quantum program should be no harder than verifying a classical array program, a paradigm commonly used in parallel programming: the Qafny quantum proof system translates into Hoare logic with array theory completely (every Qafny proof becomes a valid Hoare triple) and soundly (a valid translated triple certifies only true quantum specifications), and we mechanize the completeness direction in Rocq. The embedding determinizes quantum proof obligations and exposes the full machinery of classical automated verifiers (e.g. Dafny and SMT-based separation logic) to quantum code, removing the need for dedicated quantum proof system infrastructure. In particular, the embedding supplies the correctness argument that the existing compilation of Qafny into Dafny lacks.
Simon Fowler, Duncan Paul Attard, Danielle Marshall, Simon J. Gay, Phil Trinder
The asynchronous and unidirectional communication model supported by mailboxes is a key reason for the success of actor languages like Erlang and Elixir for implementing reliable and scalable distributed systems. Although actors eliminate many of the issues stemming from shared memory concurrency, they remain vulnerable to communication errors such as protocol violations and deadlocks. Behavioural types make it possible to detect communication errors early in the development process, but most work has addressed channel-based languages rather than actor languages. Mailbox types are a novel behavioural type system for actors first introduced for a process calculus, and capture the contents of a mailbox as a commutative regular expression. Due to aliasing and nested evaluation contexts, moving from a process calculus to a programming language is challenging. This paper presents Pat, the first programming language incorporating mailbox types, and describes an algorithmic type system. Pat is a higher-order functional language with sums, products, and lists, along with interfaces that allow finer-grained reasoning about mailbox contents. Typechecking in Pat detects four classes of behavioural error: protocol violation, unexpected message, forgotten reply and self-deadlock, as well as the usual data type errors. The Pat type system makes essential use of quasi-linear typing to tame some of the complexity introduced by aliasing. We make use of a co-contextual algorithmic type system, achieved through a novel use of backwards bidirectional typing, and we prove it sound and complete with respect to our declarative type system. We implement a type checker, and use it to demonstrate the expressiveness of Pat on a factory automation case study and a series of examples from the Savina actor benchmark suite. This establishes a foundation for applying mailbox typing to practical actor languages.
What does a recursive definition mean when the logic is grounded, so a sentence is true only if a terminating process makes it so? Kripke's answer for the special case of truth was the least fixed point. This paper takes that answer as a rule. Reflective Grounded Arithmetic (RGA) already writes any recursive definition as one self-referential term, paradoxes included. Inductive Grounded Arithmetic (IGA) adds the elimination rule for every positive one, so that accessibility, the winning positions of a game, and grounded truth itself each come with their own induction principle. The rule is sound for the omega model and the system is consistent, both machine-checked in Isabelle/HOL. With the rule, IGA proves Goodstein's theorem outright, in a logic without implication at an undecided hypothesis, and the Kirby-Paris hydra game for primitive recursive strategies, both with every step of the arithmetic a grounded derivation. It proves the Cantor normal forms well-founded, from which the well-foundedness of the standard $\varepsilon_0$ notation system in HOL follows, and it certifies the Veblen notation as an ordinal below every $\varphi(n,0)$. It defines Kripke truth for RGA's own language as one fixed point that agrees with the omega model exactly. Two equivalences locate what the classical world has and the grounded one does not. IGA proves the whole Veblen notation well-founded exactly when it admits bivalence of accessibility for that order, and bivalence of accessibility for an order is sound exactly when the order is well-founded; so $Γ_0$ lies at most one instance of excluded middle away, at the accessibility predicate of the notation, and that instance, the well-foundedness sentence and one membership claim in a primitive-recursive form of Kleene's $\mathcal O$ are interderivable over IGA.
A certified split point lets a parallel lexer cut unlexed input at a single byte with the serial token stream provably preserved, but several conventional token sets in the predecessor's controlled study certify no byte once string, comment, or whitespace-run forms are included (arXiv:2608.03473v2). We generalize from a byte to a bounded window, a byte string after which the position where the current token began is known, regardless of surrounding context. We certify the directly usable form of that recovery, namely that the token covering the window's final byte begins at the reported origin. The certificate is conditional on occurrence and may be vacuous; every applicability figure counts only windows carrying an asserted completely tokenizable occurrence witness. We give a conservative model of a maximal-munch scanner's possible histories across a window, prove it sound, and decide reachability in that model exactly by exhausting a finite quotient of its reachable configurations. Within the flat, completely tokenizable scope, model-positive answers are semantic certificates; negatives are relative to the model, which deliberately refuses some windows a greedy scanner would allow. Whether the model certifies any window, plain or witnessed, is PSPACE-complete, and a shortest window can need $2^{Ω(\sqrt{n})}$ bytes over n live states. Two smaller searches decide plain model existence, the second shipped in release 2.2.0 of munch. In a sample of 400 random token sets, 322 of the 337 sets certifying no byte gain a witnessed window, with zero inconclusive searches, and every exact-empty row of the predecessor's study gains a witnessed window of two to four bytes. The analysis runs once after automaton construction, using only the compiled tables and no input. A boundary profile marks each gap of a window forced, crossed or open, and a window-local cut is sound exactly at forced gaps.
Table-driven DFA lexing is sequential, since each transition depends on the previous byte's state. Scanning one input in parallel needs each chunk's entry state, which existing methods recover by simulation, speculation, prescanning, or overlap. We give two conditions under which none is needed. For a longest-match scanner restarting from q0 at every token boundary, a byte b is a certified split symbol when no reachable state other than q0 has a b-transition whose target can reach acceptance, and q0 is not re-entrant if it has one. Every occurrence of such a byte in completely tokenizable input begins a token, so chunks starting there reproduce the serial sequence of kinds and lengths. The condition is necessary and sufficient, but one string, comment, or whitespace run can remove every useful certificate. Comments and whitespace are usually discarded, so we weaken the guarantee to equality after deleting a declared discarded set and give a second condition, a precomputed constant-time one-bit test. It is sound but incomplete and more permissive, strictly so on suitable token sets and discarded sets. It recovers newline for a conventional C-like tokenization and tab, newline and carriage return for JSON, and refuses newline where block comments are unrestricted. Safety modulo the discarded set is decidable in PSPACE for every token automaton and in polynomial time for literal vocabularies, and every unsafe byte has a replayable counterexample. On the fifteen token sets studied the second condition is already exact. Splitting at exact certificates in munch reaches 92.6-95.3% parallel efficiency at eight threads on a restricted CPU set and a 512 MiB corpus, and a 3.46-3.94x end-to-end speedup at four threads, on one machine. It turns delimiter-based parallel lexing from a language-specific assumption into a property a compiler checks.
Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems
Shubham Agarwal, Alexander Krentsel, Shu Liu, Mert Cemri, Audrey Cheng, Rui Meng, Tomas Pfister, Chun-Liang Li 等 13 位作者
AI 速览：提出归纳演绎合成（IDS）智能体系统，联合增量地合成实现与证明，从失败中学习策略，为分布式系统生成形式化验证的代码。
AI agents increasingly excel at generating, testing, and refining code. However, they fall short on tasks requiring formal guarantees of full coverage that testing alone cannot provide. Distributed systems are a prime example: properties such as consistency between reads and writes must hold under every possible interleaving of events. Mechanized formal verification can guarantee such correctness, but typically demands months to years of expert effort. As evidence, even SOTA coding agents (Codex with GPT-5.4 and Claude Code with Opus 4.6) succeed on only 2/7 distributed key-value-store specifications. In this paper, we present the first effective approach to addressing this gap, Inductive Deductive Synthesis (IDS), which jointly and incrementally synthesizes implementation and proof, and learns from failed attempts to systematically try promising strategies. Built as an agentic LLM system, IDS achieves 7/7 in about 6.8 hours and $106 per spec on average, roughly 200x faster than expert effort and 17% cheaper than SOTA agents. IDS further incorporates performance feedback into the same loop, yielding implementations up to 3x faster than published verified systems.
Hongzheng Chen, Alexander Novikov, Ngân Vũ, Hanna Alam, Zhiru Zhang, Aiden Grossman, Mircea Trofin, Amir Yazdanbakhsh
Modern compilers rely on hand-crafted heuristics to guide optimization passes. These human-designed rules often struggle to adapt to the complexity of modern software and hardware and lead to high maintenance burden. To address this challenge, we present Magellan, an agentic framework that evolves the compiler pass itself by synthesizing executable C++ decision logic. Magellan couples an LLM coding agent with evolutionary search and autotuning in a closed loop of generation, evaluation on user-provided macro-benchmarks, and refinement, producing compact heuristics that integrate directly into existing compilers. Across several production optimization tasks, Magellan discovers policies that match or surpass expert baselines. In LLVM function inlining, Magellan synthesizes new heuristics that outperform decades of manual engineering for both binary-size reduction and end-to-end performance. In register allocation, it learns a concise priority rule for live-range processing that matches intricate human-designed policies on a large-scale workload. We also report preliminary results on XLA problems, demonstrating portability beyond LLVM with reduced engineering effort.