Anthropic的证明流水线为：开源库加Faust测试编译成RISC-V可执行文件，叠加上FreeRTOS的RISC-V与操作系统形式语义以及不崩溃性质，机械生成规格，由Claude写证明，交给Rocq内核检查。