1 Introduction↩︎

AI has become a standard tool for code generation, driven by the growing capabilities of large language models (LLMs) and LLM-based coding agents [1]. Yet AI-generated code remains error-prone, threatening the correctness and security of downstream software systems [2], [3]. This makes languages with rich static semantics particularly valuable for AI-generated code. Rust, for example, uses its ownership and borrowing discipline to provide memory safety guarantees and prevent related reliability and security failures [4], [5]. At the same time, these guarantees are enforced through strict compile-time rules, making valid code harder to generate than in more permissive languages such as C [6]–[8]. Compiler feedback can help bridge this gap by identifying violations and guiding the model toward code that satisfies these rules.

1.0.0.1 Post-Generation Compiler Feedback

The most common way to leverage compiler feedback is to wait until entire files are fully generated, run the compiler as is on the resulting program, and feed any diagnostics back to the model. This post-hoc feedback loop has important practical advantages: it works with black-box LLMs and benefits from the compiler’s guarantees and diagnostics with no additional implementation cost [9]–[11]. However, it does not take advantage of the intermediate outputs produced during generation. Feedback becomes available only after the complete program has been produced, meaning that every token emitted after the first unrecoverable error may be based on invalid assumptions and ultimately wasted. Moreover, since the feedback concerns the entire output, the model receives a batch of accumulated diagnostics all at once, which can be large enough to hinder model understanding [12], [13].

1.0.0.2 Constrained Decoding

Constrained decoding instead intervenes directly during generation. It checks intermediate outputs of LLMs, accepting only tokens that keep the current output extendable to a valid program [14]–[18]. Thus, if generation terminates, the final output is guaranteed to be valid. However, for languages with expressive static semantics, achieving this guarantee requires substantial language-specific reimplementation, making it effectively impractical to support more than restricted fragments [18]–[20]. Moreover, token-level filtering is silent: the model is steered away from invalid continuations, but never receives compiler-style explanations that could help it revise the code. Finally, constrained decoding requires white-box access to the model’s next-token distribution and sampling process, ruling out its application to frontier models exposed only through black-box APIs [15], [21].

1.0.0.3 This Work: Generative Compilation

We introduce generative compilation, the first approach to make compiler-style feedback available during code generation. It serves as a middle ground between post-generation feedback and constrained decoding, addressing key limitations of both. Like constrained decoding, a generative compiler processes partial programs while they are being produced. Unlike constrained decoding, however, it provides compiler-style diagnostics upon rejection. The model receives an explanation of what went wrong and can revise the generated code, rather than being silently steered away from invalid tokens. Because the feedback is obtained on partial code, it concerns only isolated coding mistakes and avoids contextual clutter. Further, the technique works with black-box models and reuses existing compiler infrastructure.

To enable generative compilation, the core new concept we introduce is a sealor: a transformation that closes a partial program into a complete one by filling in missing syntactic structure and inserting well-typed placeholders. The resulting sealed program can then be checked by an existing compiler. The key challenge is designing the sealor to achieve both faithful feedback and error coverage. Compiler rejection of the sealed program should guarantee that the partial program truly requires revision. At the same time, sealing should expose as many dead ends as possible, so that unrecoverable errors are caught early. We formalize these properties through corresponding completeness and soundness guarantees.

Our key insight is that a lightweight, mostly syntax-guided sealor can already meet the guarantees we target, without reimplementing the target language’s type system. We first demonstrate this on Featherweight Rust (FR), a compact calculus inspired by Rust’s ownership and borrowing discipline [22]. We develop a sealor for FR and prove that it satisfies the desired properties, with the full development mechanized in Lean. We then carry the same methodology to real Rust: the sealor preserves generated syntax, inserts a small set of placeholders for missing code, and delegates type, borrow, and lifetime reasoning to rustc, the Rust compiler.

We perform an extensive evaluation across seven frontier black-box and open-weight LLMs. We focus on two repository-level code generation tasks for Rust, designed to stress compiler feedback: C-to-Rust translation and code generation against recently updated library APIs. The results show that, compared with post-generation feedback, the on-the-fly feedback loop enabled by generative compilation further reduces compiler errors and improves functional correctness in most model-task configurations. We then analyze how: generative compilation provides more focused diagnostics that are close to the error source and available well before file completion.

1.0.0.4 Key Contributions

In summary, our main contributions are:

• We introduce generative compilation, a novel framework enabling off-the-shelf compilers to check partial programs during code generation. We define the notion of sealors and prove that their completeness and soundness lift to generative compilation. (3)

• We instantiate generative compilation on FR, presenting a syntax-guided sealor that never rejects partial programs that admit valid completion and correctly flags an important class of partial programs with no valid extension. We fully mechanize FR, our sealor, and its guarantees in Lean, making a number of corrections to the original FR formalization in the process. ([sec:lang] [sec:method])

• We apply our methodology to real Rust and build the first partial-program checker for Rust. This is based on a practical sealor that delegates semantic checking to rustc while handling Rust-specific syntax, control flow, placeholders, and future-dependent errors. (6)

• We evaluate our approach extensively on Rust coding tasks across frontier and open-weight models, showing that it reduces compiler errors, improves functional correctness, and detects various errors early during generation. (7)

2 Motivation for Generative Compilation↩︎

Today’s AI-based code generation is largely powered by LLMs. However, LLM-generated code provides no guarantee of respecting the target language’s static rules. Two existing strategies aim to address this gap: post-generation compiler feedback and constrained decoding. In this section, we present both strategies and use a running example to show their limitations, thereby motivating generative compilation.

2.0.0.1 Code Generation with Language Models

Let \(M\) denote an LLM that generates code autoregressively, one token at a time from left to right. These tokens are drawn from a fixed vocabulary \(\Sigma\), determined by \(M\)’s tokenizer. Modern LLM tokenizers are universal: any string can be constructed from tokens in \(\Sigma\) [23]. We therefore take \(\Sigma^{\ast}\) to be the domain of all strings.

None

Given a prompt \(x\) (a natural-language task, optionally with reference code) and the code generated so far \(c\), \(M\) produces a next-token distribution \(M(\cdot \mid x \circc)\), where \(\circ\) denotes string concatenation. A token \(t \sim M(\cdot \mid x \circc)\) is sampled, appended to \(c\), and generation repeats until a special end-of-sequence token \(\mathsf{EOS}\) is produced. As discussed above, this process can generate any string in \(\Sigma^{\ast}\). However, for a target language \(L\subseteq \Sigma^{\ast}\), there is no a priori guarantee that the final output lies in \(L\). For example, when prompted to write a Rust function that strips a fixed-size header from a message and formats the result for logging, an LLM might produce the code in 1. Running the Rust compiler on this program reveals that it cannot be compiled.

2.0.0.2 Post-Generation Compiler Feedback

Most programming languages provide a practical checker \(\mathcal{C}\) that decides, for a given string \(c\), whether it belongs to the language \(L\), i.e., whether \(c\) is syntactically well-formed and type checks. Although compilers perform many tasks, such as optimizing code and emitting assembly, it is common to refer to this checking phase as “compiling”; following this convention, we call the checker a “compiler” in this paper.

Formally, we model the compiler as a function \(\mathcal{C}: \Sigma^{\ast} \to \mathbb{B}\times \Sigma^{\ast}\), which maps an input string \(c\) to a pair \((\mathsf{ok}, \mathsf{err})\) consisting of a Boolean verdict and a textual diagnostic. If \(c \in L\), then \(\mathcal{C}(c) = (\mathrm{true}, \texttt{\textquotedbl\textquotedbl})\), i.e., the textual diagnostic is empty; otherwise, \(\mathcal{C}(c) = (\mathrm{false}, \mathsf{err})\), where \(\mathsf{err}\neq \texttt{\textquotedbl\textquotedbl}\) is an error message explaining why \(c \notin L\), e.g., by highlighting a failed type check, and potentially suggesting how to resolve the issue, e.g., by suggesting a type cast. The compiler can be naturally used in a feedback loop for LLM-based code generation: after the model generates a full program \(c\), we obtain \((\mathsf{ok},\mathsf{err}) \coloneq \mathcal{C}(c)\). If \(\mathsf{ok}=\mathrm{true}\), generation terminates and \(c\) is guaranteed to be an element of \(L\). Otherwise, the model is asked to try again with the original prompt augmented by the generated program and diagnostic, e.g., \(x \circc \circ\mathsf{err}\).

None

For the example program in 1, running the compiler returns \((\mathrm{false}, \mathsf{err})\), with \(\mathsf{err}\) shown in 2. The error involves Rust’s ownership, borrowing, and lifetime discipline: a value may be accessed through either shared immutable references or an exclusive mutable reference, but not both during overlapping lifetimes. At Line 2, the slice tag is an immutable borrow of msg. The call to msg.drain at Line 3 then attempts to mutably borrow msg while that immutable borrow is still live, because tag is later used at Line 4. This diagnostic is then appended to the prompt, and the model is asked to fix the error, either by regenerating the program from scratch or by editing the existing program. 3 shows a valid outcome that fixes the error by making tag an owned copy of the header rather than a borrow from msg. The temporary immutable borrow used to create this copy ends before msg.drain takes a mutable borrow, so the two borrows do not overlap and the program satisfies Rust’s rules.

None

This feedback loop pays for its simplicity through delayed feedback. In 1, the borrow conflict already manifests at Line 4. However, compiler feedback is obtained only after the model finishes generating the entire function at Line 8. For longer programs in practice, early mistakes can influence subsequent generation and snowball before the model receives any signal from the compiler. As a result, additional mistakes can be introduced and multiple errors may be reported together in a single diagnostic bundle, making each repair attempt harder and slowing the overall trial-and-error design process.

2.0.0.3 Constrained Decoding

Constrained decoding offers an alternative to compiler feedback loops. It exploits the autoregressive nature of LLM generation by intervening during decoding, rather than waiting until the entire program has been emitted. Specifically, constrained decoding relies on a prefix checker \(\mathcal{P}: \Sigma^{\ast} \to \mathbb{B}\), where \(\mathcal{P}(c)=\mathrm{true}\) if the current output \(c\) can still be extended into a full program in \(L\), or formally, if \(\exists w.\;c \circw \in L\). At each decoding step, candidate tokens are filtered through \(\mathcal{P}\), so that only tokens \(t\) satisfying \(\mathcal{P}(c \circt)=\mathrm{true}\) may be selected. As a result, invalid continuations are ruled out as soon as they arise, and every generated partial program remains a prefix of some valid program in \(L\).

Prefix checking solves a different problem from conventional compilation: the former must reason about partial programs, whereas the latter assumes full programs as input. This creates a major implementation burden. Existing compiler infrastructure cannot be used directly, so constrained decoding systems must often reimplement the relevant language semantics for prefix checking. For general-purpose programming languages, matching the behavior of the full compiler in this way is impractical. For example, the compiler-related part of the Rust codebase alone contains more than 600k lines of code [24]. As a result, existing constrained decoding systems either enforce only syntax [15], [16], [25] or cover a restricted subset of typing [18], [20].

None

Assume for now that a (well-implemented) constrained decoding engine for Rust is available, and let us again examine the example program in 1. Constrained decoding has no effect as long as each next token keeps the partial output extendable to a valid program. Thus, the model generates the same prefix up to let prio = tag, shown in 4. This prefix is still valid: tag may refer to the prefix of an identifier to be defined later, such as a function name. However, when selecting the next token, the . used in the original program must be rejected by prefix checking. Choosing . commits tag to the existing variable, which triggers the same borrow conflict. Therefore, to remain on a valid path, the model must choose the unnatural use-before-definition continuation.

