Ovid：一个让 pi 扩展记录其功能实际运行证明的扩展

- **Ovid** 是一个 Raspberry Pi Pico 上的实验性项目，给 Pi 的 C 语言 SDK 加上“形式化验证”——也就是用数学方法证明代码的行为符合预期，而不是靠跑测试赌它是对的。 - 传统固件开发靠跑测试（比如按一下按钮看灯亮不亮），但测试只能覆盖有限的情况。形式化验证用逻辑推理覆盖所有可能路径，代价是写证明非常费时。Ovid 的卖点是：让开发者用类似写注释的语法声明“这行代码之后，变量 X 总是正数”，然后自动生成证明，减少手写证明的工作量。 - 该项目用到了 **CBMC**（C 程序模型检查器），一种自动遍历所有可能执行路径的工具，以及 **Z3**（微软出品的 SMT 求解器），用来验证逻辑条件是否成立。Ovid 把两者集成到普通 Pi SDK 项目的编译流程里。 - 之所以有意义，是因为嵌入式设备（无人机、医疗设备、汽车控制器）一旦出 Bug 可能造成物理损坏甚至人员伤亡。如果能像写普通代码一样方便地加上数学保证，安全关键系统的开发门槛能大幅降低。