qizwiz/pact

# pact [](https://github.com/qizwiz/pact/actions/workflows/ci.yml) [](https://pypi.org/project/pact-tool/) [](https://pypi.org/project/pact-tool/) [](LICENSE) **针对 AI 生成的代码库进行形式化分析。** LLM 生成的代码具有典型的故障特征：未等待的协程、未受保护的空值解引用、静默的异常吞噬、ORM 写入中的竞态条件、未受保护的 LLM 响应读取。测试无法捕获这些问题——它们只能运行你能想到的路径。pact 将每种故障模式编码为调用图上的 Z3 约束并找出所有问题，然后生成可以进行模型检测的 TLA+ 规约。 支持 Python 和 Go。更多语言遵循相同的模式。 ``` pip install pact-tool pact . ``` ``` ✗ pact: 14 violation(s) tasks/auto_eval.py:89 [missing_await] coroutine 'trigger_evaluation' called without await — the evaluation never runs; this is a silent no-op model_hub/views.py:203 [optional_dereference] 'api_key' assigned from .get() at line 201 but passed to LLM client without None check — AttributeError in production evaluations/tasks.py:156 [save_without_update_fields] .save() re-writes every column; concurrent request at line 201 overwrites the status you just set utils/cache.py:44 [bare_except] except Exception: pass — the Redis timeout that caused your 3am incident is silently swallowed here ``` ## 为什么选择 pact？ 这个名字起初是 "Python AST Constraint Tool" 的缩写——一个围绕其核心 Z3 约束引擎构建的反向首字母缩写。它被保留下来是因为它具有实际意义：pact 意为正式协议、契约。这正是 pact 所执行的——你的代码与自身之间建立的那些隐式契约，除非你早就知道要编写相应的测试，否则没有 linter 会检查，也没有测试会覆盖它们。 针对 Python 的特定起源现在只是一个细节。该约束引擎适用于任何具有 AST 的语言。 ## pact 的不同之处 大多数 linter 负责捕获代码风格。大多数类型检查器负责捕获类型。pact 负责捕获**结构性 bug** ——那些只在并发、大规模场景下，或者当 LLM 响应比你预期的要短时才会出现的问题。 每种故障模式都被编码为调用图上的 Z3 约束，而不是正则表达式。这意味着： - **跨文件推理**：`tasks.py` 中的 bug 是由 `models.py` 中的更改引入的 - **上下文感知**：`.get("key", default)` 是安全的；`.get("key")` 则不安全——pact 知道其中的区别 - **形式化基础**：违规项满足 Z3 可满足性，而不是启发式猜测 ## 真实世界的发现 **[home-assistant/core](https://github.com/home-assistant/core)** — 8万7千星标，14,096 个文件： ``` $ pact /tmp/ha-core/ ✗ pact: 34,701 violation(s) in 14,096 files (2m 43s) optional_dereference 22,458 nullable state pervasive across 3,000+ integrations required_arg_missing 11,148 plugin pattern omits positional args at call sites missing_await 1,068 async polling called without await — body never runs ``` **[langchain-ai/langchain](https://github.com/langchain-ai/langchain)** — 13万6千星标： ``` $ pact /tmp/langchain/libs/ ✗ pact: 438 violation(s) missing_await 256 _astream() unawaited across every provider llm_response_unguarded 4 response.content[0] without length guard — crashes on content-filtered responses ``` **[future-agi/future-agi](https://github.com/future-agi/future-agi)** — 生产级 AI 平台： ``` $ pact futureagi/ ✗ pact: 6,931 violation(s) ``` 参见 [`examples/future-agi/findings.md`](examples/future-agi/findings.md)。 ## 安装 ``` pip install pact-tool ``` 如需生成 TLA+ 规约（需要 Anthropic API 密钥）： ``` pip install "pact-tool[llm]" ``` ## 使用方法 ``` # Scan 你的项目 pact path/to/project/ # CI 模式 — 仅限自 main 分支以来更改的文件 pact . --incremental main --strict # Ranked refactoring targets (highest violation density × lowest coupling) pact . --suggest # Structural analysis: cycles, pass-through hops, fan-out hubs pact . --reduce # 用于下游工具的 JSON pact . --json ``` ## 故障模式 | 模式 | 捕获内容 | |------|-----------------| | `optional_dereference` | 使用 `.first()` / `.get()` 的结果时未进行 `None` 检查 | | `missing_await` | 在没有 `await` 的情况下调用了异步函数——函数体永远不会执行 | | `bare_except` | `except Exception: pass` ——静默的错误抑制 | | `save_without_update_fields` | `.save()` 会覆盖所有列，导致并发写入出现竞态 | | `unvalidated_lookup_chain` | 将 `d.get(k)` 的结果作为字典键使用而未加保护 | | `required_arg_missing` | 调用时省略了必需的参数 | | `mutable_default_arg` | `def f(x=[]):` ——跨调用共享状态 | | `llm_response_unguarded` | 使用 `response.choices[0]` 时未进行长度检查 | | `model_constraint` | 创建 Django model 时缺少必需的字段 | 通过 `pact-go` 支持 Go：`go_ignored_error`、`go_bare_recover`、`go_unchecked_assertion`、`go_goroutine_no_sync`。 ## CI 集成 ``` - name: pact uses: qizwiz/pact/.github/actions/pact@main with: path: . incremental: "true" strict: "true" ``` 或直接使用： ``` - run: pip install pact-tool z3-solver && pact . --incremental main --strict ``` ## TLA+ 规约合成 pact 从你的 Python 源码中提取 TLA+ 规约——70% 通过 AST 机械性提取，30% 由 LLM 补充（活性属性、领域不变量）。 ``` # Generate skeleton pact spec gen path/to/models.py # Fill in liveness + domain invariants export ANTHROPIC_API_KEY=sk-... pact spec complete path/to/tasks.py -o MySpec.tla # Model-check with TLC java -jar tla2tools.jar -config MySpec.cfg MySpec.tla ``` pact 自身的形式化规约位于 [`docs/tla/Pact.tla`](docs/tla/Pact.tla)，在 CI 中通过 TLC 进行了验证。 ## 图缩减 `--reduce` 用于发现**结构性脆弱点**——调用循环、穿透跳数和扇出枢纽——并按 `reduction_potential + violations × 0.5` 排名： ``` $ pact . --reduce ⬡ TANGLE payments.charge → payments.validate → payments.charge cycle of 3 — break to make this subgraph a DAG score=4.0 violations=4 ⬡ PASSTHROUGH api.route_and_forward 1 caller → 1 callee — pure hop; inline to collapse 1 node + 2 edges score=3.5 violations=1 ``` ## 工作原理 ``` extractor.py AST → ModelManifest, FunctionManifest, CallSite failure_mode.py FailureMode plugin layer (per-call + file-level checks) z3_engine.py Z3 Fixedpoint Datalog — whole-program queries checker.py Orchestration: extraction → Z3 → dedup → Violation list refactor.py Suggestion engine: violation density ÷ caller coupling specgen.py AST → TLA+ skeleton (70% mechanical) speccomplete.py Anthropic API → fills TODO stubs (30%) go/checker/ Go AST checker (Go codebase support) cli.py Entry point ``` pact 将每种故障模式编码为调用图上的 Z3 约束。增量引擎通过 BFS 将更改传播到整个调用图，因此只会重新分析有变动的子图。 ## 架构决策 设计理由参见 [`docs/adr/`](docs/adr/)。从 [ADR-036](docs/adr/ADR-036-pact-formal-analysis-toolkit.md) 开始阅读——了解为什么选择 Z3 Fixedpoint 而不是传统的数据流分析，以及为什么选择 TLA+ 而不仅仅是属性测试。 ## 许可证 MIT

标签：AI生成代码检测, DNS解析, Go, LLM代码审查, odt, pact-tool, Python, Ruby工具, SAST, SOC Prime, TLA+模型检验, Z3约束求解器, 代码安全, 代码静态分析, 并发竞态条件检测, 开发工具, 开源项目, 形式化分析, 抽象语法树, 数据管道, 无后门, 漏洞枚举, 盲注攻击, 调用图分析, 软件工程, 逆向工具, 静态代码检查