openDaisugi 发布：用 Z3 形式证明约束 AI Agent 工具调用的 JIT 编译器

levitatingflyfisher 发布 openDaisugi，一个面向 AI Agent 的 JIT 编译器：模型决策，信封定义允许范围，Z3 在每次工具调用执行前证明其不越界，重复工作可编译为验证过的 pathway 以零 token 复用。支持 enforce（证明失败即拒绝）与 audit（默认，仅记录）两种模式，可通过 hook 接入 Claude Code、Codex、pi 和 OpenCode，并提供 Go、Rust、Python 三套实现，Python 包为 oracle。Go/Rust 门控调用 p50 分别为 8.8ms 和 6.1ms，一致性测试 0 分歧；作者说明实用性尚未实测、Codex hook 失败时会放行、尚无正式发布版本。