Basis 团队提出一个直白的做法来解决「形式化语义」这个验证瓶颈：不要手写语义再祈祷它和实现对得上，而是把语言现存的那个解释器编译成 RISC-V 二进制（RISC-V 的指令语义已有形式化模型），让 LLM 写一份可读的语义规则，并在 Lean 里证明「对任何程序，这份规则预测的输出与编译后解释器实际打印的输出完全一致」。若某条规则写错，证明就卡住，而这个无法闭合的证明义务通常正好指向错的那条规则。实验对象是教科书里 WHILE 语言的扩展版：整数、字符串、带闭包的一等函数、if/while/for 与运行时错误，解释器是 1,855 行 C，编译后 25,336 条 RISC-V 指令。语义只有约 400 行规则，但光靠测试根本不够——早期版本的语义通过了整套测试，却在函数名长达 59 字符时出错：C 里 stringify 用 64 字节栈缓冲加 snprintf，连接时截到 63 字节，语义却按完整名字输出。证明逼出了四处修正：64 位整数回绕、for 循环初始化忽略中断状态、内建函数在打印与连接中呈现不同、长闭包名截断到 63 字节。内存推理最麻烦：malloc 的写入足迹随所有权变化，固定足迹集合无解，最终把 xv6 证明用的 MachCSL 移植到 iris-lean 才走通。峰值证明约一百万行 Lean，其中三分之二由 35 个脚本按约 11,800 条指令逐条生成；后来用抽象替换生成族，压到 20 万行以内。语义可信之后，团队三天内基于它做出类型检查器、程序逻辑、抽象解释器和经验证的编译器，编译后指令数降到解释器的 1/2.7 至 1/8.2。