Rocq

Bend：用证明阻断AI错误的编程语言

Bend 是一门宣称通过内置“法律”(LAWS.bend)与可验证证明(PROOF.bend)防止 AI 引入错误的新语言，编译为原生代码并可在 GPU 上并行运行。其类型检查器兼作证明检查，声称对中等代码库在秒级完成校验，单核接近 C 的速度、GPU 上最高可达百倍加速。该设计旨在让 AI 在提交前必须给出形式化证明以避免回归。