Our research helps people write software that executes as intended.
Directed by Charlie Murphy · Gianforte School of Computing · Montana State University
Research
Helping you write secure, trustworthy software.
FORGE combines the complementary strengths of generative AI and symbolic, automated reasoning. Generative models scale and produce plausible, often-correct results—but we don't take them on trust. We pair them with automated reasoning that checks their output and returns sound, interpretable feedback. That is why our work centers on solvers and reasoning systems that produce concrete examples and proof certificates: evidence a developer or another tool can inspect and build on. Together they yield strong guarantees about what software actually does—across programming languages, provable security, and program synthesis.
Programming languages, logic solving, and automated reasoning: the core engines—program synthesis, verification, and decision procedures—that everything else in the lab is built on.
PL · Logic · Automated ReasoningTurning security properties into obligations a machine can check—so that guarantees about access, isolation, and policy hold by construction rather than by testing alone.
Verification · Policy · GuaranteesGenerative models can propose programs; formal reasoning can decide whether to trust them. We pair synthesis from LLMs with solvers and proofs so the code they produce is provably correct.
Synthesis · LLMs · CertificatesOur systems run generative proposal and symbolic checking in a loop. A model proposes a candidate; a solver or verifier checks it against the specification. When it holds, we return the result with a certificate of its correctness. When it fails, the same machinery yields a proof witness that says why—that this input diverges, or that these inputs violate a particular conjunct of the spec—not merely that some input–output pair is wrong. That witness becomes rich, structured feedback for the next proposal, so each iteration is guided by an interpretable reason rather than a blind retry.
Some of our projects generate a program together with a machine-checked proof of its correctness—in Verus for Rust, or in proof assistants like Lean 4 and Rocq. A verification harness guarantees soundness, while tooling and practice from software engineering push toward verified software that is high-quality and maintainable—rather than proving isolated properties one at a time. The same idea carries into agentic coding tools: we bring decades of programming-languages and software-engineering research to the coding loop, so the code these agents produce is correct and maintainable—not just plausible.
News
What's new.