热点事件持续更新

作者用LLM写Kopis加密实现并以Lean验证

1 篇报道1 个报道来源1 小时前更新

先了解这件事

AI 综述

一位参与后量子 KEM Kopis 标准化的作者公开了用 LLM 编写 Rust 实现 kopis-rs、再用 Lean 形式化验证其等价性的流程。他先手写 Markdown 规格并反复让 LLM 查找歧义，再用 aeneas 把 Rust 代码提取到 Lean 中证明等价，最终得到 18 条顶层定理和约 30 条公理，并用 TrustBase.lean 检查是否出现预期外的公理。作者同时发布 kopis-rs-smallcode：该版本几乎没有 LLM 生成的代码，但比 kopis-rs 慢得多，且没有形式化验证，只是代码体积更小。Kopis 正在 C2SP 进行标准化；作者称 Lean 代码、测试向量和 Rust 实现均已公开。

AI 根据报道生成 · 59 分钟前更新

最新进展10月22日 02:40

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

报道时间线

沿着报道，了解事件的不同侧面。

10月22日

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

本事件热度走势

还没有足够的连续观测数据，暂不绘制趋势。