formal-verification

dawnr：以七种证明器形式化验证为门槛的可信代码助手

trestoncuzzort/dawnr · An assistant built to be trusted by proof, not by sounding right: a small language model trained from random weights on one machine, running with nothing behind it, whose programs carry specifications checked by seven provers (Dafny, Verus, SPARK, Frama-C, Lean 4, Rocq, F*), each also refuting a sabotaged twin. It learns only from what was proved.

dawnr 是一个以“先证明、后采信”为核心原则的助手项目，用小型语言模型生成带规格说明的程序，再交由 Dafny、Verus、SPARK、Frama-C、Lean 4、Rocq、F* 七种独立证明器检查。材料记录了学生模型在给定规格时的证明通过率、七证明器一致性门槛、构造性反例（被篡改孪生程序）检验、规格与问题一致性的额外检查，以及在本地硬件上以量化方式运行的整体流程。仓库同时包含从零训练核心模型、用已验证数据微调开源权重、强化学习与门控反馈成新数据、个人记忆与适配器、检索/语音/视觉/工具调用等实验性模块，并声明各项进展与已知失败模式。