用 LLM 和 Lean 形式化验证写出高保障密码学代码

作者以自己参与标准化的后量子 KEM Kopis 为例，记录了借助 LLM 编写 Rust 实现、再用 Lean 形式化验证保证等价性的完整流程。他手写 Markdown 规格并反复让 LLM 找歧义，用 aeneas 把 Rust 提取到 Lean 证明等价，最终得到 18 条顶层定理和约 30 条公理，并用 TrustBase.lean 检查是否出现预期外的公理。