Alchemy Domain 新 PR:用 Z3 验证领域不变量,穷举 13,310 条命令序列找反例
samgoodwin89 · x · 2026-11-12
alchemy-run/alchemy 仓库的 PR #3260(Draft)展示了 Alchemy Domain 的自动验证能力:
- Prove:对 Aggregate 的每个状态和命令证明不变量成立,不给具体值,直接读源码让 Z3 求解;示例中删掉 WithdrawMoney 的一个校验,证明立即失败并给出违例状态与命令
- Explore:枚举经由 API 的所有短命令序列(跟随 policy、saga 和调度),探测打破不变量的组合;Bank 模型示例穷举 13,310 条序列、15,014 个状态,发现 NoAccountOverTenDollars 被一条「注册 + 存入 1001 美元」的命令组合打破
- 用法上只需 Prove.invariants(Account, {source}) 或 Explore.check(Bank, {apis, depth: 3}),无需手写测试值——求解器会自动挑出边界输入(如超限一美分的存款)
所属事件:Alchemy 尝试用 Z3 求解器自动验证领域模型不变量(2 条相关)→
「编程与Agent」频道最新
- 8组Agent并行写代码，3小时生成83秒日式动画短片 — FinanceYF5 · 2026-11-12
- Fable 5.5纯代码做出83秒动画短片，8组Agent并行3小时完成 — FinanceYF5 · 2026-11-12
- 用多机器人团队协作后，作者改推「Checked Loop」循环工作法 — JoeJustice · 2026-11-12
- 开发者让 AI agent 当解谜游戏公司 CEO,每天自动发明新游戏 — RichardsonDx · 2026-11-12
- AI Agent 为何健忘？一文讲清记忆层如何补上架构缺口 — sharpeye_wnl · 2026-11-12
- 免费目录收录约 200 个 AI Agent 平台，按 20 类场景对比定价 — Mahmoud_Zalt · 2026-11-12