This example exposes two further costs of constrained decoding. First, constrained decoding silently filters out the token . and can only shape future continuations. The model is never told why the token was rejected, nor can it revise the already generated prefix, as the repair in 3 would require. The only way forward is to force the model onto the low-probability use-before-definition path described above. This can degrade global generation quality, especially when the rejection is due to non-local semantic constraints such as Rust’s borrow checking [16], [17], [25]. Second, filtering and resampling tokens require white-box access to the model’s next-token distribution, which rules out the closed-weight frontier models that currently dominate coding workflows in practice.

2.0.0.4 Generative Compilation on the Running Example

Prior work has made valuable progress on addressing the limitations of constrained decoding from the perspective of probabilistic sampling [16], [17], [25]–[29]. In contrast, our generative compilation approach aims to explore a different route. Like constrained decoding, it operates on partial programs rather than waiting for a full program. Like conventional compilation, however, it produces textual feedback rather than altering the sampling process. Crucially, it does so through a lightweight implementation that largely reuses existing compiler infrastructure and supports black-box models available only through APIs. As a result, generative compilation addresses the limitations of the two strategies above.

We now use the running example to sketch how generative compilation handles partial programs. The key idea behind it is to seal partial programs, turning them into full programs that can be checked by a conventional compiler. From the discussion above, the error in 1 already manifests when generation reaches the prefix in 4, including .. There, the program has committed to referring tag to the previously defined variable, which violates Rust’s borrow-checking rules. Through a series of rule applications, our sealor transforms this partial program into the full program shown in 5. The sealed program preserves the access to tag at Line 4. It then inserts a generic placeholder, \(\mathtt{hole}_\mathtt{val}()\) at Line 5, which represents an arbitrary well-typed value. In this example, it is a value of the function’s \(\mathtt{String}\) return type. Finally, the sealor closes the function at Line 6 such that the program is syntactically well-formed.

None

Compiling the sealed program exposes the same semantic issue as the full program in 1: tag still borrows from msg across the call to msg.drain. Thus, the Rust compiler rejects 5 with a similar borrow-checking diagnostic. Compared with the partial program in 4, the sealed program has only inserted \(\mathtt{hole}_\mathtt{val}()\), which does not introduce type errors, and completed the missing syntax. Thus, the borrow-checking error reported on the sealed program reflects a genuine error already committed by the partial program. This is one of the guarantees we aim to obtain from the sealor: compiler errors on sealed programs should correspond to errors in the original partial programs, rather than artifacts of sealing.

We then map the diagnostic produced on the sealed program back to the partial program by comparing source-code spans. The model receives the partial program together with the mapped diagnostic, but never sees the sealed program itself. With this feedback, it ultimately produces the same repaired program as in 3, making tag an owned copy rather than a borrow from msg. Generative compilation therefore provides the relevant feedback four and a half lines earlier than post-generation feedback, when the error first becomes unavoidable.

3 Generative Compilation↩︎

Next, we formally define generative compilation in a generic, language-agnostic form.

3.1 Generative Compilers and Sealors↩︎

3.1.0.1 Generative Compilers: Definition

A generative compiler is a function \(\mathcal{G}: \Sigma^{\ast} \to \mathbb{B}\times \Sigma^{\ast}\). That is, it has the same interface as a conventional compiler and returns a Boolean verdict \(\mathsf{ok}\) together with a textual diagnostic \(\mathsf{err}\). However, instead of checking whether a complete program belongs to \(L\), it performs prefix checking, i.e., whether a partial program \(c\) admits a valid completion. Unlike constrained decoding, a generative compiler retains compiler diagnostics: \(\mathsf{err}\) is empty whenever \(\mathsf{ok}=\mathrm{true}\) and otherwise provides a textual explanation, rather than a silent rejection signal.

3.1.0.2 Generative Compilers: Completeness and Soundness

We say that a generative compiler \(\mathcal{G}\) accepts \(c\) when it returns a positive verdict on \(c\), i.e., when \(\mathcal{G}(c) = (\mathrm{true}, \texttt{\textquotedbl\textquotedbl})\). It is complete on a class of programs \(\mathcal{X}\subseteq \Sigma^{\ast}\) if for all \(c \in \mathcal{X}\), \(\exists w.\;c \circw \in L\) implies that \(\mathcal{G}\) accepts \(c\). It is sound on \(\mathcal{X}\) if for all \(c \in \mathcal{X}\), \(\mathcal{G}\) accepts \(c\) implies \(\exists w.\;c \circw \in L\). Intuitively, completeness rules out rejecting partial programs that admit valid extensions, whereas soundness rules out accepting dead-end partial programs. We say \(\mathcal{G}\) is globally complete or sound, when \(\mathcal{X}= \Sigma^{\ast}\). \(\mathcal{G}\) is exact on \(\mathcal{X}\) iff it is sound and complete on \(\mathcal{X}\). Note that the first output of \(\mathcal{G}(c)\) can be viewed as a prefix checker, inheriting the corresponding notions of soundness and completeness [18].

3.1.0.3 Sealors: Definition

Generative compilation seeks to reuse the existing compiler to obtain rich feedback and avoid costly reimplementation, while checking partial programs during generation. This is achieved through a new notion of sealing, which we define now. A sealor is a lightweight, language-specific transformation \(\mathcal{S}: \Sigma^{\ast} \to \Sigma^{\ast}\) that attempts to close the unfinished structure of a partial program. Its goal is to produce a closed form that a conventional compiler can process, thereby obtaining a verdict and diagnostic.

Given a compiler \(\mathcal{C}\) and a sealor \(\mathcal{S}\), the induced generative compiler is defined by \(\mathcal{G}_{\mathcal{C},\mathcal{S}}(c) \coloneq \mathcal{C}(\mathcal{S}(c))\). This definition abstracts away a practical mismatch: diagnostics produced by \(\mathcal{C}\) refer to the sealed program \(\mathcal{S}(c)\), whereas the model should receive feedback on the original partial program \(c\). This can be addressed by post-processing diagnostics, for example, by mapping source spans in \(\mathcal{S}(c)\) back to their corresponding spans in \(c\). We discuss this implementation detail for Rust in 6.1; for simplicity, we assume for now that diagnostics are reported on the corresponding spans of the partial program \(c\).

3.1.0.4 Sealors: Completeness and Soundness

We define completeness and soundness for sealors analogously to generative compilers.

Intuitively, completeness requires that sealing turns every prefix with a valid continuation into a valid program, whereas soundness requires that sealing not make a dead-end prefix appear valid. Assuming \(\mathcal{C}\) is exact, the completeness and soundness of a sealor correspond directly to those of its induced generative compiler.

These characterizations give semantic proof obligations for a sealor, which can be established from the metatheory of the target language and then lifted to completeness or soundness of the induced generative compiler. We dive deep into this for our FR sealor in 5.

3.1.0.5 Target Guarantees: Global Completeness and Selective Soundness

Achieving both global completeness and global soundness amounts to exact prefix checking, which is undecidable in general for expressive semantic constraints [20]. Constrained decoding faces this difficulty at every decoding step. Because emitted tokens cannot be revisited, it typically requires global soundness to inductively ensure that generation always remains on a path that admits a valid extension. Token-level completeness is not required, but highly desirable: rejecting a token prematurely that could still lead to a valid program may significantly degrade model performance under constraints [25], [30]. Maintaining both properties token by token pushes constrained decoding toward exact prefix checking. When constrained decoding should support rich static semantics, this causes substantial reimplementation effort of the corresponding semantic analysis such as typing [18].

For generative compilation, the priorities for soundness and completeness change, with incompleteness becoming the more harmful failure mode. Rejecting a partial program that admits a valid continuation causes the model to discard or revise a prefix from which a correct program could still be generated, providing spurious feedback that can confuse the model. Meanwhile, soundness can be relaxed. A rejection triggers revision: the model regenerates based on diagnostic feedback, allowing to revise already generated tokens. Missing a soundness violation is thus tolerable: the generative compiler may accept a dead-end prefix and allow generation to continue, but the error can still be caught by a later check or by final compilation, when more code context is available. Nevertheless, soundness remains valuable where it can be obtained cheaply, because it lets on-the-fly feedback arrive as early as possible. Therefore, for generative compilation, we target global completeness together with soundness on a selected class of programs \(\mathcal{X}\subsetneq \Sigma^{\ast}\).

3.2 Combining Generative Compilation and LLM-Based Code Generation↩︎

6 shows the approach we use in this paper to combine generative compilation with LLM-based code generation: the two run as (concurrent) modules that exchange only plain text. Other integration strategies are possible; we discuss them in 8.

The module on the left represents LLM-based code generation. It performs standard autoregressive decoding, as discussed in 2. Generation is interrupted and restarted whenever the module receives a new prompt \(x\) from generative compilation. As token generation proceeds, the module sends the latest partial program \(c\) to generative compilation, stopping when \(\mathsf{EOS}\) is emitted. This module does not require access to \(M\)’s token distribution or control over its sampling procedure. It only observes the current partial program \(c\) as it is generated. For frontier black-box models, this can be obtained through streaming API responses, where output is returned incrementally rather than only after completion. Although 6 illustrates communication at token granularity, the same design also works when the API returns larger chunks of text.

The module on the right performs generative compilation. It checks received prefixes using a latest-wins strategy: incoming prefixes do not interrupt ongoing validation, and prefixes received during validation are coalesced so that only the newest one is retained. When validation of a prefix \(c\) finishes with \((\mathsf{ok},\mathsf{err}) \coloneq \mathcal{G}_{\mathcal{C},\mathcal{S}}(c)\), the module acts on the verdict. If \(\neg\mathsf{ok}\), it augments the prompt with \(c\) and \(\mathsf{err}\) and sends the revised prompt to the generator. If \(\mathsf{ok}\) holds and \(c\) ends with \(\mathsf{EOS}\), it returns \(c\) as the generated program. Otherwise, \(c\) is a valid partial program, and the module begins validating the latest buffered prefix, if one is available. In the common case where the \(\mathsf{EOS}\)-terminated prefix is already a complete program, the final check coincides with ordinary post-generation compiler feedback. More generally, generative compilation and post-generation feedback are complementary and can always be combined.

When configured to run concurrently, generative compilation does not block token generation: the LLM can continue producing code while one prefix is being validated. This avoids waiting for a compiler result after every token when validation is slower than token sampling. The latest-wins strategy then retains only the newest prefix generated during validation for the next check. As a result, a rejection may arrive after the LLM has produced a few additional tokens. This extra work is modest and limited to the short suffix generated during a single validation, and once the earlier prefix is rejected, its continuation is discarded in the restarted attempt. When incremental compilation is available, as in rustc, compilation speed can increase significantly. Generative compilation benefits also from this, since it is built largely on existing compiler infrastructure.

4 FR: A Core Calculus for Rust↩︎

In this section, we review Featherweight Rust [22], a compact calculus inspired by Rust’s borrow system. We present the syntax (4.1) and typing (4.2) needed to demonstrate our generative compilation approach in 5, omitting details that are not essential here. For the full calculus, we refer readers to [22].

4.0.0.1 Why a Core Calculus

