StarFuse: LLM Guided Multimodal Interactive Theorem Proving

Abstract

Interactive Theorem Provers (ITPs) like F* provide robust mathematical guarantees for software correctness, but their steep learning curves, specialized syntax, and complex proof mechanics severely limit their mainstream adoption. To lower this entry barrier, we propose StarFuse, an LLM-assisted developer tool that automatically synthesizes fully verified F* programs from mixed-format source files. StarFuse allows developers to express their intents using a combination of natural language, pseudocode, imperative code (C), functional code (OCaml), and F* sketches. It employs a context-aware, compiler-guided repair loop that iteratively queries a Large Language Model (LLM) and utilizes F* compiler diagnostics to refine and fix the generated code. Additionally, it integrates a "fuzz first" mechanism for functional snippets to quickly filter out shallow bugs before invoking the expensive verification process. To evaluate StarFuse, we created a benchmark suite based on instances from the F* repository. Our evaluations demonstrate the ability of StarFuse at successfully verifying implementations across various modalities, thereby offering a practical bridge from informal intent to rigorous formal verification.