源代码级形式化证明

基于抽象解释，自动分析所有整数变量的取值范围、数组索引边界、变量间线性关系。无需开发者写任何形式化规约，即可证明无除零、无越界、无算术溢出。

当证明失败时，输出最小化具体输入值 + 违反断言的代码行号 + 变量状态快照。可直接用该输入运行程序，一步定位根因。

为每个函数生成前置/后置条件的摘要，调用者仅依赖摘要而非函数体。修改实现只重证该函数与依赖摘要的接口，大幅提升大规模代码验证效率。

额外处理按位运算、非线性乘法截断、CPU 标志寄存器、内联汇编块。适用于 RTOS 内核、驱动与混合 C/汇编代码库。

在任意线程交错下，证明共享内存更新始终符合高层设计的原子性要求，且不会引发死锁或数据竞争。