To present and analyze our approach formally, we need a language formalization. Since our target is Rust, this means a formalization for Rust, and it must satisfy two requirements. First, it should remain close to Rust’s surface syntax, because our approach directly manipulates Rust source code. Second, it should provide a compact setting in which our approach can be defined, analyzed, and understood, while still capturing Rust’s most prominent features.

Existing Rust formalizations do not simultaneously meet these requirements. RustBelt [5], RustHorn [31], and Aeneas [32] provide powerful foundations for semantic reasoning and verification, but they operate at a level of abstraction that is not sufficiently close to the source syntax, and their developments are necessarily substantial. Oxide [33] is closer to Rust’s surface syntax, but still introduces significant machinery, making it more elaborate than needed for our purpose.

4.0.0.2 Why FR

Featherweight Rust (FR) [22] follows the philosophy of Featherweight Java [34]: provide a concise and minimal proof of type soundness while preserving the essence of the soundness argument for the full language. Concretely, FR remains close to Rust’s surface syntax and captures many key aspects of Rust, including copy and move semantics, mutable and immutable borrows, and lexical lifetimes. Moreover, FR is compact and establishes soundness guarantees.

4.1 Syntax↩︎

FR’s syntax is shown entirely in 7. We highlight some important details in order of appearance.

4.1.0.1 Move vs.Copy is Syntactic

In Rust, a use of \(w\) is a copy if its type implements the \(\mathtt{Copy}\) trait, and a move otherwise. FR instead makes this distinction syntactically: \(w\) denotes a move, whereas \(\mathtt{copy}\;w\) denotes a copy. This design keeps the operational semantics independent of the type system. The type system (defined in 4.2) then enforces that copies are only performed on copyable values: \(\mathtt{copy}\;w\) is well typed only if \(w\) has type \(T\) satisfying \(\mathrm{copy}(T)\), FR’s analog of the \(\mathtt{Copy}\) trait. In our mechanization, the predicate holds for \(\varepsilon\), \(\mathtt{int}\), and shared borrows, but not for mutable borrows or boxes. Treating unit as copyable is a small adaptation relative to [22].

4.1.0.2 Lifetimes are Lexical

A block \(\{^{l}\, \overline{t}\}\) is a sequence of terms separated by semicolons and annotated by a lifetime. Lifetimes \(l, m\) annotate every lexical block \(\{^{l}\, \overline{t}\}\). Lifetimes form a partial order \(l\succeq m\), which means that \(m\) is inside \(l\). This holds exactly when \(m\)’s block is lexically nested inside \(l\)’s, e.g., \(\{^{l}\, \{^{m}\, \overline{t}\}\}\). We note that modern Rust uses non-lexical lifetimes (NLL), which let a borrow end at its last use rather than at the enclosing block’s exit. FR’s lexical model admits a substantially simpler metatheory while capturing the essence of lifetimes and remaining sound.

The block’s lifetime is written after the opening brace, \(\{^{l}\, \overline{t}\}\), rather than after the closing brace as in [22] (i.e., \(\{\overline{t}\}^{l}\)). The two notations denote the same abstract syntax, but placing the lifetime up front makes it visible that the label is committed at block-entry rather than at block-exit. This matters for several typing rules in 4.2, which type body terms against the block’s ambient lifetime: the label must be fixed before the first body term is checked. It also matters for our partial syntax in 5, where a partial block whose tail is being emitted must already carry its lifetime.

4.1.0.3 Reference Values Encode Drop Responsibility

Reference values come in two flavors: an owning reference \(\ell^{\bullet}\) and a borrowed reference \(\ell^{\circ}\). Dropping an \(\ell^{\bullet}\) recursively drops the location it refers to, whereas dropping a \(\ell^{\circ}\) does not. Encoding this distinction at the value level keeps the operational semantics independent of the type system. By contrast, the distinction between shared and mutable references appears only in the type system, not at runtime. Both shared and mutable borrows therefore evaluate to \(\ell^{\circ}\) values, since they are non-owning references.

4.1.0.4 Borrow Types Name the Borrowed LVal

A reference type is either a shared borrow \(\mathtt{\&}\,w\) or a mutable borrow \(\mathtt{\&}\,\mathtt{mut}\,w\); we write \(\mathtt{\&}\,[\mathtt{mut}]\,w\) if either mode is allowed, where the target is a single lval (e.g., \(\mathtt{\&}\,x\)). Naming the borrowed lval directly in the type allows validating borrow safety by tracking overlaps and conflicts between borrowed and assigned lvals. In contrast to [22], we adopt FR’s follow-up work [35], restricting the \(w\) to a single lval instead of a set of lvals to establish cycle-freeness of borrows. This formulation is sufficient in the absence of conditionals.

4.1.0.5 Partial Types and Values Track Moved-Out Storage

At runtime, a partial value \(v^{\bot}\) extends \(v\) with the undefined marker \(\bot\), which marks a slot whose contents have been moved out. At the type level, a partial type \(\tilde{T}\) extends \(T\) with \(\square\,\tilde{T}\) (a box whose contents are themselves partial) and \(\lfloor T \rfloor\) (a slot moved out but with its former shape remembered, e.g., \(\lfloor \mathtt{\&}\,x \rfloor\), so re-assignment can be shape-checked). Every value is trivially a partial value, and every type a partial type. The converses fail because only the partial forms admit moved-out markers.

4.1.0.6 Source-Level Fragment

The reference values \(\ell^{\bullet}\) and \(\ell^{\circ}\) arise only at runtime, as the results of evaluating \(\mathtt{box}\) and borrow expressions; a programmer never writes them directly. We call a term source-level when no reference value appears as a subterm. The language does not require a distinguished surrounding block: a top-level program is any term typable from the empty environments at the root lifetime \(l_{\mathrm{root}}\). Blocks remain the construct that introduces nested lexical lifetimes.

None

4.2 Typing↩︎

8 presents the main typing rules of FR that we use in later sections. Next, we start by introducing the typing contexts and judgments, followed by the auxiliary functions, and then explain the rules. We close by stating FR’s type and borrow safety and summarizing our Lean mechanization.

4.2.0.1 Contexts and Judgments

Typing uses two contexts. The typing environment \(\Gamma\) maps each declared variable \(x\) to a slot type \(\langle \tilde{T} \rangle^{m}\), recording its partial type \(\tilde{T}\) and the lifetime \(m\) in which \(x\) was declared. The store typing \(\sigma\) assigns types to runtime locations. \(\sigma\) is needed only when typing intermediate execution states; source-level programs are typed under \(\sigma= \varnothing\).

The typing rules in 8 use one main judgment: \(\Gamma_1 \vdash \langle t: T\rangle^{l}_{\sigma} \dashv \Gamma_2\). It asserts that, in lifetime \(l\), the term \(t\) has type \(T\), and that evaluating \(t\) transforms the environment from \(\Gamma_1\) to \(\Gamma_2\). Threading the environment through the judgment in this input/output style makes the type system flow-sensitive. For example, after moving from an lval \(w\), the corresponding slot in \(\Gamma_2\) is marked moved out, so a subsequent use of \(w\) is rejected. Declarations and assignments similarly update the environment in a way that affects subsequent typing decisions. These effects cannot be captured by a traditional flow-insensitive type system, in which each variable has a single fixed type throughout its scope.

8 uses three auxiliary judgments only as premises of the main rules: LVal typing, type well-formedness, and shape compatibility. LVal typing, \(\Gamma\vdash w: \langle \tilde{T} \rangle^{m}\), determines the partial type of \(w\) and the lifetime \(m\) in which it can safely be used. Type well-formedness, \(\Gamma\vdash T\succeql\), holds when every borrow in \(T\) targets storage that outlives \(l\). Shape compatibility, \(\Gamma\vdash \tilde{T}_1 \sim\tilde{T}_2\), holds when two partial types agree in structural shape modulo lifetimes and undefined components, while still comparing the types beneath any undefined components. Each of these three has routine rules, so we defer to [22] for their full definition.

4.2.0.2 Auxiliary Functions

The typing rules also use FR’s standard auxiliary functions [22]. Each is defined by straightforward case analysis over its input so we summarize their roles rather than reproduce the full definitions. Several auxiliary predicates characterize accessibility. \(\mathrm{copy}(T)\) holds when \(T\) admits copy semantics. \(\mathrm{readProhibited}(\Gamma, w)\) holds when \(w\) is currently mutably borrowed in \(\Gamma\), whereas \(\mathrm{writeProhibited}(\Gamma, w)\) holds when it is borrowed in either mode. \(\mathrm{mut}(\Gamma, w)\) holds when \(w\) is mutably accessible: no dereference in \(w\) steps through an immutable borrow.

Three update functions modify the environment. \(\mathrm{move}(\Gamma, w)\) marks the value at \(w\) as moved out by replacing the corresponding component of its slot type with \(\lfloor T \rfloor\), where \(T\) is the component’s former type. \(\mathrm{write}^{0}(\Gamma, w, T)\) updates \(\Gamma\) to reflect assigning a value of type \(T\) through \(w\). \(\mathrm{drop}(\Gamma, m)\) removes all bindings declared in lifetime \(m\).

4.2.0.3 Typing Rules for Terms

Each rule in 8 types one corresponding term form from 7. T-Const checks literals and runtime values against \(\sigma\) and leaves the environment unchanged. T-Box assigns \(\mathtt{box}\;t\) the type \(\square\;T\) when \(t\) has type \(T\), while preserving any environment changes caused by evaluating \(t\). T-Copy and T-Move encode Rust’s familiar distinction between copy and move semantics. T-Copy permits copying an lval only when its type satisfies \(\mathrm{copy}\) and \(\mathrm{readProhibited}\) is false. T-Move returns the lval’s type, requires \(\mathrm{writeProhibited}\) to be false, and marks the corresponding component of its slot as moved out via \(\mathrm{move}\).

T-ImmBorrow and T-MutBorrow simulate Rust’s distinction between shared and mutable borrows, establishing their mutual exclusion. T-ImmBorrow creates a shared borrow only when \(w\) is not currently mutably borrows, i.e., \(\mathrm{readProhibited}(\Gamma,w)\) is false. This permits multiple shared borrows while excluding simultaneous mutable borrows. T-MutBorrow creates a mutable borrow only when \(w\) is not currently borrowed in any way, i.e., \(\mathrm{writeProhibited}(\Gamma,w)\) is false. This reflects Rust’s requirement that mutable access excludes any simultaneous borrows. Additionally, \(w\) must be mutable. The borrow expression itself leaves the environment unchanged. Its borrow information is recorded only when the resulting reference is stored through a declaration or assignment.

