007 · 断言能被证明，就等于安全语义被保留了吗？AutoTrans 用信号约束、编译与形式化验证移植 RISC-V 安全断言；它能筛掉错误和空洞断言，但‘可证明’与‘忠实保留原安全意图’仍是两个命题。