形式化验证有潜力大幅减少软件错误，但其高昂的额外成本阻碍了大规模应用。虽然Dafny有望显著减少编写验证程序的工作量，但用户通常需要提供逻辑注释来辅助验证器。在这里，我们探索使用大型语言模型和搜索的组合来构建dafny-annotator：一个向Dafny方法添加逻辑注释的工具，直到验证器能够证明其正确性。在一个来自DafnyBench程序集合的测试集上，由LLaMa 3.1 8B引导的贪婪搜索仅成功注释了15.7%的方法。由于这种数据驱动的方法受到缺乏大规模训练数据的阻碍，我们提出了一种在灵活管道中进行开放式合成新Dafny程序的方法，其中大型语言模型制定高级思想，实现它们，并逐步提出对现有程序的更改，而Dafny则进行验证。这为我们提供了一个合成数据集DafnySynth，我们用它来增强DafnyBench进行训练。在两个数据集上进行微调将LLaMa 8B的成功率提高到50.6%——显著优于基线模型或仅在一个数据集上进行训练的结果。我们的结果表明，为尚无大规模人工生成示例的语言构建强大的AI助手的方法。反过来，这样的助手可能会减少用户的摩擦，并最终推动应用。