038 · 不知道 exp 怎么算，也能证明浮点 kernel 等价吗？
这篇论文把超越函数保留为不透明符号，证明生成 kernel 与形式规格对同一符号的使用一致。关键问题是：这种对任意函数都成立的定理，为什么仍依赖真实实现采用同一个函数？
Formal-Verification
034 · AI 写的证明通过了，信任消失了吗？
Blanc 直接验证已部署的 EVM 字节码，让 AI 参与写证明，由 Lean 内核检查。值得追问的是：不再信任证明生成者以后，哪些判断仍留在证明之外？
031 · 绕过 Triton 后端，正确性责任去了哪里？
AI as a Compiler 让 Agent 从 Triton 直接生成 PTX，在部分任务上找到传统 lowering 之外的优化；但高性能指令也超出了原版验证器的能力。减少中间表示，并不等于消除语义建模与正确性责任。
025 · 返回值被唯一确定，就算规格完整了吗？
SpecAgent 用依赖感知规划、形式验证、跨规格修复与强度审查生成 ACSL 规格；其完备性探针能识别返回值欠约束，但不能单独证明规格已表达全部重要语义。
022 · 断言被证明后，谁证明它值得验证？
ProofLoop 让 Agent 查询 RTL 结构并利用形式反例修正 SVA，显著提高可证明断言的比例；但在 Design2SVA 中，性质成立、性质非空洞与性质重要仍是三个不同判断。
021 · 六类任务拼在一起，就算端到端验证了吗？
FIXME 用 180 道题覆盖规格理解、参考模型、测试用例、testbench、断言和调试；它拓宽了 LLM 硬件验证评测，却也留下一个概念边界：流程覆盖不等于端到端执行。
019 · 编译器被证明正确，错误还藏在哪里？
ACDC 以 Axon 为对象，分别测试已验证核心、可信检查、未验证文本接口与机器语义；实验说明形式证明能封闭一部分错误，却不能替代对规格、信任边界和拒绝行为的测试。
007 · 断言能被证明，就等于安全语义被保留了吗？
AutoTrans 用信号约束、编译与形式化验证移植 RISC-V 安全断言；它能筛掉错误和空洞断言，但‘可证明’与‘忠实保留原安全意图’仍是两个命题。
004 · RTL 与断言来自同一份规格，形式化证明了什么？
一条从受控自然语言规格同时生成 RTL 与形式化断言的工作流，以及它尚未消除的共同误解与证据边界。
001 · AI 开始设计芯片，工程师还需要哪些基本功？
一篇关于 AI 时代芯片设计基础、知识与判断力的观点论文：读懂作者论证，追问其假设与边界。附 alphaXiv 与三个思考问题。