GenV 精读：把 Z3 等价性判定蒸馏成语言模型的“第六感”
CWRU×AWS（实习合作）提出 GenV：把离线 Z3 等价 oracle 蒸馏为 reference-free 的连续等价分，专治 autoformalization 中“表面合法但语义错位”的欺骗性轨迹。GenV+HN 在 VPU 检测上 F1 0.832（process RM 仅 0.246），logit lens/SAE 机制分析证明信号真实存在于残差流而非捷径。
形式化验证
MachCSL 精读：MIT 用 AI Agent 把 xv6 内核验证推进到 RISC-V 硬件级
MIT CSAIL（Kaashoek×Zeldovich）的 MachCSL 把并发分离逻辑（Iris 系）扩展到 RISC-V 硬件级语义——页表翻译、TLB、特权级、DMA、断电——并以此为基座证明 6,593 行 xv6 内核的全部不变量。验证过程发现 9 个 xv6 bug 与 1 个 Sail 语义 bug；全程由 LLM Agent 深度参与：77 天、407 个 agent 会话、2,254 个子代理运行、Claude 累计运行 1,729 小时。