UC San Diego

In the past few years, the landscape of software development has been reshaped. Large Language Models have made generating code, proofs, tests, and documentation cheap and abundant. A generated artifact may look plausible yet be subtly wrong. At the pace generation now runs, manual review cannot close the gap. Generation is cheap; review is the bottleneck. This dissertation investigates how to establish formal guarantees for code at scale, with minimal human oversight. The first part of this dissertation studies mechanisms for enforcing strict syntactic constraints during LLM generation. In particular, we focus on Grammar-Constrained Decoding (GCD), which integrates formal grammar parsers directly into the decoding process. To make this approach practical for modern LLMs with large vocabularies, we develop techniques to improve the efficiency of grammar-aware decoding. We also identify a fundamental theoretical limitation of GCD: although it guarantees syntactic validity, it can distort the model’s learned probability distribution. To address this limitation, we introduce the Grammar-Aligned Decoding (GAD) problem, which seeks to align the sampling distribution with the desired structural constraints. While syntax can often be captured by explicit grammars, semantic correctness is substantially harder to specify. The second part of this dissertation addresses the problem of synthesizing precise semantic specifications from source code. We introduce a counterexample-guided synthesis algorithm that generates sound and precise program specifications within a target domain-specific language. We further extend this algorithm to nondeterministic programs, enabling the synthesis of both over-approximate and under-approximate specifications. The third part of this dissertation builds on these component-level specifications to synthesize complex systems compositionally. Rather than verifying or generating a large system monolithically, our approach constructs larger programs from existing sub-programs and verified lemmas. Each synthesis task is reduced to a smaller subproblem of the same general form, keeping the search space and proof obligations bounded at the component level. Together, these techniques provide a robust path toward the scalable, specification-guided construction of verified software systems.