Alchemy 作者探索用 Z3 求解器静态证明 TypeScript 领域模型不变量
samgoodwin89 · x · 2026-11-12
Alchemy 作者 sam-goodwin 分享了他在 Alchemy Domain 中做的自动验证实验:在 Aggregate 上声明不变量(invariant),用 SMT 求解器 Z3 静态「证明」或「探索」它们永不被破坏。
后续推文补充:静态证明有极限,于是还提供 Explore 模式——穷举命令/事件/策略空间,模拟每个短命令序列(经由 API、跟随 policy/saga/调度反应)寻找打破不变量的反例,本质上就是仿真。配套 PR #3260 已在 alchemy-run/alchemy 仓库公开,作者承认 TypeScript 能力有边界,但看好这个方向,并致谢高产出贡献者 @taraskorn。
所属事件:Alchemy 尝试用 Z3 求解器自动验证领域模型不变量(2 条相关)→
「编程与Agent」频道最新
- 单条 prompt 用 Blender MCP 搭拉面摊,Qwen4-Max 用量仅 DeepSeek 约 1/4 — teortaxesTex · 2026-11-12
- 1.7B 小模型被曝用浏览器写 HTML 自主跑任务,称达 4o 水平 — JosephJacks_ · 2026-11-12
- 黑客松作品:用 Hermes 智能体从自然语言生成 3D 打印模型 — alexcovo_eth · 2026-11-12
- 百度 ERNIE 5.5 Flash 自写代码生成可编辑 CAD 摩天楼模型 — heyshrutimishra · 2026-11-12
- Gamma 的 /docs/ 页面沦为 parasite SEO 靶子,域名风险警示 — gefei55 · 2026-11-12
- 一个实用 prompt：让 agent 说出它对你的需求假设 — keyanzhang · 2026-11-12