Basis 用 LLM 和 Lean 证明解释器到 RISC-V 机器码全链路正确

Basis 团队介绍了一种利用 LLM 为小型编程语言生成精确形式化语义、再用 Lean 证明其解释器编译至 RISC-V 机器码后仍符合语义规则的方法。相关工作还包括用 agent 构建 JS 到 WebAssembly 编译器、验证 Linux nftables 编译器，以及 MIT 团队在 9 月将 xv6 内核验证至机器码层。