一句话：提出 StarFuse，用 LLM 从多模态输入合成并修复出经 F* 验证的程序。
交互式定理证明器（ITP）如 F* 能提供强软件正确性保证，但其陡峭学习曲线、专用语法和复杂证明机制限制主流采用。本文提出 StarFuse，一个 LLM 辅助开发工具，可从混合格式源文件自动合成完全验证的 F* 程序。开发者可用自然语言、伪代码、C、OCaml 和 F* 草图混合表达意图。StarFuse 采用上下文感知、编译器引导的修复循环，迭代查询 LLM 并利用 F* 编译器诊断精化与修复代码；还集成“fuzz first”机制，在昂贵验证前过滤函数片段中的浅层错误。基于 F* 仓库实例的评估表明能跨多种模态验证实现，为从非形式化意图到形式验证提供桥梁。
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.