# ProofForge

**Repository Path**: to-mingwen/proof-forge

## Basic Information

- **Project Name**: ProofForge
- **Description**: 可信 AI 软件工厂 —— 让 AI 生成的每一行代码都有据可查
- **Primary Language**: Unknown
- **License**: Apache-2.0
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 4
- **Forks**: 0
- **Created**: 2026-10-09
- **Last Updated**: 2026-10-21

## Categories & Tags

**Categories**: ai

**Tags**: ai-coding-agent, ai-coding-agent-llm-e2e-testing, llm, e2e-testing

## README

# ProofForge

[![CI](https://img.shields.io/badge/CI-Gitee%20Go-28a745)](https://gitee.com/to-mingwen/proof-forge/pipelines)
[![star](https://gitee.com/to-mingwen/proof-forge/badge/star.svg)](https://gitee.com/to-mingwen/proof-forge)

[English](#overview) · [中文](#the-verifier-native-agentic-software-factory)

## Overview

**ProofForge is a verifier-native agentic software factory.** It turns a natural-language requirement into a running web application — and produces a defensible evidence chain for every claim. **AI writes the code; ProofForge proves it works.**

Generic coding agents treat AI output as a deliverable. ProofForge treats it as a **hypothesis to be verified**: every generated app is compiled against a structured requirement contract, launched for real, exercised in a real browser with Playwright, and auto-repaired until it passes — with a quantified evidence score attached.

| | Generic coding agents | ProofForge |
|---|---|---|
| AI output | Deliverable | **Hypothesis to verify** |
| Verification | None or manual | **5-layer stack, fully automated** |
| Failure handling | Manual debugging | **Diagnose → targeted repair → re-test (budgeted loop)** |
| Deliverable | Code | **Code + evidence chain + score** |

### Architecture

![ProofForge architecture: 8-stage pipeline, decision layer vs model layer, and the budgeted repair loop](docs/screenshots/architecture.png)

Left: the 8-stage pipeline, each stage annotated with the module that actually implements it. Right: the **decision layer** — write gates, the monotonic metric gate with best-checkpoint rollback, and the 5-dimension score — all deterministic Python. The model layer only writes and patches code; it never grades itself. The dashed orange arrow is the budgeted repair loop, which routes a failed test round back to source rather than back to regeneration.

The repair prompt opens with a **fact ledger**: a deterministic cross-comparison of the trace request/response bodies, the on-disk data files and the route blueprint (e.g. "the register request carried `email`; the stored record carries `id, username, password`"). Facts come before deductions — when the attribution card and the ledger disagree, the ledger wins.

Text-only version:

```
Requirement (YAML)
  → Contract compilation (UI / API / FUNC / DB)
  → Backend & frontend generation (deterministic shell + parallel view workers)
  → Real runtime verification (Node.js server + real browser, Playwright E2E)
  → Failed? → structured evidence → targeted repair → re-test (budgeted loop)
  → PASS / FAIL with Evidence (5-dim score, pass^k stability, Wilson bounds)
```

### Quick Start

```bash
git clone https://gitee.com/to-mingwen/proof-forge.git && cd proof-forge
cp .env.example .env          # set ARK_API_KEY (any OpenAI-compatible provider)
pip install -r requirements.txt
cd web && npm install && npm run build && cd ..
uvicorn src.api.server:app --host 0.0.0.0 --port 8080
```

Or run the bundled example directly from the CLI:

```bash
python main.py --requirement-dir todo/ticket-booking-extracted/ticket-booking--ticket-booking \
               --output-dir output --human-tests tests/human
```

Validated end-to-end on a full Chinese ticket-booking requirement: the focused-repair loop converged from a 0/10 baseline to **10/10 passing** human E2E tests (expected=10, unexpected=0, flaky=0). Artifacts and per-round evidence are generated at run time into `output/` (gitignored). Due to model stochasticity we don't guarantee 10/10 on every run — we guarantee **convergence**: the repair loop keeps pushing pass counts toward full pass, fully traceable.

### Documentation (Chinese)

| Doc | Content |
|-----|---------|
| [deploy/USER_GUIDE.md](deploy/USER_GUIDE.md) | Step-by-step user guide |
| [deploy/作品介绍_ProofForge.md](deploy/作品介绍_ProofForge.md) | Product positioning & design |
| [docs/evidence.md](docs/evidence.md) | Evidence chain & scoring |
| [docs/repair-evidence-research.md](docs/repair-evidence-research.md) | Repair-time evidence supply: survey & design (Chinese) |
| [ROADMAP.md](ROADMAP.md) | v0.2 → v1.0 plans |
| [docs/adr/](docs/adr/) | Architecture decision records |

License: Apache-2.0

---

## The Verifier-Native Agentic Software Factory

**验证优先的自主软件工厂** — 从自然语言需求到可验证软件的 Agentic Engineering 平台

> 2026 年 5 月，Gartner 发布首份 *Magic Quadrant for Enterprise AI Coding Agents*，用 "Enterprise AI Coding Agents" 取代了沿用多年的 "AI Code Assistants" 品类。新品类的定义是：**"autonomous or semiautonomous software engineering solutions that perceive context, translate human intent into multistep plans, and execute and verify those steps across code, tests, and related engineering artifacts."**
>
> ProofForge 从第一天起就按这个标准构建 —— 并把行业普遍缺失的最后一环 **Verify** 做成了产品的核心：不是"跑一下测试"，而是需求契约校验、真实运行时、真实浏览器、结构化证据链组成的**防幻觉验证栈**。

**AI 负责开发，ProofForge 负责证明。**

## 行业坐标

软件工程 AI 正沿四级阶梯演进：

```
AI Coding Assistant   →   Vibe Coding   →   Agentic Engineering   →   Autonomous Work Execution
（补全代码）               （生成应用）        （对工程任务负责）           （对结果负责）
```

| 能力维度 | Vibe Coding 平台<br>(Lovable / Bolt / v0) | 通用 Coding Agent<br>(Copilot / Cursor / Devin) | **ProofForge** |
|---------|----------------|----------------|----------------|
| 需求理解 | Prompt 即需求 | Prompt + 代码库上下文 | **结构化需求编译**：UI/API/FUNC/DB 四层契约 + 接口矩阵 |
| 测试 | 人工或无 | 辅助生成 | **自动生成**（DSL 结构化用例 + Playwright E2E） |
| 验证 | 预览即交付 | 多数不验证 | **真实启动 + 真实浏览器 + 契约比对** |
| 失败处理 | 人工返工 | 人工排查 | **自动诊断 → 定向修复 → 重测**（预算化循环） |
| 结论可信度 | "看起来能跑" | "大概率没问题" | **PASS/FAIL with Evidence**（5 维量化评分） |
| 监督自治 | 无 Harness | 部分 | **确定性 Harness**：模型无法给自己放水 |

核心区别：通用 Coding Agent 把 AI 输出当**产物**，ProofForge 把 AI 输出当**待验证的假设**。

## Core Goals

- **Trustworthy** — AI 输出默认不可信，经契约校验、真实启动、浏览器验证后才给结论
- **Traceable** — 全链路事件流 + 逐文件可追溯的证据体系
- **Reproducible** — Reproducibility Manifest 记录需求 hash、模型配置、依赖与产物，同输入可复盘

## Architecture Highlights

### 确定性 Harness（Supervised Autonomy）

LLM 在受约束的软件 Harness 内工作，关键决策不由模型自由发挥：

- **结构化测试 DSL** — 测试以 schema 校验的 DSL 表达，模型永远不能写自由脚本让自己通过
- **写盘门禁** — 修复产物经语法校验 + 模块系统一致性检查后才落盘，无效修复直接拒收
- **架构守护** — 修复可干净翻转前端架构（SPA↔多页），但禁止架构混合；目标文本缺失的修复直接拒收
- **确定性前端外壳与分视图生成** — SPA 骨架（路由/导航/API helper/会话恢复）由代码模板生成而非模型自由发挥；模型只按页面路由并行生成视图（4 worker），生成后真实启动应用逐路由冒烟并以交互探针实测表单链路（探针自身崩溃不再吞掉证据），失败视图定向重生
- **停滞检测与预算控制** — 重复错误自动熔断，修复循环受预算约束，杜绝失控重试

### 多模型编排运行时（Multi-Model Orchestration Runtime）

三角色模型路由（生成/修复、视觉分析、测试生成）之上，叠加生产级韧性层：

- **对冲请求（Hedged Requests）** — 主请求超时未响应即补发相同请求，谁先出内容谁赢，长尾等待缩短 80%+
- **Chunk 看门狗** — 流式响应断流/慢滴流自动检测并重试，慢实例不拖垮整条流水线
- **滑动窗口速率门控** — 产出速率低于阈值连续触发即断流换道，而非无限等待

### 防幻觉验证栈（Hallucination-Resistant Verification Stack）

五层验证，每层独立于模型：

```
需求契约校验 → 种子数据契约 → 测试覆盖矩阵 → 真实运行时（HTTP + Playwright）
     → 结构化失败证据（URL/选择器/期望值/实际值）→ 定向修复
```

- **UI 词条分类器** — 从中文需求中甄别"必须逐字出现的 UI 文本"与行为约束，杜绝误判引发的死循环
- **修复期事实层** — trace 请求体 / 响应体 / 磁盘存储 / 路由蓝图四源交叉比对，把"注册请求带了 email、落库记录只有 id/username/password"这类观测事实直接摆到修复 prompt 顶部（事实优先于归因卡）。四道防误报闸：按 trace 分组（防跨测试夹具碰撞）、凭据键永不回报、存储行归属需值重叠、同拼写 401 不归因读路径。零模型调用，不参与打分
- **失败证据结构化** — 浏览器失败自动生成最小可定位上下文（而非整个 HTML），修复模型拿到的是"靶点"而非噪声；测试运行时同步记录每个 `/api` 调用的请求体与响应体（`api_detail` 保留完整 body），失败时直接呈现「接口收发了什么」，而非只有 UI 文案与 timeout
- **运行时透明化** — 后端启动失败自动捕获 stderr 尾部拼入错误信息，修复模型看到真实报错而非盲修
- **API 失败证据链** — 浏览器测试期间自动采集后端 5xx 崩溃与 404 未挂载路由的响应体和后端 stderr 尾部，诊断器据此把后端文件纳入修复疑似集合，后端 bug 不再被误判成前端问题

## How It Works

双引擎协作：Agent 引擎以测试驱动的方式生成与修复，Platform 引擎全程记录与验证。

分层架构与判定权归属见上方 [Architecture](#architecture) 图：左列 8 段主管线逐段标注真实模块，右列拆分「确定性判定层」与「模型层」，橙色虚线为预算化修复回路。

```
需求解析 → 需求契约(UI/API/FUNC/DB) → 测试预期
      → 路由蓝图（先于生成的权威 API 路由表，三端单一事实源）
      → 后端生成 → 前端生成 → 生成期蓝图自检（机械对齐/一票否决）
      → 构建/启动检查
      → 真实浏览器执行 Playwright E2E
      → 失败？→ flaky 复核（单次失败隔离重放，重放即过不烧预算）→ 诊断 → 生成补丁 → 重测（有限预算循环）
      → 通过/预算耗尽 → 证据链 + 评分报告
```

## Features

- **需求契约驱动**：从 YAML 自动提取四层接口定义，作为生成与验收标准
- **TDD 式 Agent**：先定测试场景（DSL 正/负向用例），再写代码，用测试驱动修复
- **真实运行时验证**：实际启动 Node.js 后端 + 真实浏览器执行 E2E，非 mock、非静态扫描
- **多层自动修复**：契约修复、构建/启动修复、浏览器场景修复，补丁经语法与架构守卫后才落盘；补丁锚点在磁盘上找不到时自动回喂文件真值（`ANCHOR MISS FEEDBACK`），模型不再对着幻觉锚文本空转烧轮次
- **跨层 API 契约审计**：静态比对前端调用（含 body 字段键）、后端路由与 handler 必填字段、存储读写形状、响应形状（蓝图响应契约 vs handler `res.json` 字面量键级比对）、前端 localStorage/sessionStorage 跨视图键名漂移；缺口以「缺口卡片 + 兄弟路由填空模板」逐轮注入修复 prompt，被回滚补丁引入的新缺口经补丁态审计差集（CARRIED OVER）同样可见，消除「审计慢一拍」的原地打转
- **跨阶段蓝图裁决**：路由蓝图落盘 `.proofforge/route_blueprint.json`，每个 API 路由声明成功响应键（response 契约，session 路由必须含 token；数据路由未声明同样定向重试），修复期契约审计加载为第一优先方向裁决——生成与修复对同一参照系仲裁；shell 路由清单生成期锚定，修复轮改写过 shell 即降级不可信；数据文件（`backend/data/*`）触碰即拒，杜绝把期望值塞进初始数据的作弊路径
- **失败侧环境硬化**：单次失败自动隔离重放 1 次（timeout 类优先），重放即过记为 flaky 并保留 traceability 信号（`flaky_replays`：重放后仍失败与从未重放可区分），不烧修复预算；蓝图解析带确定性截断修复层，max_tokens 截断不再让权威路由表整体丢失
- **人工测试确认**：支持导入人工编写的 Playwright 测试作为最终验收标准；存在时自动替代 AI 生成测试，驱动修复循环
- **证据链与评分**：5 维评分（需求覆盖 / 测试覆盖 / 验证通过 / 可追溯 / 可复现；有人工测试时追加 `human_test_confirmation` 维度）
- **可观测**：Web 界面实时流水线、事件时间线、运行列表（Web+CLI 统一视图，5 秒刷新，可删除）；`.proofforge/traceability/` 全量 JSON 留痕
- **自托管友好**：本地 / Docker 部署，数据不出域；不捆绑模型厂商

生成目标：Node.js + Express 后端，HTML/CSS/原生 JS 前端，Playwright E2E 测试。

## Quick Start

### 环境要求

- Python 3.12+
- Node.js 18+（LTS 推荐）

### 本地启动

```bash
git clone <repo>
cd ProofForge

# 1. 配置环境变量
cp .env.example .env
# 在 .env 中填入 ARK_API_KEY

# 2. 安装依赖
pip install -r requirements.txt
cd web && npm install && npm run build && cd ..

# 3. 启动 API 服务
uvicorn src.api.server:app --host 0.0.0.0 --port 8080
```

- API 文档：http://localhost:8080/docs
- Web UI（开发模式另开）：`cd web && npm run dev` → http://localhost:3000

### Docker 启动

```bash
cp .env.example .env   # 填入 ARK_API_KEY
docker compose up -d
```

启动后浏览器打开 `http://localhost:8080`（Web UI 与 API 文档同端口，无需另开前端服务）。

### Web UI 界面

**首页 — 提交需求**：输入项目名与需求描述，一键启动「生成 → 运行时验证 → 修复」全流程。

![ProofForge 首页：提交需求](docs/screenshots/1.png)

**运行列表**：追踪每次 Run 的状态（运行中 / 已结束）、结论（PASS / FAIL）、评分与来源，支持查看运行详情与下载验证证据。

![ProofForge 运行列表](docs/screenshots/2.png)

**API 文档**：内置 OpenAPI 3.1 交互式文档（`/docs`），项目创建、Run 启停、证据获取等全部能力可直接在浏览器里试调。

![ProofForge API 文档](docs/screenshots/3.png)

### 命令行直接跑一个需求

```powershell
python -u -X utf8=1 main.py `
  --requirement-dir "需求目录(含 requirements.yaml)" `
  --output-dir "输出目录"
```

导入人工测试作为最终验收标准（可选）：

```powershell
python -u -X utf8=1 main.py `
  --requirement-dir "需求目录" `
  --output-dir "输出目录" `
  --human-tests "人工测试目录(含 .spec.ts + playwright.config.ts)"
```

> 人工测试存在时，自动跳过 AI 测试生成，以人工测试驱动修复循环。不存在时走 AI 生成路径，零影响。

## Models：更换或不使用 AI

ProofForge 通过标准 **OpenAI 兼容接口**（`/chat/completions`）调用模型，三个角色可独立配置：

| 角色 | 环境变量 | 默认模型 |
|------|---------|---------|
| 主模型（生成/修复） | `OPENAI_BASE_URL` + `MODEL` | deepseek-v4-flash |
| 视觉模型（截图分析） | `VISUAL_BASE_URL` + `VISUAL_MODEL` | qwen3.8-max |
| 测试模型（用例生成） | `TEST_GENERATOR_BASE_URL` + `TEST_GENERATOR_MODEL` | Qwen3-Coder-Flash |

- **换供应商**（如 DeepSeek 官方 / Kimi / 任何 OpenAI 兼容服务）：改 `ARK_API_KEY` + `OPENAI_BASE_URL` + `MODEL` 三行，重启即可
- **离线模式**：留空 `ARK_API_KEY`，自动降级为内置 Mock 适配器，全流程可跑通（产出为占位响应，适合体验与 CI 冒烟）
- 流式调用内置卡顿看门狗与自动重试；思考模式按角色开关（`MODEL_ENABLE_THINKING` / `TEST_GENERATOR_ENABLE_THINKING`）。**所有角色默认关闭思考（2026-10-19 起）**，需要时用 `=1` 显式开启（实测部分网关会静默忽略 `enable_thinking` 参数，改用 `thinking:{"type":"disabled"}` 字段才真正生效——复杂生成任务不再出现数万字符空转推理）。**根因修正（2026-10-19）**：此前「网关连 disabled 也忽略」的观察实为 gitee ai 网关 bug——payload 携带 `stream_options:{include_usage:true}`（usage 统计）时 disabled 会被静默忽略；已修复为禁思考的 main 请求跳过 stream_options（usage 按字符估算回填，报告用途），蓝图等阶段思考真正关闭，调用失败自动重试而非静默降级。**默认值修正（2026-10-19，run 1019g）**：代码默认值此前仍是开（文档与代码不同步，裸启动静默重开思考导致蓝图 runaway 双烧）——现默认值翻转为关，与文档承诺一致

完整配置说明与示例：[deploy/USER_GUIDE.md](deploy/USER_GUIDE.md) 第八章。

## Documentation

| 文档 | 内容 |
|------|------|
| [deploy/USER_GUIDE.md](deploy/USER_GUIDE.md) | 傻瓜式使用手册：安装、运行、日志排障、`.proofforge` 文件详解、模型切换 |
| [deploy/作品介绍_ProofForge.md](deploy/作品介绍_ProofForge.md) | 产品定位、双引擎设计、与 Copilot/Devin/Cursor 的差异、开源合规 |
| [docs/architecture.md](docs/architecture.md) | 系统架构 |
| [docs/demo.md](docs/demo.md) | 演示流程 |
| [docs/development.md](docs/development.md) | 开发指南 |
| [docs/evidence.md](docs/evidence.md) | 证据链与评分体系 |
| [docs/repair-evidence-research.md](docs/repair-evidence-research.md) | 修复期证据供给：同类项目调研与「证据阶梯」方案 |
| [docs/reproducibility.md](docs/reproducibility.md) | 可复现性设计 |

## Validation

平台已在完整中文需求（车票预订系统 ticket-booking：注册/登录/车次搜索/预订，需求包见 `todo/ticket-booking-extracted/`）上完成端到端验证：自动生成前后端与 Playwright 测试，真实启动并在浏览器中执行验证。以 10 条人工 E2E 用例（`tests/human/`）为验收标准，聚焦修复循环从 0/10 基线自主收敛至 **10/10 全通过**（Playwright stats：expected=10, unexpected=0, flaky=0），产物与逐轮证据由运行生成写入 `output/`（已 gitignore）。

> 由于模型生成存在随机性，不确保每次生成都达到 10/10 通过；我们保证的是**收敛性**——修复循环以人工用例为裁判，持续把通过数推向 10/10。详见 [docs/evidence.md](docs/evidence.md)。

## Roadmap

版本化路线图（v0.2 → v1.0：大任务编排、生成目标扩展、多模型适配层、企业部署与社区治理）见 [ROADMAP.md](ROADMAP.md)。当前焦点：

| 优先级 | 方向 | 说明 |
|------|------|------|
| P0 | 聚焦修复对大任务的处理 | 从单节点推广到多节点 / 大型需求树的编排与并行修复 |
| P1 | 压缩生成时间 | 在保持性价比的前提下压缩端到端生成与修复耗时（并行生成、缓存复用、更聪明的重试策略） |
| P2 | 持续优化评分体系 | 当前评分偏严格（小样本 Wilson 下界、断言级覆盖等保守机制），持续校准评分与实际质量的偏差 |

## License

Apache-2.0