tsinghkothari-droid/pramaan

# Pramaan **用于 AI 生成 pull request 的验证基础设施。**  AI 编程 agent 的速度已经快到足以编写全球很大一部分的软件。现在的瓶颈不再是代码生成，而是信任。 Pramaan 将 AI 生成的代码变更转化为可审计的证明 bundle：包含结构化的回执、执行证据、风险 ID、重放数据，以及哈希链接的 artifact，以展示哪些内容已被检查，哪些仍需要人工判断。Sigstore/in-toto 签名已在路线图中；目前已支持本地哈希完整性验证。 它并不兜售某种工具可以证明任意软件正确性的幻想。它解决的是工程团队每天面临的实际问题： ## 问题 现代 AI agent 能够生成看起来完善、能通过 CI，却仍然破坏生产行为的代码。 其失败模式非常隐蔽： - agent 没有修复 bug，反而削弱了测试； - 更新了快照或 fixture 以通过错误的行为； - 从未重现最初的失败案例； - 虚构了虚假的 API、import、参数或 symbol； - 新测试只检查某物是否存在，而没有验证行为是否正确； - 修复仅对狭窄的 prompt 有效，却导致相邻路径发生回归； - CI 日志消失在构建系统中，没有留下持久的证据轨迹。 传统的 CI 只回答一个问题：这些命令是否成功执行完毕？ Pramaan 回答的是审查者真正需要了解的问题： ## 当前实现状态 Pramaan 仍处于早期阶段。该仓库已经发布了 Rust CLI 基础、带有稳定 `$id` URL 的回执 schema、bundle 哈希验证、沙箱/环境证据、记录真实底层工具版本的静态检查适配器、结构化的 oracle 完整性检查、演示 fixture、在工具安装时运行的变异适配器、确定性差分重放证据、带有受限沙箱执行的 AI 证据探测计划、未校准的可审计置信度投票、验证器滥用面检测，以及 GitHub Action 包装器。 `pramaan verify` 现在默认会编排真实的执行阶段（声明范围、沙箱设置、静态检查、oracle 完整性、差分模糊测试）。变异测试可通过 `--with-mutation` 选项启用。可以使用 `--skip-stage ` 跳过特定阶段，以实现快速迭代。 它目前**尚未**提供生产级的 Sigstore 签名、强制容器隔离、生产级沙箱内任意生成代码的执行、完整的编译器 AST oracle 解析或已校准的置信度。在安装了相关工具的情况下，可以运行受限的生成式 Hypothesis/fast-check 测试套件；仅当受限的 AI 探测带有安全标记并绑定到变更行为时，才能对其进行编译/运行检查。缺失的工具和被拒绝的探测将作为可见的残余风险保留下来。 请参阅 [STATUS.md](STATUS.md) 获取真实的特性矩阵。 ## 操作者文档 - [快速开始](docs/quickstart.md)：使用一条命令实现最小且好用的验证器循环。 - [操作指南](docs/operator-guide.md)：安装、运行、检查和发布。 - [GitHub Action](docs/github-action.md)：CI 包装器的输入、权限和摘要行为。 - [安全模型](docs/security-model.md)：信任边界和运行器指南。 - [故障排除](docs/troubleshooting.md)：缓慢的变异、缺失的工具、不稳定的测试、fork 的 PR 以及 bundle 验证。 - [发布打包](docs/release.md)：手动发布门控和 artifact 检查清单。 - [渲染示例](docs/rendered-examples/README.md)：通过、警告、失败和 bundle 检查示例。 - [审查者用户体验](docs/reviewer-ux.md)：用于优先检查阻碍项的本地 HTML/Markdown 报告。 - [审查者界面](docs/reviewer-interface.md)：原始命令名称、配置契约和 PR 审查面边界。 - [人工签核](docs/human-signoff.md)：agent 可以自我验证什么，以及在哪里需要人工批准。 - [竞品基准测试](docs/competitive-benchmark.md)：Pramaan 与审查助手、质量报告聚合器、测试生成器和认证基元相比，有哪些重叠、复用和不同之处。 - [Phase-36 前的 GSD Prompt](.planning/AUTONOMOUS_GSD_BEFORE_PHASE_36_PROMPT.md)：即用型自主 prompt，用于在语言深度扩展之前完成所有剩余的 GSD 阶段。 ## Pramaan 的回答 Pramaan 是一个用于代码审查的“回执优先”验证层。对于每个 pull request，它正致力于构建一个包含各阶段回执的可检查 bundle：  ``` PR diff -> Claim scope (runs in `pramaan verify`) -> Sandbox setup + environment evidence (runs in `pramaan verify`) -> Static and hallucination checks (runs in `pramaan verify`) -> Oracle integrity (runs in `pramaan verify`) -> Differential fuzz / replay evidence (runs in `pramaan verify`) -> Delta mutation (opt-in: --with-mutation) -> Auditable confidence vote (separate: pramaan confidence explain) -> Bundle integrity, signing metadata, attestation -> GitHub Action summary (rendered from bundle.manifest.json) ``` 每个阶段都会生成一份回执，包括被跳过和失败的阶段。审查者可以确切地看到运行了什么，使用了哪些工具和版本（真实的 ruff / mypy / tsc / cargo / mutmut / StrykerJS / cargo-mutants 版本，而不仅仅是 Pramaan 包装器的版本），对哪些文件和 artifact 进行了哈希处理，使用了哪些种子或语料库，缓解了哪些风险，以及还存在哪些风险。 Pramaan 不是又一个模糊的 AI 评论家。它是基于执行的验证基础设施。 同时也应将其理解为对现有工具的补充，而不是一揽子替代方案。审查助手、质量报告聚合器、测试生成系统以及 SLSA/Sigstore/in-toto 证明都是有用的相邻工具。Pramaan 的差异化优势在于围绕这些信号构建的可审计 PR 证据 bundle。请参阅[竞品基准测试](docs/competitive-benchmark.md)以获取当前的相关技术地图，以及 Pramaan 仍然拒绝做出的声明。 ## Bundle 能证明什么 Pramaan bundle 是一个有界限的声明，而不是一张神奇的证书。  它可以证明以下内容： - 声称失败的测试现在未加修改地通过了； - 现有测试仍然通过； - 测试没有被跳过、删除或明显削弱； - fixture 和快照的变更被标记为对 oracle 敏感； - 静态检查未发现虚构的 import 或未定义的 symbol； - 变异测试覆盖了变更的行为，并记录了存活的变异体； - 模糊/属性测试使用了记录的种子和重放数据； - 证明 bundle 本身未被篡改。 它不声称： - “此代码是正确的”； - “所有 bug 都是不可能存在的”； - “LLM 评论家们同意，所以合并吧”； - “七项检查意味着七个独立的概率。” 这种克制正是它的产品价值所在。Pramaan 为团队提供了更有力的证据，而不是假装不确定性已经消失。 ## 为什么现在这很重要 AI 代码生成改变了软件审查的经济学。人工审查者再也无法像检查手写代码那样，以同样的注意力检查每一行生成的代码，尤其是当 agent 每天生成许多小型 PR 时。 开发者工具链的下一层必须是： - **可审计**：每个结论背后都有 artifact 支撑； - **基于执行**：检查针对真实的基础/目标代码运行，而不仅仅是文字描述； - **风险感知**：输出结果会指出仍然存在危险的地方； - **可重放**：失败和模糊测试用例可以被重现； - **可签名**：目前证据已实现哈希链接，并为未来的签名做好了准备； - **诚实**：绝不虚假声称拥有完全的正确性。 Pramaan 就是作为这一层而构建的。 ## 核心能力 ### 回执优先验证 每个阶段都会写入结构化的 JSON 回执，包含： - 阶段名称和状态； - 工具标识和版本； - 输入和 artifact 哈希值； - 开始/结束时间戳； - 退出代码和摘要； - 已缓解、残余、已跳过和不适用的风险 ID。 ### 声明范围 Pramaan 会在判断测试和执行证据是否与声明一致之前，记录 pull request 声称要更改的内容。 这可以捕获一种主要的 AI 代码失败模式：PR 通过了测试，但解决的却是错误的问题、过拟合了 prompt，或者批准了预期范围之外的行为。 ### Oracle 完整性 Pramaan 将测试、fixture 和快照视为信任边界的一部分。 它旨在检测： - 跳过的测试； - 移除的断言； - 削弱的断言； - 更改的快照； - 更改的 fixture； - 缺失的原始失败测试； - 可疑的 oracle 漂移。 这是杀手级用例：正常的 CI 可能会显示通过，因为 agent 削弱了测试。Pramaan 应该将其转化为清晰的红色（失败）回执。 ### 静态和幻觉检查 AI 生成的代码经常由于虚构了看似合理的名称而失败： - 不存在的 import； - 未定义的变量； - 虚构的 API； - 无效的参数； - 错误的文件或资源名称。 Pramaan 会对这些失败进行分类，而不是将它们笼统地压缩成通用的“lint 失败”输出。 ### 增量变异 覆盖率是不够的。测试可能会执行了代码，却没有对关键行为进行断言。 Pramaan 正在构建使用基于 diff 范围的变异测试，以提出一个更尖锐的问题： 目前的代码包含变异命令包装器、回执标准化、原始输出摘要和工具缺失回执。这些工具在安装后会运行；缺失的工具将作为可见的残余证据保留下来，而不是直接显示为通过。 ### 属性、模糊和差分检查 对于符合条件的变更函数，Pramaan 会在共享的生成输入上比较基础版本和目标版本的行为。当前代码包含针对狭窄的纯函数 fixture 的确定性重放证据，记录是否安装了 Hypothesis 或 fast-check，并在安装了这些工具时尝试运行受限的生成式 Hypothesis/fast-check 测试套件。缺失的工具将作为可见的回退证据保留下来，而不是直接通过。 这就是 Pramaan 捕获“bug 已修复，但附近的行为发生了改变”情况的方式。 ### 签名的证明 Bundle 回执和 artifact 被收集到一个 bundle 清单中。如今已经可以对 bundle 进行哈希完整性验证，并为未来的 Sigstore、GitHub artifact 证明以及 in-toto/SLSA 风格的溯源流程做好了准备。 ## 非目标 Pramaan 有意不声称自己是： - 任意软件都正确的证明； - 自动合并授权机构； - CI 的替代品； - 通用的 agent 注册表； - 在 CLI 和 GitHub Action 变得值得信赖之前的以仪表板为主的产品。 ## 审查者摘要示例 这是审查者体验的发展方向，并不保证以下每一行内容都会在当前 `verify` 命令的一次集成运行中输出。 请参阅 [STATUS.md](STATUS.md) 和 [声明审计](docs/claim-audit.md) 了解目前发布的具体功能。 ``` Claim Fix invoice rounding for mixed tax rates. Evidence PASS Original failing test now passes unchanged. PASS Existing tests still pass. PASS No assertions were weakened. PASS Static checks found no invented imports or undefined symbols. WARN Mutation killed 87% of changed-line mutants; 3 survived. PASS Differential property checks found no unexpected divergence. Residual risks R-049 concurrency not exercised. R-057 performance not benchmarked. R-081 formal verification not applicable. Bundle Hash verified. Tool versions recorded. Seeds and corpus hashes recorded. ``` ## 研究基础 Pramaan 建立在软件测试研究、AI 代码评估失败经验以及生产级供应链工具的基础之上。 ### AI 代码可靠性 - [tau2-bench](https://arxiv.org/abs/2506.07982)：重复评估暴露了不可靠的 agent 行为。 - [SWE-Lancer](https://arxiv.org/abs/2502.12115)：前沿模型可能会在真实的软件任务中默默失败。 - [SWE-bench Verified](https://openai.com/index/introducing-swe-bench-verified/)：展示了为什么基准/任务筛选很重要。 - [SWE-bench Verified 退役分析](https://openai.com/index/why-we-no-longer-evaluate-swe-bench-verified/)：促成了声明范围和 oracle 对齐回执的产生。 ### 步骤级验证 - [Let's Verify Step by Step](https://arxiv.org/abs/2305.20050)：支持基于过程的证据，而非仅仅依赖二元化的最终结果。 - [Lost in the Middle](https://arxiv.org/abs/2307.03172)：促成了分块回执，而不是进行庞大上下文的审查。 ### LLM 评估器的局限性 - [自我偏好偏差](https://arxiv.org/abs/2410.21819)：警告不要信任模型的自我判断。 - [LLM 评估器中的位置偏差](https://arxiv.org/html/2406.07791v9)：促成了谨慎的评论家设计。 - [Don't Judge by Its Cover](https://arxiv.org/abs/2505.16222)：评论家们的共识是信号，而不是证明。 - [CodeJudge](https://arxiv.org/abs/2410.02184)：作为专门的审查信号很有用，但绝不能作为唯一的把关者。 ### 幻觉检测 - [CodeHalu](https://arxiv.org/abs/2405.00253)：支持代码幻觉分类。 - [Collu-Bench](https://arxiv.org/html/2410.09997v1)：促成了超越语法失败范围的检测。 - [Delulu](https://arxiv.org/abs/2605.07024)：涵盖了虚构的 API、无效参数、未定义的变量和不存在的 import。 ### 变异和测试质量 - [Just et al., FSE 2014](https://homes.cs.washington.edu/~mernst/pubs/mutation-effectiveness-fse2014.pdf)：变异测试与真实的错误检测相关联。 - [Papadakis et al., ICSE 2018](https://dl.acm.org/doi/pdf/10.1145/3180155.3180183)：变异测试有用，但并不完美。 - [LLMorpheus](https://arxiv.org/abs/2404.09952)：将变异风格的测试与 LLM 生成的代码缺陷联系起来。 - [mutmut](https://mutmut.readthedocs.io/en/latest/)、[StrykerJS](https://stryker-mutator.io/docs/stryker-js/incremental/) 和 [cargo-mutants](https://mutants.rs/timeouts.html)：分别用于、TypeScript 和 Rust 的实用引擎。 ### 模糊测试和差分测试 - [Fuzz4All](https://arxiv.org/abs/2308.04748)：展示了广泛的模糊测试增益。 - [代理式基于属性的测试](https://arxiv.org/html/2510.09907v1)：促成了带有可重放证据的生成式属性检查。 - [CodaMosa](https://dl.acm.org/doi/10.1109/ICSE48619.2023.00085)：支持基于搜索的测试用例扩充。 - [Metamorphic Prompt Testing](https://arxiv.org/abs/2406.06864)：在难以进行直接断言时，推动了蜕变关系的应用。 - [Hypothesis](https://hypothesis.readthedocs.io/en/latest/reference/api.html) 和 [fast-check](https://fast-check.dev/docs/introduction/why-property-based/)：生产级的属性测试引擎。 ### 供应链证明 - [SLSA](https://slsa.dev/spec/)：溯源和构建完整性框架。 - [Sigstore](https://docs.sigstore.dev/cosign/signing/overview/)：无密钥签名和基于透明度的身份认证。 - [in-toto](https://in-toto.io/)：供应链证明框架。 - [GitHub artifact 证明](https://docs.github.com/en/actions/concepts/security/artifact-attestations)：实用的 CI 原生签名溯源。 - [Nix 可重复性研究](https://arxiv.org/pdf/2501.15919)：明确了关于逐位可重复性的诚实边界。 ## 为什么 Pramaan 与众不同 大多数工具只提供一个单薄的信号： - CI 说命令通过了。 - 覆盖率说代码被执行了。 - 评论家说补丁看起来合理。 - 扫描仪说发现或没有发现某一类问题。 Pramaan 将这些结合成一个风险感知的证据 bundle。其价值不在于任何单一的检查，而在于这本账簿： - 声明了什么； - 检查了什么； - 有什么证据支持； - oracle 发生了什么变化； - 跳过了什么； - 还存在什么风险； - 在签名元数据可用时，记录了是谁/什么签名或生成了该 bundle，以及时间。 ## 目标用户 Pramaan 适用于期望 AI agent 贡献生产级代码的团队： - 采用编程 agent 的工程负责人； - 构建代码审查门控的平台团队； - 需要为 AI 生成的变更提供审计轨迹的安全团队； - 审查 AI 生成 PR 的开源维护者； - 在合并自动化代码之前需要证据的企业。 ## 仓库导航 - [crates/pramaan-cli](crates/pramaan-cli)：CLI 入口点和阶段命令。 - [crates/pramaan-core](crates/pramaan-core)：回执、声明范围、风险和共享模型。 - [crates/pramaan-sandbox](crates/pramaan-sandbox)：工作树和环境证据。 - [crates/pramaan-bundle](crates/pramaan-bundle)：bundle 清单、哈希、签名元数据和验证。 - [schemas](schemas)：公开的 JSON Schemas。 - [docs](docs)：产品和操作者文档。 - [examples](examples)：fixture、演示和合成回执。 - [plugins](plugins)：语言插件计划和适配器。 - [.planning](.planning)：GSD 规划、需求、研究和阶段验证。 ## 快速开始 使用默认阶段集（声明范围、沙箱、静态检查、oracle 完整性、差分模糊测试）验证 PR 的 diff： ``` cargo run -p pramaan-cli -- verify \ --base origin/main --head HEAD \ --out target/pramaan ``` 添加变异测试（较慢，可选择启用）： ``` cargo run -p pramaan-cli -- verify \ --base origin/main --head HEAD \ --out target/pramaan \ --with-mutation ``` 快速迭代：跳过你目前不需要的阶段： ``` cargo run -p pramaan-cli -- verify \ --base origin/main --head HEAD \ --out target/pramaan \ --skip-stage static_checks --skip-stage fuzz ``` 可选的 CI 归因 —— 设置这些环境变量以记录是哪个 AI 编程 agent 生成了变更。默认情况下不设置；也绝不进行推断： ``` export PRAMAAN_AGENT_PRODUCT="Codex" export PRAMAAN_AGENT_MODEL_FAMILY="gpt-5" export PRAMAAN_AGENT_MODEL_VERSION="..." export PRAMAAN_AGENT_EXECUTION_MODE="ci_pull_request" export PRAMAAN_AGENT_SOURCE="github_actions" ``` 验证工作区： ``` cargo fmt --all -- --check cargo clippy --workspace --all-targets -- -D warnings cargo test --workspace -- --test-threads=1 ``` ## 文档 - [Tasks to Serious v1](TASKS.md) - [回执模型](docs/receipt-model.md) - [风险分类法](docs/risk-taxonomy.md) - [Bundle 验证](docs/bundle-verification.md) - [认证](docs/attestation.md) - [GitHub Action](docs/github-action.md) - [杀手级演示](docs/demo.md) - [研究索引](docs/RESEARCH_INDEX.md) - [声明审计](docs/claim-audit.md) - [路线图](.planning/ROADMAP.md) ## 许可证 Pramaan 基于 MIT 许可证授权。详见 [LICENSE](LICENSE)。

标签：AI代码审查, DevSecOps, Rust, 上游代理, 可视化界面, 可验证凭证, 测试审计, 网络流量审计, 软件供应链, 通知系统