T-Seq threads the environment through a sequence of terms from left to right and gives the sequence the type of its last term. T-Block types \(\{^{m}\, \overline{t}\}\) in its own lifetime \(m\). Its result type must be well formed in the enclosing lifetime \(l\), which prevents borrows of block-local storage from escaping. After exiting the block, \(\mathrm{drop}\) removes any bindings declared in \(m\). The premise \(l\mathrel{\succeq{}_{\text{imm}}}m\), requiring \(m\) to be the immediate child of \(l\), corrects a missing assumption in FR’s typing that \(m\) is inside \(l\). We specify this as an immediate-child relationship, as one can always choose an immediate child \(m\) in place of any assigned \(m'\) inside \(l\).

T-Declare first types the initializer and then extends the resulting environment with a fresh binding \(x \mapsto \langle T \rangle^{l}\). The freshness check is made in the post-initializer environment \(\Gamma_2\), rather than in \(\Gamma_1\) by [22]: otherwise an initializer can redeclare \(x\) and return it to the environment before the outer declaration installs its binding. T-Assign types the right-hand side to obtain \(\Gamma_2\) and \(T_2\), then resolves the left-hand side in \(\Gamma_2\). The lval-typing environment \(\Gamma_2\) is another correction to FR’s typing, since evaluating the right-hand side may re-type the path under \(w\) (e.g., \(*p = \{p;mut\,w\}\) moves \(p\) out, thus making access to \(*p\) invalid). The rule then requires \(T_2\) to be shape-compatible with the destination’s stored partial type and well formed for the destination’s declaration lifetime \(m\), updates the environment via \(\mathrm{write}^{0}\), and requires \(\mathrm{writeProhibited}(\Gamma_3,w)\) to be false.

4.2.0.4 Type and Borrow Safety

[22] establish type and borrow safety for FR: a well-typed program does not get stuck, and if it terminates, it does so in a store that respects the borrow invariant, i.e., free of dangling or duplicated owning references and with at most one mutable borrow per location. We leverage this result to treat FR as a meaningful proxy for a usefully complex and expressive type system, motivating our choice of FR.

4.2.0.5 Mechanization and Corrections

We fully mechanize FR in Lean, including syntax, typing, operational semantics, and type and borrow safety proofs. In this process, we corrected the stated typing rules in several places. The main corrections to T-Block, T-Declare, and T-Assign are marked with grey boxes in 8. Beyond these typing adaptations, we correct the rules for unit values, align the runtime semantics with the reference implementation by [22], and strengthen the progress invariant with borrow safety and the linearizability property of [35]. We refer to our extended writeup alongside our mechanization.

5 Instantiating Generative Compilation on FR↩︎

In this section, we instantiate the generic framework of generative compilation (3) by defining a concrete sealor for FR. We deliberately make this sealor syntax-guided, keeping both its implementation and its proof lightweight, thereby making the approach easier to adopt for real languages. Despite this, we show that it is globally complete (5.3) and sound on an important class of partial programs (5.4). The developments in this section are fully mechanized in Lean.

5.1 Partial Syntax and Realization for FR↩︎

We first define FR’s partial syntax, which lays the basis for the sealor definition. It describes prefixes of syntactically valid FR programs. We then define realization, which relates a partial-syntax string to a full-syntax string obtained by extending the partial string. This relation is useful because completeness and soundness connect partial programs with their possible full programs.

5.1.0.1 Partial Syntax

We define partial syntax relative to FR’s full syntax in 7, focusing on source-level terms that may arise during autoregressive generation. 9 gives the resulting grammar of partial terms $ \(, which extends over a full term by allowing one of its parts to be only partially generated. The first two cases,\) $ and \(t\), respectively describe the two endpoints: no part of the current term has yet been generated, and generation has produced a full term. Each remaining production follows one term form from 7, replacing the component currently being generated with its partial counterpart. For example, $ $ denotes a partial value, and \(\mathtt{copy}\; \mathpalette\douwidehat{w}\) a copy term with a partial lval. \(\{^{l}\,\overline{t};\, \mathpalette\douwidehat{t}\) represents an unclosed block with a partial tail. The lifetime label \(l\) is an internal annotation, fixed once the opening brace is generated, rather than text generated by the model. The production $ $ covers both moves and assignments, which share a prefix until an \(=\) is generated.

Partial lvals $ $ and partial values $ $ complete the picture. They are not listed in 9 but are described in prose next. A partial lval is either $ \(, a full\)w$, a partially generated variable name $ $, or a dereference \(* \mathpalette\douwidehat{w}\) whose operand remains partial. A partial value $ $ is either a full value \(v\) or a partially generated integer constant; the unit value \(\varepsilon\) is always full.

For simplicity, we omit prefixes concerning only keywords, such as \(\mathtt{let\;mut}\), \(\mathtt{\&mut}\), or prefixes of either. Such prefixes contain no partially generated term, lval, or value for the sealor to preserve, so we fold them into the case of $ $.

5.1.0.2 Realization of Partial Programs

Realization models autoregressive generation: decoding may add text at the unfinished frontier, but cannot revise an earlier prefix. It differs from sealing, which may discard or alter unfinished fragments. This distinction will be made concrete once we introduce \(\mathcal{S}_{\text{FR}}\). Our completeness result presented later in this section connects these two notions.

We write $ $ when \(t\) realizes $ $, and define this relation case by case in [fig:realizes]. In most cases, realization retains the term form already determined by the generated prefix and recurses on its unfinished subterm. The two clauses for $ $ make its Move/Assignment ambiguity explicit: once $ $ realizes an lval \(w\), the term may realize either the move \(w\) or an assignment \(w= t\) with any right-hand side \(t\). For lvals, the relation $ $ has four cases: $ $ for any \(w\); \(w\rightsquigarroww\); $ x$ when $ $ is a prefix of \(x\); and \(* \mathpalette\douwidehat{w}\rightsquigarrow*w\) when $ $.

5.2 \(\mathcal{S}_{\text{FR}}\): A Syntax-Guided Sealor for FR↩︎

10 defines our syntax-guided sealor \(\mathcal{S}_{\text{FR}}\) by case analysis over partial syntax. It maps each partial term form to a full FR term. As required by the generic definition, \(\mathcal{S}_{\text{FR}}\) is total. Prefixes outside the partial syntax are handled separately by returning them unchanged, so that the underlying compiler may report a syntax error.

At a high level, \(\mathcal{S}_{\text{FR}}\) abstracts type checking through a syntax-guided transformation. Rather than deciding exactly whether a partial term admits a well-typed completion, it constructs a term whose well-typedness is necessary for that of every possible completion, thereby preserving completeness. Accordingly, sealing preserves generated structure when it exposes useful typing obligations, while abstracting away other obligations when they require information not yet generated or analysis beyond syntax. Several cases therefore seal directly to \({\varepsilon}\): \(\mathtt{copy}\; \mathpalette\douwidehat{w}\), $ \(,\),[]; \(, and\);; $. Their unfinished components must be resolved before the corresponding typing rules can establish useful premises. Here, \({\varepsilon}\) provides a well-typed placeholder with no additional typing obligations. Moreover, for \(\mathtt{let}\;\mathtt{mut}\;x = \mathpalette\douwidehat{t}\) and \(w= \mathpalette\douwidehat{t}\), \(\mathcal{S}_{\text{FR}}\) recurses only on $ $. It drops the enclosing declaration or assignment, including the declared variable \(x\) or assigned lval \(w\), and hence their associated typing obligations.

This abstraction is deliberately not maximally aggressive. With completeness preserved, we seek to retain as much soundness as possible. Fully generated terms are therefore unchanged, including both a standalone \(t\) and all already-full terms \(\overline{t}\) inside an unclosed block. Furthermore, \(\mathcal{S}_{\text{FR}}\) preserves partial subterms that can themselves contain generated structure relevant to later typing, rather than discarding them outright. Thus, it recurses on $ $ in \(\mathtt{box}\; \mathpalette\douwidehat{t}\), \(\{^{l}\,\overline{t};\, \mathpalette\douwidehat{t}\), \(\mathtt{let}\;\mathtt{mut}\;x = \mathpalette\douwidehat{t}\), and \(w= \mathpalette\douwidehat{t}\). At the same time, we do not make \(\mathcal{S}_{\text{FR}}\) more sound at the cost of a lightweight design. For instance, in \(\mathtt{let}\;\mathtt{mut}\;x = \mathpalette\douwidehat{t}\) or \(w= \mathpalette\douwidehat{t}\), one could use the type of \(x\) or \(w\) to further constrain $ $. We do not pursue this in \(\mathcal{S}_{\text{FR}}\), because it would require typing information beyond our syntax-guided design. This would add implementation cost without substantial benefit, since \(\mathcal{S}_{\text{FR}}\) is already sound on an important class of programs, as we show in 5.4.

A few remaining cases complete the definition. $ $ seals to \({\varepsilon}\), since either no part of the current term has been generated or the generated prefix consists only of keywords. An unfinished partial value $ $ also seals to \({\varepsilon}\). Although a partially generated integer already suggests type \(\mathtt{int}\), we choose this simpler syntax-guided rule rather than recover that information, at a small cost to soundness. The bare $ $ production likewise seals to \({\varepsilon}\): before an \(=\) is generated, it remains ambiguous between a move and the left-hand side of an assignment, and sealing it as either would prematurely commit to one interpretation. Finally, for \(\{^{l}\,\overline{t};\, \mathpalette\douwidehat{t}\), the sealor appends a trailing \({\varepsilon}\) and the closing brace after sealing $ $, ensuring that the result is a closed block.

5.3 Global Completeness of \(\mathcal{S}_{\text{FR}}\)↩︎

\(\mathcal{S}_{\text{FR}}\)’s design was motivated by global completeness, which we formally prove next. We first show that whenever a partial term realizes a well-typed full term, sealing the partial term with \(\mathcal{S}_{\text{FR}}\) also yields a well-typed term.

The proof follows 9 row by row, in order, naming each case after that row’s description.

Let \(L_{\text{FR}}\) denote the set of well-typed top-level FR terms. As discussed in 4, FR’s top-level terms are typed under the root lifetime \(l_{\mathrm{root}}\), empty typing environment, and empty store typing. That is, \(L_{\text{FR}}:= \{\, t\mid \exists T, \Gamma.\;\varnothing\vdash \langle t: T\rangle^{l_{\mathrm{root}}}_{\varnothing} \dashv \Gamma\,\}\). 2 is stronger than the top-level result we ultimately need: it permits arbitrary initial typing environments and store typings, as well as lifetime. This allows the proof to apply to intermediate terms within larger programs. Specializing it to top-level typing yields completeness for top-level partial syntax.

The generic framework defines global completeness over arbitrary strings rather than partial-syntax terms, so we finally lift 1 to that setting.

Finally, based on 1, the global completeness of the corresponding generative compiler \(\mathcal{G}_{\text{FR}}(s) \coloneq \mathcal{C}_{\text{FR}}(\mathcal{S}_{\text{FR}}(s))\) follows from that of \(\mathcal{S}_{\text{FR}}\) and an exact compiler \(\mathcal{C}_{\text{FR}}\) for FR.

5.4 Selective Soundness of \(\mathcal{S}_{\text{FR}}\)↩︎

While \(\mathcal{S}_{\text{FR}}\) achieves global completeness, it also abstracts away information that soundness would need in order to remain lightweight and syntax-guided. For instance, \(\mathcal{S}_{\text{FR}}(\mathtt{copy}\; \mathpalette\douwidehat{x}) = {\varepsilon}\) is accepted unconditionally, even when $ $ can only realize a moved-out variable. We nevertheless identify an important class on which \(\mathcal{S}_{\text{FR}}\) is sound: statement boundaries, where generation has finished one or more complete statements in a block and is about to begin the next. This is a useful guarantee in practice because statement boundaries occur frequently during generation.

We now give formal characterizations of this property. We call $ $ a statement boundary if $ = {^{l}, ;, \(. That is, after a series of full terms in a block, the model is exactly at the point immediately after a semicolon, before any token of what follows has streamed in. Let\)_{} {, {^{l}, ;, , ;l ,}$, i.e., the class of statement boundaries.

As with 2, 4 is stronger than the top-level result we need. Specializing it yields selective soundness at top level.

We lift 2 from partial-syntax terms to arbitrary strings.

Finally, based on 3 and 5, \(\mathcal{S}_{\text{FR}}\) is exact at statement boundaries. So is \(\mathcal{G}_{\text{FR}}\) according to 1.

6 From FR to Real Rust↩︎

We now carry the methodology of 5 from FR to real Rust by presenting our Rust sealor, \(\mathcal{S}_{\text{RS}}\).

6.0.0.1 Inherited from FR

We design \(\mathcal{S}_{\text{RS}}\) following the same principles as FR’s sealor \(\mathcal{S}_{\text{FR}}\) (5.2). It remains lightweight and syntax-guided in most cases, discards typing obligations when needed for completeness, and adds targeted analysis where doing so improves soundness. It preserves already-generated structure verbatim and recurses on the still-partial frontier. As with \(\mathcal{S}_{\text{FR}}\), the goal is global completeness together with selective soundness.

For each Rust feature, we describe its syntactic shape, the partial forms the sealor may encounter, and the sealor rules used to close those partial forms. For readability, we reuse FR’s notation where applicable and introduce new notation only for constructs specific to Rust.

6.0.0.2 Not Inherited from FR

Two aspects of this section depart from 5. First, Rust is much larger than FR. The Rust sealor must therefore handle constructs with no FR counterpart, as well as constructs that resemble FR but differ in syntactic structure or typing behavior. We discuss a representative selection of such features across this section. Second, we give informal, per-feature arguments for typing behavior, completeness, and soundness, rather than the formal, mechanized treatment we gave for the whole FR. This is because our goal for this section is to directly capture the behaviors of rustc, the Rust compiler. Using an existing Rust formalization as an intermediate target would make correctness depend on that formalization’s faithfulness to rustc, rather than on rustc directly, which is especially undesirable as Rust continues to evolve. The global completeness argument follows the same structure as 5.3: as long as each sealor case is complete with respect to the corresponding rustc behavior, the entire sealor and the generative compiler are complete.

6.1 General Design Choices for Rust↩︎

We describe design choices recurring across Rust’s features, before per-feature treatment in 6.2.

6.1.0.1 Sealors \(\mathcal{S}_{\text{RS}}^s\) and \(\mathcal{S}_{\text{RS}}^e\)

Since Rust distinguishes statements and expressions, we introduce two sealors: a statement sealor \(\mathcal{S}_{\text{RS}}^s\) that seals a partial statement (possibly an expression statement) into a list of statements, and an expression sealor \(\mathcal{S}_{\text{RS}}^e\) that seals a partial expression into an expression with an unconstrained type. When an expression is desired, and its type can be inferred from context, the expression sealor is used. In all other cases, we use the statement sealor.

6.1.0.2 Placeholders \(\mathtt{hole}_\mathtt{div}()\) and \(\mathtt{hole}_\mathtt{val}()\)

FR’s sealor closes every abstracted case with the single unit placeholder \({\varepsilon}\), since FR’s control-flow-free terms leave no other typing obligation to discharge. rustc’s typing rules for branching and looping constructs additionally require reasoning about multiple control-flow paths, e.g., that both branches of an \(\mathtt{if}\) agree, or that a loop body’s effects are consistent across iterations. To seal such constructs conveniently, we introduce two placeholders with deliberately different typing behavior.

The first placeholder, \(\mathtt{hole}_\mathtt{div}()\), is simply \(\mathtt{panic!}()\) in our implementation. Statically, \(\mathtt{panic!}()\) has type \(!\), the never type, whose expressions can be coerced to any expected type. It diverges: executing it never returns normally. Because the continuation after a divergent expression is unreachable, rustc does not require it to satisfy the usual borrow-checking obligations. This helps preserve completeness; otherwise rustc might report borrow errors caused only by an intermediate partial state, such as a variable being moved out before later generated code would reinitialize it. This makes \(\mathtt{hole}_\mathtt{div}()\) useful for sealing control flow branches that should not produce a value.

The second, \(\mathtt{hole}_\mathtt{val}()\), instead behaves as if it produces a well-typed value without diverging. We implement it as a call to a generic helper function: \(\mathtt{const}\;\mathtt{fn}\;\mathtt{hole}_\mathtt{val}(){}\textrm{<}T\textrm{>}() \rightarrow T \;\{\;\mathtt{panic!}()\;\}\). The function body diverges at run time, but this divergence is not exposed at the call site. The call expression \(\mathtt{hole}_\mathtt{val}()\) has the declared return type \(T\), not the body type \(!\). The type parameter \(T\) is instead resolved by type inference from the surrounding context. Thus, \(\mathtt{hole}_\mathtt{val}()\) can instantiate to any expected type in the surrounding code while keeping the borrow checker enabled.

A more subtle reason not to use \(\mathtt{hole}_\mathtt{div}()\) as the expression placeholder is Rust’s fallback for the never type. When type inference is underconstrained, \(!\) may fall back to the unit type \(()\), causing spurious type or trait mismatch errors. The type parameter \(T\) in \(\mathtt{hole}_\mathtt{val}()\) does not undergo this fallback, making it a safe choice when sealed code must supply an expression value.

6.1.0.3 Suppressing Future-Dependent Errors During Generation

Sealing Rust sometimes requires treating rustc errors more carefully than a simple accept-or-reject verdict. This is not a peculiarity of our sealor, but a consequence of Rust features whose well-typedness can depend on code generated later. For example, a partial trait implementation may not yet contain all required methods, a call may refer to a function item declared later in the file, and an expression may have an ambiguous type that is resolved only by a subsequent use. Such errors are required to be suppressed for completeness. Otherwise the sealed program could be rejected even though the missing suffix would make the final program well-typed. To limit the impact on soundness, we suppress errors only in the scope where necessary. For instance, “missing trait items” is suppressed only if it occurs inside the sealing of partial trait implementations and “type annotations needed” errors only inside the sealing of partial function bodies. When we arrive at a fully generated program after the \(\mathsf{EOS}\) token, we clean out all suppressed errors, such that rustc could catch all errors.

6.1.0.4 Projecting Error Messages on Partial Programs

Since rustc checks the sealed program \(\mathcal{S}_{\text{RS}}(c)\) rather than the original partial program \(c\), its diagnostics refer to \(\mathcal{S}_{\text{RS}}(c)\). Feeding these diagnostics directly to the model can be confusing, because \(\mathcal{S}_{\text{RS}}(c)\) may differ from \(c\), as in 4 5. We therefore project diagnostics from \(\mathcal{S}_{\text{RS}}(c)\) back to \(c\). During sealing, we maintain a positional map of code copied verbatim from \(c\) into \(\mathcal{S}_{\text{RS}}(c)\). We then re-render rustc’s diagnostics using \(c\) as the reference code, mapping the locations of diagnostic highlights from \(\mathcal{S}_{\text{RS}}(c)\) back into \(c\). Inserted code such as \(\mathtt{hole}_\mathtt{val}(){}\) has no source in \(c\); diagnostics arising only from such code are suppressed by the module described above.

6.2 \(\mathcal{S}_{\text{RS}}\): Our Sealor for Rust↩︎

We now introduce the Rust sealor rules for expression and statement forms.

6.2.0.1 Blocks

A block in Rust, denoted \(b\), consists of a sequence of statements \(\overline{s}\), optionally terminated by an expression \(e\). That is, \(b::= \{\, \overline{s};\, e^? \}\). A block is itself an expression, so it may appear wherever an expression is expected. A block creates a lexical scope for bindings: variables defined inside are not visible outside, and owned values are dropped at the end unless moved earlier. The type of a block is the type of its tail expression, or the unit type if there isn’t one. Independently of that, a block diverges if any of its statements or tail expression diverges. A block may end with a partial expression or statement. Both are sealed identically:

The block sealors preserve the full statements \(\overline{s}\) and seal the partial component with \(\mathcal{S}_{\text{RS}}^s\). The statement sealor then appends \(\mathtt{hole}_\mathtt{div}()\), making the sealed block diverge to stop the control-flow path (more on this later in this section when we discuss conditionals and loops). The expression sealor instead appends \(\mathtt{hole}_\mathtt{val}()\), so the block produces a value of the type expected by its context.

Completeness follows from two facts. First, preserving the completed statements \(\overline{s}\) and recursively sealing the partial component (\(\mathcal{S}_{\text{RS}}^s( \mathpalette\douwidehat{s})\)) mirrors FR’s completeness argument for unclosed blocks (5.3). That is, each piece is checked in exactly the environment it would occupy in any well-typed completion. Second, the trailing placeholder never introduces a new failure: \(\mathtt{hole}_\mathtt{div}()\) and \(\mathtt{hole}_\mathtt{val}()\) type check against any expected type, so appending them cannot make an otherwise completable block fail to type check. For soundness, we preserve all of rustc’s checking on \(\overline{s}\) and on the recursively sealed partial form, so any uncompletable prefix that fails these checks is rejected.

6.2.0.2 Fallback Sealors

For every feature discussed next, we present a bespoke statement sealor \(\mathcal{S}_{\text{RS}}^s\). We do not need a separate expression sealor \(\mathcal{S}_{\text{RS}}^e\), since we automatically derive one from \(\mathcal{S}_{\text{RS}}^s\) via \(\mathcal{S}_{\text{RS}}^e( \mathpalette\douwidehat{e}) \coloneq \{\, \mathcal{S}_{\text{RS}}^s( \mathpalette\douwidehat{e});\, \mathtt{hole}_\mathtt{val}()\, \}\). This turns any sealing of $ $ from a list of statements into an expression that produces a value of the expected type. Both completeness and soundness of this derivation are inherited directly from \(\mathcal{S}_{\text{RS}}^s\): appending \(\mathtt{hole}_\mathtt{val}()\) neither introduces nor discards any typing obligation, since \(\mathtt{hole}_\mathtt{val}()\) type checks against any expected type.

When a construct has no specific rule for \(\mathcal{S}_{\text{RS}}^s( \mathpalette\douwidehat{s})\), we fall back to \(\mathcal{S}_{\text{RS}}^s( \mathpalette\douwidehat{s}) \coloneq ()\). This discards the partial statement, preserving completeness by removing its typing obligations. Soundness may be lost temporarily, but is recovered once the statement is fully generated and copied verbatim.

6.2.0.3 Conditionals

Conditionals in Rust are expressions: the condition is an expression, and the branches are blocks; chaining multiple conditions with \(\mathtt{else\;if}\) is allowed. That is, \(e_\mathtt{if} ::= \mathtt{if}\;e\;b\mathbin{|} \mathtt{if}\;e\;b\;\mathtt{else}\;b\mathbin{|} \mathtt{if}\;e\;b\;\mathtt{else}\;e_\mathtt{if}\). rustc type checks the condition against \(\mathtt{bool}\), then type checks each branch and merges the two states after them. When an \(\mathtt{else\;if}\) chain is nested, the two-way merge applies recursively from the innermost pair outward. A branch that diverges contributes nothing to the merge: its result type and borrow state at the join point are unobservable, so the result type and the borrow state after the \(\mathtt{if}\) are entirely determined by the live branch.

A partial component may appear inside the condition, inside the then-branch, or inside the else-branch. That is, $ ::= ; ;e; ;e;b;; ;e;b;; $. We close the missing branch with \(\mathtt{hole}_\mathtt{div}()\), so that it is diverging and the whole \(\mathtt{if}\) is well-typed against the live side alone. The statement sealor \(\mathcal{S}_{\text{RS}}^s\) for $ $ is defined below:

A partial \(\mathtt{else\;if}\) condition is sealed as an \(\mathtt{else}\) body, closed with \(\mathtt{hole}_\mathtt{div}()\) just like the missing branch itself. Once the condition becomes full, we instead recurse via \(\mathcal{S}_{\text{RS}}^s\) on the remaining \(\mathtt{if}\;e_1 \ldots\) as a fresh partial \(\mathtt{if}\).

Our sealor is complete for conditionals. Every partial component we recurse on inherits completeness from the inductive hypothesis on branch blocks and boolean conditions. Although we do not separately discuss boolean conditions in detail, the completeness of sealing them should be easy to achieve. The only other addition, \(\mathtt{hole}_\mathtt{div}()\), never introduces new obligations: since it diverges, rustc excludes it from the branch-type merge, so it cannot constrain what the live side must satisfy. For soundness, we preserve all of Rust’s checking up to the partial form, so any uncompletable prefix that fails one of these checks is still rejected.

6.2.0.4 While Loops

A Rust \(\mathtt{while}\) loop consists of a condition and a body block. That is, \(e_\mathtt{while} ::= \mathtt{while}\;e\;b\). A well-typed \(\mathtt{while}\) loop requires that the loop body be well-typed as if it were executed any number of times. Informally, the borrow and initialization state after one iteration must be compatible with the state at the start of the next. Moving out of a variable in a loop body without reinitialization is rejected, as the second iteration would read a moved-out slot. Rust waives this obligation when the body diverges, because control never reaches a second iteration.

Either the condition or the body may be partial, i.e., $ ::= ; ;e; \(. We force a partial body to diverge by appending\)_()$ via \(\mathcal{S}_{\text{RS}}^s( \mathpalette\douwidehat{b})\), eliminating the “carries over between iterations” obligation while still checking everything on the already-generated first iteration.

The other loop forms in Rust (\(\mathtt{for}\), unbounded \(\mathtt{loop}\)) are handled analogously. For completeness, the condition case is similar to \(\mathtt{if}\). For the body case, the sealed body diverges by construction, so rustc does not enforce the second-iteration consistency check, and the first-iteration prefix (the condition and the completed body prefix \(\overline{s}\)) is checked against exactly the same environment it would occupy in any well-typed completion. For soundness, we do not lose anything more than what is lost in the partial term in the loop body, as the realization of $ $ can also diverge.

6.2.0.5 Function Calls

A function call consists of a callee and zero or more arguments. That is, \(e_\mathtt{call} ::= e(\overline{e})\). At a call site \(e_0(e_1, \ldots, e_n)\), rustc resolves \(e_0\) to a signature, then type checks the arguments left-to-right, threading each argument’s move/borrow effects into the environment used to check the next. The number of arguments must equal the declared arity.

A partial call has zero or more completed arguments followed by one partial argument. That is, $ ::= e(, $. If the callee is still partial, sealing reduces to handling whatever partial expression the callee is via its own rule, so we do not specifically discuss this case here. Our sealor first queries rustc as an arity oracle: we invoke it on a sealing where \(e_0\) is called with no arguments and inspect its type. Once the arity \(n\) is known, we pad with \(\mathtt{hole}_\mathtt{val}()\) for the missing arguments: via \(\mathcal{S}_{\text{RS}}^e\) for the partial argument, and directly for the ones not at all present in $ $.

For completeness, our sealor places each completed argument \(e_i\) in exactly the same environment it would occupy in any well-typed completion (arguments before it are the same; then the partial argument is sealed, and arguments after it are \(\mathtt{hole}_\mathtt{val}()\), which is generic and produces no effect on the environment). This covers the case \(k < n\), i.e., fewer arguments have been generated so far than the callee accepts. If instead \(k \geq n\), the prefix already has more arguments than the callee’s arity, our sealor still copies all of them rather than truncating, so rustc rejects the sealed call with a genuine arity mismatch. This is not a false rejection, since no well-typed completion can exist once too many arguments have already been committed. For soundness, we preserve rustc’s checking of the callee \(e_0\) and the completed arguments \(e_1, \ldots, e_k\) exactly as it would occur in the real program, so any type or borrow error among them is still caught.

6.2.0.6 Field Accesses

A field access has the form \(e.f\), where \(e\) is an expression of record (or reference-to-record) type and \(f\) is an identifier naming one of its fields. That is, \(e_\mathtt{field} ::= e.f\). Field accesses are lvals, so they participate in move, copy, borrow, and assignment on the same footing as variables.

The partial syntax rule is $ ::= e. $. In other words, the receiver is completed but the field has been cut off mid-token. For \(e. \mathpalette\douwidehat{f}\), we only copy the receiver. We take a reference to avoid moving out of \(e\). This is necessary because the completion may be a method invocation (either on \(e\) itself or on a field) that takes \(\mathtt{self}\) by reference. That is, \(\mathcal{S}_{\text{RS}}^s(e. \mathpalette \sbox 0{\m@th f\widehat{\hphantom{)}}} \sbox 2{\m@th fx} \sbox 4{\m@th f)} \dimen 0=\ht 0 \advance\dimen 0 -.57\ht 2 \dimen 2=\dp 4 \rlap{ \raisebox{\dimexpr\dimen 0-\dimen 2}{ \makebox[\wd 4][c]{\scalebox{0.75}[-1]{\box 0}} } } {)} = \&e\).

For completeness, the receiver of any partial field access is a strict sub-prefix of every completion, so the receiver is well-typed if the completion is well-typed. In terms of borrow checking, we need to suppress E0382 (borrow of moved value) because fields of the receiver (other than the one accessed) could be uninitialized. Suppressing E0382 means we do not check if the field (or the whole record) is initialized until later. For soundness, we preserve the type and borrow-checking of the receiver in all cases. We do not attempt to check whether truncated identifiers can be extended to a real field of the receiver’s type, as this goes beyond our syntax-guided design. Instead, we wait until the field becomes full.

6.2.0.7 Other Expressions and Top-Level Items

We briefly summarize the remaining Rust constructs. Aggregate literals, including tuples \((\overline{e})\), arrays \([\overline{e}]\), and record expressions \(S\{\overline{f:e}\}\), are sealed by recursing on the trailing partial element with \(\mathcal{S}_{\text{RS}}^e\) and then closing the aggregate. For record expressions, we suppress E0063 (missing field initializers). This preserves completeness because already generated elements are checked in order, while missing fields may still be supplied later; soundness is preserved for the fully generated elements.

Closure expressions are sealed by sealing the body as an expression, using \(\mathtt{hole}_\mathtt{val}()\) to close value-producing positions. Closures with partial signatures are skipped until the signature is complete, which delays checking of parameter types. Other expression forms, including unary expressions, \(\mathtt{return}\), condition-local \(\mathtt{let}\), parenthesized expressions, \(\mathtt{try}\), ranges, indexing, and casts, are handled uniformly: the sealor preserves fully generated components and recurses into the partial one. Constructs without a bespoke expression rule use the fallback sealor described above.

Top-level items are handled similarly. Function bodies are sealed like closure bodies. Item-containing constructs, such as module definitions and impl blocks, preserve the enclosing definition and all fully generated sub-items, then recursively seal the partial item at the frontier. For constructs without bespoke rules, including type definitions, type aliases, constants, statics, extern blocks, global asm!, and macros, fully generated instances are preserved verbatim, while partial instances are discarded until enough syntax has been generated for a more specific rule to apply.

6.2.0.8 Example Revisited

Three rules seal the partial program in 4 into the full program in 5. First, the function body is an unclosed block ending in the partial statement \(\mathtt{let}\;\mathtt{prio} = \mathtt{tag}. \mathpalette\douwidehat{f}\), so the block rule appends \(\mathtt{hole}_\mathtt{val}()\): \(\mathcal{S}_{\text{RS}}^e( \mathpalette\douwidehat{b}) = \{\, \overline{s}; \mathcal{S}_{\text{RS}}^s( \mathpalette\douwidehat{s});\, \mathtt{hole}_\mathtt{val}()\,\}\). Second, like the FR sealor (5.2), the \(\mathtt{let}\) rule drops the left-hand side and recurses on the partial right-hand side: \(\mathcal{S}_{\text{RS}}^s(\mathtt{let}\;\mathtt{prio} = \mathtt{tag}. \mathpalette\douwidehat{f}) = \mathcal{S}_{\text{RS}}^s(\mathtt{tag}. \mathpalette\douwidehat{f})\). Finally, the field-access rule closes the partial access as \(\&\mathtt{tag}\).

7 Experimental Evaluation↩︎

In this section, we experimentally evaluate our generative compilation approach. We focus on two core research questions: (R1) Can our generative compilation effectively support code generation? and (R2) What are observable effects of generative compilation?

7.1 Experimental Setup↩︎

7.1.0.1 Models and Agent Harness

We evaluate seven recent coding models. The three frontier black-box models, Claude Opus 4.8 [36], GPT 5.3 Codex [37], and Gemini 3.5 Flash [38], come from major model providers and are explicitly advertised for coding. We also include four strong open-weight models, Kimi K2.7 Code [39], GLM 5.2 [40], and two models from the Qwen 3.5 family, a large 397B-parameter model and a smaller 9B-parameter model [41]. This selection spans a broad range of model categories and capabilities. We evaluate each model twice on every task, sampling with temperature \(0.6\) whenever the provider permits configuring it.

We use an agent harness with fixed control flow, similar in style to Agentless [42], to isolate the effect of feedback and enable a clean comparison. The model generates files or structured edits, while the harness deterministically writes them to disk, runs fixed compilation commands, and feeds any diagnostics back into the next prompt.

7.1.0.2 Tasks and Benchmarks

We evaluate two repository-level tasks for which Rust compiler errors occur frequently. Both tasks require filling a Rust skeleton that defines struct and function signatures. We report two end-to-end metrics: compiler error rate and functional correctness. Compiler error rate is the fraction of generated outputs for which the Rust compiler reports at least one error diagnostic. Functional correctness is the fraction of generations that pass the task’s unit tests. To better understand the results, we also measure runtime, the number of diagnostics in each compiler-feedback report, whether errors are detected during generation, and how far detected errors are from their original locations. We list prompts for both tasks in 13.

The first task, denoted Translation, is based on CRUST-Bench [8], a benchmark for C-to-Rust translation. Translation is based on a subset of 20 complex instances from CRUST-Bench. The model is given the C implementation of a library and is tasked to translate it into Rust. We ask the model to translate each C file at a time, such that it uses the specified interfaces. C to Rust translation is an important topic, as Rust is considered a more memory-safe and similarly performant alternative to C. At the same time, large translations are challenging: the model must translate C data structures consistently and adapt them to Rust interfaces across files.

The second task, denoted UpdatedAPI, evaluates whether models can adapt to changed Rust library APIs. Each instance asks the model to implement a small command-line utility that requires using a recently updated API function. This setting is relevant because LLMs always have fixed training knowledge cutoffs and may therefore generate code against deprecated APIs. The benchmark tests whether the model can use compiler feedback about the changed API to repair its generation. We provide details about benchmark construction in 11.

7.1.0.3 Comparison

We compare three approaches. The first, LLM, samples directly from the LLM without compiler feedback. The second, denoted PC for short, adds standard post-generation compiler feedback: after each generated solution, the compiler is run, and any diagnostics are fed back to the model. If compilation fails, the model may either edit its previous output or regenerate a new solution from scratch. This process may repeat up to \(n\) times. The third approach, denoted GC, further incorporates on-the-fly feedback enabled by generative compilation (6). This tests whether generative compilation can improve over post-generation feedback by detecting errors early. During generation, generative compilation may detect compiler errors on partial outputs and restart generation, up to \(k\) times. If the model has not produced a valid output after these \(k\) restarts, we allow it to finish generating a full output and then apply up to \(n-k\) iterations of post-generation compiler feedback. In our experiments, we set \(n=15\) in UpdatedAPI and \(n=20\) on Translation, and \(k=10\) in both settings. We ablate over the budget choices in 11.5.

Note that we cannot experimentally compare against constrained decoding because, to our knowledge, no constrained decoding implementation exists for Rust. Although our approach can check partial programs, it is not suitable for constrained decoding. This is because our approach guarantees global completeness, whereas constrained decoding requires global soundness, as discussed at the end of 3.1. Building a constrained decoder from scratch for real Rust would be highly complex and costly, as discussed in 2. This contrast highlights a key benefit of generative compilation: it is lightweight to implement and largely reuses existing compiler infrastructure.

7.1.0.4 Implementation Details

Our sealor is implemented in about 5k lines of Rust, which is orders of magnitude less than the \(\sim\)​600k lines in Rust’s compiler frontend [24]. It parses partial Rust code using rust-analyzer [43], synthesizes sealed programs using the rules outlined in 6, and queries rustc for compiler feedback. We apply minimal patches to rust-analyzer to improve its handling of partial ASTs. The LLM-facing layer comprises about 3k lines of Python: it streams candidate tokens, invokes the sealor and the Rust compiler through bindings, and implements the logic in 6. For robustness, the implementation is covered by 329 Rust and Python tests spanning the sealor and inference behavior. Finally, we include wrappers for different LLM inference APIs, evaluated datasets, and inference and evaluation orchestration comprising another 8k lines of Python code.

4pt

7.2 Benefits for End-to-End Code Generation↩︎

We integrate our method into the code generation pipeline and measure its benefits, answering R1.

7.2.0.1 Reduced Compiler Errors and Improved Functional Correctness

As shown in 1, LLM produces non-compilable outputs in up to \(90.0\%\) of cases. Post-generation compiler feedback (PC) reduces the average compiler error rate from \(65.9\%\) to \(20.7\%\), highlighting the strong repair capabilities of state-of-the-art LLMs. Even so, adding on-the-fly feedback with GC reduces the error rate further to \(13.1\%\). Across all 14 model-dataset configurations, GC achieves a better compiler error rate than PC and one tie; in 9 of the configurations, the improvement over PC is statistically significant. Notably, GC eliminates compiler errors entirely for Opus 4.8 on UpdatedAPI (\(0.0\%\) vs.\(6.7\%\) with PC) and reduces them from \(13.3\%\) to \(3.3\%\) for GPT 5.3 Codex.

Reductions in compiler errors also transfer to improving functional correctness. GC attains the best functional correctness in 11 of the 14 model-dataset configurations. The largest improvements are visible on UpdatedAPI for GLM 5.2 (from \(53.3\%\) with PC to \(71.7\%\) with GC) and on Translation for Kimi K2.7(from \(39.9\%\) to \(53.9\%\), respectively).

7.2.0.2 Decreased Runtime

Despite intervening during generation, GC decreases overall runtime. The average overhead over LLM drops from \(233\) seconds (\(+283\%\)) with PC to \(135\) seconds (\(+170\%\)) with GC. This reduction is driven by models that require many feedback rounds, namely Gemini 3.5 Flash and the Qwen 3.5 models. For Qwen 9B, GC more than halves the average runtime on both datasets; for example, on Translation, runtime drops from on average \(879\) to \(357\) seconds per sample. By interrupting generation at the first unrecoverable error, GC avoids repeatedly completing files that cannot compile. For Opus 4.8, and Kimi K2.7, which require on-the-fly feedback less frequently, runtime remains essentially unchanged, increasing by \(2\) seconds (\(+6\%\)) for former, and decreasing \(11\) seconds (\(-6\%\)) for the latter.

7.3 Analysis: What Effects Does Generative Compilation Have?↩︎

7.3.0.1 Mitigated Error Snowballs

Looking more closely at GC, we find that most errors are resolved during the early-feedback phase, i.e., within the first \(k=10\) restarts. Overall, \(85.3\%\) of tasks complete without ever switching back to post-generation compiler feedback, and \(55.4\%\) of all tasks are solved correctly within the early-feedback phase. Weaker models require more restart: Qwen 9B takes more than 10 restarts in \(40.9\%\) of tasks and Qwen 397B on \(20.5\%\), compared to only \(2.1\%\) for GPT 5.3 Codex. We attribute this partly to weaker models unfamiliarity with the early compiler-feedback format; in particular, they often regenerate the same erroneous prefix.

Generative compilation also makes error reports smaller and more focused. When a completed file is compiled, one core mistake can cascade into many follow-on diagnostics. By interrupting generation at the first unrecoverable mistake, GC instead surfaces a reduced set of diagnostics that focuses on the root cause. As shown in 11 (a), \(65\%\) of GC error reports contain only one or two distinct diagnostics, with an average of \(5.5\) diagnostics per message. In contrast, only \(40\%\) of PC reports are this succinct, averaging \(13.8\) diagnostics and, on Translation, sometimes reaching several hundred. This reduction gives the model a smaller and more targeted repair signal, reducing the burden of locating the relevant error within its context.

7.3.0.2 Reporting Errors Close to Their Source

To further assess the quality of GC’s error detection, we measure how early it surfaces errors during generation. For each of the \(961\) erroneous files generated by LLM and included in this analysis, we record the location of the first compiler error returned by rustc in the completed program. We then replay the same file prefix by prefix against GC and record where GC first reports an error. The replay feeds each file verbatim at 50 tokens per second, a typical decoding speed for current frontier coding models¹, while running GC in parallel without asking the model to repair errors.

Oracle denotes the primary span of the first compiler error reported on the completed file. This span is a lower bound on the earliest possible detection point for that error, but is generally not achievable from a prefix alone: a prefix ending at the span may still admit a valid completion, for example if the error refers to an item that could be defined later. We compare this oracle span with those reported by GC. We also compare against two baselines: GC\(^{\mathsf{fn}}\), a simpler variant that checks only completed function bodies, and PC, which reports compiler feedback only after the full file has been generated.

In the median case, GC reports the error only \(3\) lines after the primary span of the eventual compiler error, and in a quarter of all cases it reports the error exactly at that span. By contrast, GC\(^{\mathsf{fn}}\) and PC report errors much later, with median delays of \(14\) and \(89\) lines after Oracle, respectively, as shown in 11 (b). The delay distribution for GC is heavy-tailed, with a mean of \(27.7\) lines. This is expected: our configuration deliberately tolerates references to not-yet-defined items, as they may legitimately be introduced later in the file. Errors involving such items are therefore reported only once such a later definition is ruled out, e.g., when the model signals the end of file generation. Indeed, among errors in the top quartile of detection delay (\(\geq 25\) lines; mean \(99\) lines), \(90.5\%\) involve such items: unresolved names and imports (\(63.8\%\)) or missing methods and functions (\(26.7\%\)).

7.3.0.3 Errors are Detected Long before File Completion

Reporting errors close to their source is most useful when those sources occur early in generation, since it prevents the model from producing later code based on wrong assumptions. As shown in 11 (c), GC reports unrecoverable errors at a mean detection point of \(33.3\%\) of the file, nearly matching the timing-free upper bound of \(32.7\%\). Thus, GC avoids generating the remaining \(66.7\%\) of unrecoverably non-compiling output. By contrast, PC reports errors only after file completion by construction, while GC\(^{\mathsf{fn}}\) lags behind with a mean detection point of \(40.3\%\).

7.3.0.4 Detected Error Kinds

We categorize errors detected during mid-file restarts into syntax errors, type errors, borrow-check and lifetime errors, and others. Most errors are type-system related; the most frequent is type mismatch (E0308), which accounts for over a third of reports. Our method also detects more intricate borrow-check and lifetime violations early, including conflicting borrows (E0502) and moves out of borrowed values (E0507). A detailed breakdown appears in 11.4.

8 Discussion and Future Work↩︎

8.0.0.1 Modeling Error Messages

Our generative compiler returns both a verdict \(\mathsf{ok}\) and a diagnostic \(\mathsf{err}\). However, our completeness and soundness results concern only \(\mathsf{ok}\), and do not model \(\mathsf{err}\). In particular, we do not formalize whether \(\mathsf{err}\) describes a genuine defect in the original, unsealed partial program rather than an artifact of sealing, but observe this behavior empirically. This is due to two core reasons: First, we take active measures against reporting artifacts of sealing, by suppressing errors that stem from sealing-inserted code using the expected-error machinery described in 6.1.0.3. Second, in most cases, the placeholders that sealing introduces add no new typing obligations of their own, leaving only already-generated code that is mostly preserved verbatim. Formalizing that \(\mathsf{err}\) represents a genuine defect in the partial prefix, building on prior formal treatments of type-error localization [44]–[46], is future work. A related, open question is how to design error messages for their consumer, for instance whether diagnostics should be reformulated or supplemented with context to be more actionable. This has been studied for human programmers [47] and, more recently, for AI coding agents [48]. Our current rendering follows the rustc diagnostic formatting, because we assume that models are most familiar with this feedback based on their training corpus.

8.0.0.2 When and How to Invoke Generative Compilation

In 3.2, generative compilation is tied to a fixed mechanism: invoke it whenever the previous check finishes, and on rejection, augment the prompt and restart generation. Concurrency makes this loop practical, since validation runs alongside token generation and adds only modest overhead. Decoupling generative compilation from this hardwired decoding loop opens several directions. First, the invocation frequency could be tuned to trade compiler overhead against wasted generation, since less frequent checks only risk discarding a short suffix after rejection. Second, the decision of when and how to invoke generative compilation could be delegated to the coding agent, alongside other tools it may call. Third, our current use of generative compilation treats the LLM as a black box, leaving open whether white-box model access could yield further improvements. Fourth, the diagnostics \(\mathsf{err}\) produced on rejection provide valuable training signals, suggesting the possibility of using them during training rather than only at inference time. Finally, we highlight that generative compilation is a general concept applicable beyond LLMs, and works with any code generation method that is steerable by natural language prompts, and produces intermediate code outputs.

8.0.0.3 Automating Sealor Construction

The sealors in this paper, for both FR(5) and Rust (6), are hand-written. For each construct, we manually derive a sealing rule and argue its completeness and soundness. An open direction is to synthesize such rules automatically from a language’s specification or reference implementation, rather than by hand. This is a challenging task, since rules must be complete while achieving strong soundness, so synthesis would need to search under these constraints rather than under well-formedness alone. Automating this construction could help generative compilation scale even further: to languages beyond Rust, to languages as they evolve, and even to new languages as they are designed and implemented. The latter two cases may benefit most, since LLMs have little or no training data for such code, making direct and on-the-fly compiler feedback especially valuable.

9 Related Work↩︎

9.0.0.1 Compiler Feedback

Compilers help programming in two distinct ways: they establish guarantees, such as memory safety [4], [49] or information-flow security [50], and they provide feedback that guides revision when those guarantees are violated. Such feedback, especially well-designed error messages, has long helped human programmers from novices to professionals [44]–[47]. Earlier research has brought this feedback into AI-assisted code generation, using it during training through supervised fine-tuning [9] or reinforcement learning [11], and at inference time to iteratively refine generated programs [10]. Compiler feedback is now common in coding agents, which run compilers through the command line or invoke them as tools, obtain diagnostics, and accordingly revise code [7]. These approaches all use the compiler after a complete program has been generated. Generative compilation instead invokes the compiler during generation, on still-partial programs, making it an earlier in-the-loop complement to post-generation feedback.

9.0.0.2 Constrained Decoding

Like generative compilation, constrained decoding checks programs during autoregressive generation [14], [51]. The key difference is how the check is used. Constrained decoding intervenes inside sampling, restricting next-token choices. Early approaches do so locally, token by token, which can harm the final program [16], [25], [26]; later work makes sampling aware of global constraints, but still operates at the sampling level [17], [27]–[29]. Constrained decoding for constraints beyond syntax typically requires significant reimplementation [18], [20], and a constraining system that only accepts a subset of the language (i.e., one that is incomplete) can degrade performance [52]. For this reason no constrained decoding techniques exist for complex properties such as the Rust borrow and lifetime system that we could compare generative compilation to.

9.0.0.3 Syntax- and Type-Guided Program Construction

Syntax and types have long guided the program search, especially in synthesis from formal specifications [53]–[57]. Our work also reasons about syntax and types, but targets LLM-based code generation.

Designed for live programming environments like IDEs, typed holes [58], [59] are close in spirit to our placeholders: \({\varepsilon}\) for FR(5.2), and \(\mathtt{hole}_\mathtt{div}()\) and \(\mathtt{hole}_\mathtt{val}()\) for Rust (6.1). The purpose of typed holes is also to make incomplete programs well-typed, permitting the extraction of static type contexts [60]. The difference is where the hole lives. In contrast to our placeholders, typed holes require an extension of the language: the hole in the program is made a first-class citizen of the language, and the type system is extended to reason about it. Our placeholders instead leverage existing elements of the language and are already handled by the language’s type system.

10 Conclusion↩︎

We introduced generative compilation, the first approach to bring compiler feedback into the intermediate steps of LLM-based code generation. The central idea is to seal a partial program into a complete program that a standard compiler can check, thereby turning an off-the-shelf compiler into a prefix checker with diagnostics. This preserves the practical advantages of compiler feedback: black-box model access, use of the real compiler, and rich error messages. At the same time, we avoid the delayed feedback of post-generation checking and the implementation burden of constrained decoding.

We formalized this idea through sealors, proving that a sealor induces a generative compiler with the same completeness and soundness guarantees, and instantiated the framework on Featherweight Rust with a syntax-guided sealor satisfying this property, fully mechanized in Lean. We then carried the same methodology to build the first prefix checker for real Rust, where the sealor handles Rust-specific expression and statement structure, control flow, placeholders, and future-dependent compiler errors while delegating type, borrow, and lifetime reasoning to rustc.

Our evaluation on Rust code generation tasks shows that generative compilation detects many errors close to their source and long before file completion, including type, borrow-check, and lifetime errors. Integrated into code generation, this early feedback reduces non-compiling outputs and improves functional correctness compared with standard post-hoc compiler feedback.

Acknowledgments↩︎

We thank Ralf Jung for his invaluable insights into the complexity of formalizing Rust and his encouragement to pursue the project. Dawn Song and Jingxuan He were supported in part by the Defense Advanced Research Projects Agency (DARPA) Translating All C To Rust (TRACTOR) program under Agreement No. HR00112590134. Niels Mündler-Sasahara and Martin Vechev are supported by the grant SAFEAI (Certified Safe, Fair and Robust Artificial Intelligence). The work has received funding from the Swiss State Secretariat for Education, Research and Innovation (SERI), contract no. MB22.00088. Any opinions, findings, and conclusions expressed in this material are those of the authors, and do not necessarily reflect the views of the sponsoring entities. This research was partially funded by the Ministry of Education and Science of Bulgaria (support for INSAIT, part of the Bulgarian National Roadmap for Research Infrastructure).

11 Experimental Details↩︎

11.1 Construction of UpdatedAPI↩︎

For the UpdatedAPI dataset, we construct a benchmark that requires LLMs to use third-party libraries with API changes after their knowledge cutoff date. The benchmark is constructed as follows. We first fetch the 100 most downloaded Rust crates that have had minor or major version bumps in the previous 6 months at the time of writing. We then task Codex with GPT 5.3 to filter out the packages that had changes to their public-facing API during this version bump. We then task the model to construct realistic and sufficiently complex use cases of these libraries that require the changed API. This step results in 30 single-file code projects that we manually assess to be suitable for LLM evaluation. We then remove the implementation of the function that uses this changed API, replacing it with unimplemented!(). The model is then tasked to regenerate the entire file, including the corrected function bodies. The tasks require implementing an average of 5.9 function bodies (maximum 15) and solutions averaging 3,142 characters (maximum 4,952), which are verified by an average of 3.23 test cases.

11.2 Construction of Translation↩︎

The dataset is based on the CRUST-Bench benchmark [8], consisting of 100 C-to-Rust translation tasks. We run GPT 5.3 and Claude Opus 4.8 on these tasks and observe that they are capable of solving around 80 of these tasks zero-shot, without any compiler feedback. We focus on the remaining 20 tasks. We split each task, which concerns translating an entire library, into individual tasks for each file in the library. The final evaluation is performed by embedding the generated file into a repository of golden solutions. Since interfaces and structures are fixed before compilation, model generations for each file should be independent of the surrounding files. We list the prompts used for generation in 13.

11.3 Experimental Setup Details↩︎

11.3.0.1 Rust Implementation

Our implementation is based on Rust 1.95.0 [24]. We apply a minimal patch to the Rust compiler to access type inference results to reveal defined identifiers and available functions and methods as well as the respective expected number of parameters. Our changes are supplied with the implementation as a code patch.

11.3.0.2 Hyperparameters

The Qwen 3.5 models, GLM 5.2 and Kimi K2.7 are accessed through OpenRouter. Gemini 3.5 Flash is accessed directly through the Google Vertex API. GPT 5.3 Codex is accessed through the OpenAI responses API. Claude Opus 4.8 is accessed directly through the Anthropic API. For Opus, since the API endpoint does not permit setting a temperature, we omit it in requests. For all other models we set it to \(0.6\). The maximum token output for the UpdatedAPI task is 20,000 tokens; for the Translation task, it is 30,000 tokens. We retry model inference errors up to 10 times with a timeout of 600 seconds. Beyond this point we consider inference for a task as failed. This occurs rarely and affects \(0.8\%\) of files in Translation and \(0.2\%\) of files in UpdatedAPI. We further observe that such failures occur for the same instances, which have extremely long input sizes. The verifier and compilation are run on a server with 2 AMD EPYC 9655 96-core processors, totaling 192 physical and 384 logical cores.

11.4 Detailed Analysis of Detected Error Kinds↩︎

We categorize the error codes reported during mid-file restarts in 7.3 into syntactic errors (Syntax), type violations (Type), borrow-check and lifetime violations (Borrow & Lifetime), and others (Other), denoting errors without an associated error code as . 12 shows the resulting histogram per dataset.

The most frequent error on both datasets is a mismatch between an expression and its expected type (E0308), accounting for \(38.2\%\) of reports on Translation and \(37.4\%\) on UpdatedAPI. On Translation, it is followed by accesses to unknown fields (\(9.5\%\), E0609), reflecting the difficulty of faithfully porting C data layouts to the provided Rust skeletons. On UpdatedAPI, the subsequent errors are calls with a wrong number of arguments (\(18.1\%\), E0061), uses of a wrong number of generic arguments (\(7.2\%\), E0107), initializations with nonexistent fields (\(7.2\%\), E0559), and accesses to unknown fields (\(5.4\%\), E0609), errors that arise when a library’s public API evolves, matching the dataset design.

11.5 Restart Budget and Token Limit↩︎

To confirm that the restart budgets of \(15\) (UpdatedAPI) and \(20\) (Translation) restarts and the token limits of \(20,000\) and \(30,000\) tokens do not constrain the results in 7.2, we pool the generations of all evaluated models on both datasets and measure the fraction of compilable outputs attainable within a given number of restarts (13). Both methods improve steeply over the first few restarts and then flatten: increasing the budget from \(15\) to \(20\) restarts raises the fraction of compilable outputs by at most \(2.1\) percentage points for either method (\(84.9\%\) to \(87.0\%\) for GC, \(79.2\%\) to \(80.5\%\) for PC). Per restart, PC initially gains more, as each of its restarts has all compiler errors in context at once; from four restarts onward, however, GC surpasses it. At seven restarts, GC resolves \(4.4\) percentage points more generations within the same budget. Moreover, the generated outputs stay far below our token limits of \(20,000\) and \(30,000\) at every restart count. We conclude that neither the restart budgets of \(15\) and \(20\) nor the token limits constrain the compared methods.

12 End-to-End Example↩︎

The excerpt in 14 is from the UpdatedAPI task for rustls-webpki, obtained with Claude Opus 4.8. The model is asked to update a small certificate-validation crate to a new version of the library while filling the missing implementation in src/lib.rs. During generation, the model constructs a certificate wrapper as a temporary and stores a trust anchor that borrows from it. Our setup detects that the temporary would be dropped while the borrow remains live and returns the E0716 diagnostic immediately. After receiving this feedback, the model binds the certificate wrapper to a local variable, extending its lifetime; and is otherwise correct as well. The early feedback was provided in line 4 of a 32 line function, thus preventing potentially wasteful generation of a significant number of following code.

13 Inference Prompts↩︎

The inference code sends one user message containing the dataset prompt. The required prefix for grading is either prefilled as the beginning of the assistant answer (open-weight models) or appended to the user message as an instruction to start with that exact text (black-box models).

13.1 Generic Inference Wrappers↩︎

Since we require a specific prefix for grading of results but cannot prefill assistant answers for black-box models, we append the short instruction shown in 15 that specifies the required answer prefix; it appears instantiated at the end of the dataset prompts in [fig:prompt-apiupgrade-user,fig:prompt-crustbench-user]. 16 is the user message appended by Generative Compilation after a rejected partial output; the rejected output itself is added to the prompt history as an assistant message, and generation restarts from the prefilled prefix. 17 is the corresponding user message used by Post Compilation after a rejected complete output. Here, the model responds with complete replacement files, patches in a unified diff-like format, or a combination of both, which are applied to the previous output and re-checked. If a returned patch fails to apply, a follow-up user message reports the patch application error and repeats the format instructions.

13.2 UpdatedAPI↩︎

18 is the generation prompt used for UpdatedAPI inference. It is sent as the user message for each crate instance, with the concrete file list and incomplete src/lib.rs substituted into the placeholders.

13.3 Translation↩︎

19 is the user prompt used for Translation inference. It is instantiated with the C sources and the incomplete Rust interface of the target file.

None

None

None

None

None

None

References↩︎

---

1. As reported by OpenRouter for Claude Opus 4.8 (https://openrouter.ai/anthropic/claude-opus-4.8) and GPT 5.3 Codex (https://openrouter.ai/openai/gpt-5.3-codex).↩︎