---

💡 Why Trace?

When Autonomous AI Agents write and execute software today, they suffer from three fundamental limitations:

1. Context Window Token Bloat: LLMs waste 50% to 80% of tokens reading entire files and massive 50-line traceback dumps just to fix a single bug.
2. Crash Inconsistency & Duplicate Side Effects: When an agent's multi-step execution crashes mid-way (e.g., API timeout or server restart), external effects are leaked, payments double-charged, or compensation order broken.
3. Multi-Agent Collision (Lost Updates): Text-based Git diffs fail when multiple agents collaborate on the same file, resulting in torn ASTs and merge conflicts.

Trace solves this at the language and runtime foundation:

• 🛡️ Durable Sagas: Mathematically proven reverse compensation order, process crash recovery (os._exit resilient), and failure blockades.
• 🌳 Persistent AST Identity & CAS: Every syntax node has a stable cryptographic UUID and content hash. Updates apply via Compare-And-Swap (0% lost updates).
• 🎯 Sub-Millisecond Counterexample Shrinking: Automatically isolates minimal failing inputs in 0.3ms, cutting diagnostic tokens by 77% and achieving single-turn Pass@1 bug repairs.
• 📐 Mechanically Verified in Lean 4: 27 core theorems proved with zero unreviewed axioms and zero sorry.

---

🎯 现实中怎么用？开发所有项目都要用它吗？

When Should I Use Trace? (And When Shouldn't I?)

tl;dr 核心结论：绝对不要所有项目都用它，你完全不需要推翻重写现有的项目！
90% 的普通业务逻辑（写网页界面、查数据库列表、做数据分析）继续用你熟悉的 Python/Go/JS/Vue；只有那 10% 最核心的“AI Agent 调度、多步外部 API 扣费/发货、容灾防重复” 的高危链路，交给 Trace 守护。

┌────────────────────────────────────────────────────────────────────────┐
│                   你的现有项目 (FastAPI / Django / Go)                  │
│                                                                        │
│   常规业务接口 (90%)                       高危交易 / AI Agent 任务 (10%) │
│   ┌───────────────────────────┐           ┌──────────────────────────┐ │
│   │ 查列表、展示数据、写网页   │           │ 多步扣费、调度外部 API   │ │
│   │ 普通 Python / Vue 代码    │           │ 用 Trace @flow 守护      │ │
│   └───────────────────────────┘           └────────────┬─────────────┘ │
└────────────────────────────────────────────────────────┼───────────────┘
                                                         │
                                           ┌─────────────▼───────────────┐
                                           │ Trace Lens 本地可视化控制台 │
                                           │ (http://127.0.0.1:8080)     │
                                           └─────────────────────────────┘

🌟 适用场景：它在什么时候是“救命稻草”？

1. 场景 1：AI Agent 复杂多步外部调用（核心痛点：崩溃防重与自动回滚）

   • 典型业务：Agent 执行 “抓取数据 ➔ 扣除用户 50 积分 ➔ 调用外部模型 ➔ 发送短信通知”。
   • 痛点：普通 Python 代码一旦在第 4 步发短信时网络超时，由于已经扣了 50 积分，重试就会导致**“重复扣费 100 积分”；不重试就会导致“扣了费没发短信”**。
   • Trace 怎么解决：用 @flow 包装。Trace 自动落盘事务日志，断电重启自动断点续跑；若短信彻底失败，严格按数学反向顺序自动触发退款回滚，0 重复扣费，0 坏账。

2. 场景 2：让 AI 程序员（Cursor / Devin / 自动化 Agent）修代码

   • 典型业务：让 AI 自动给已有系统找 bug 并打补丁。
   • 痛点：传统 Python 报错会丢出 50 行堆栈，消耗巨量 Token 且 Agent 容易改错；如果有 2 个 Agent 同时改代码，还会把彼此的代码直接覆盖（Lost Update）。
   • Trace 怎么解决：用 trace agent-ce 在 0.3毫秒内把报错精准收缩成最小输入（例如：输入为 0 时越界），Token 消耗降低 77%；提交补丁使用 AST 密码学 CAS，冲突直接拦截，绝不会互相覆盖。

3. 场景 3：金融/电商/审批等高敏感交易链条

   • 典型业务：跨系统的订单支付、库存锁定、优惠券核销。
   • 痛点：手写 try-catch、防重表和分布式回滚极容易出 bug。
   • Trace 怎么解决：底层经过 Lean 4.35.0 形式化机械证明（27项定理），从数学公理上保证“只要补偿失败就强制封锁告警，绝不假装成功”。

🚫 哪些场景绝对不要用它？

• ❌ 不要用来写网页前端（UI）：做页面请继续用 Vue/React。
• ❌ 不要用来做大模型矩阵计算或极低延迟网关：做张量计算用 PyTorch/CUDA，做微秒级通信用 C++/Rust。
• ❌ 不要用来写简单的一次性脚本：如果只是写一个爬虫、或者转个 Excel 文件，普通的几行 Python 脚本是最快的，引入形式化事务属于过度设计。

---

📊 Feature Comparison

Capability	Raw Python / JS	Temporal / Cadence	LangGraph / CrewAI	Trace
Crash-Safe Multi-Step Saga	❌ Manual	✅ Yes (Heavy Server)	❌ Memory-only	✅ Built-in & Lean 4 Proven
Zero Side-Effect Leaks on Crash	❌ No	✅ Yes	❌ No	✅ 100% Guaranteed
AST-Level Compare-And-Swap (CAS)	❌ Text Diffs	❌ N/A	❌ N/A	✅ Cryptographic AST Identity
Sub-Millisecond Counterexample Shrinking	❌ Raw Tracebacks	❌ N/A	❌ No	✅ 0.3ms Minimal Inputs
Context Window Token Savings	0%	0%	0%	✅ 53.3% - 80%+ Reduction
Runtime Overhead & Dependencies	Low	Heavy Cluster	Medium	Zero External Dependencies

---

🚀 Quickstart in 5 Minutes

Trace adopts a Progressive Adoption Ladder: start directly in your existing Python codebase with zero rewrite, or use the dedicated .trace DSL.

Level 0: Python Decorator SDK (@flow & @contract)

No new syntax required! Import Trace directly into your Python service:

from trace_lang import flow, contract

# 1. Add contracts with automatic property fuzzing
@contract(
    requires=lambda price: price >= 0,
    ensures=lambda result, price: result >= 0
)
def calculate_discount(price: int) -> int:
    return price - 50 if price > 100 else price

# 2. Define durable, crash-resilient multi-step Sagas
@flow(db_path="ecommerce.db")
def checkout_pipeline(ctx, order_id: str, amount: int):
    # If payment succeeds but license fails, payment is automatically refunded in reverse order!
    ctx.step("charge_card", forward=stripe_charge, undo=stripe_refund, payload=amount)
    ctx.step("provision_key", forward=generate_license, undo=revoke_license, payload=1)

# Execute or resume after crash
order = checkout_pipeline(run_id="order_9901", order_id="ord_9901", amount=150)
result = order.run()
print(f"Status: {result['status']}") # 'succeeded' or 'compensated'

Level 1: Launch Trace Lens Visual DevTools

Trace includes an embedded local web console for real-time transaction debugging and AST inspection:

# Launch interactive developer UI on http://127.0.0.1:8080
python -m trace_lang lens

(Interactive visual DAG of Sagas, compensation flows, AST lineage, and 0.3ms property fuzzing sandbox)

Level 2: Agent Tooling CLI (For Autonomous Coding Agents)

When an AI agent needs to inspect or patch code, use Trace's specialized CLI:

# 1. Get minimal dependency slice & hole info (saves >50% context tokens)
python -m trace_lang agent-context examples/orders.trace --target "fn.quote"

# 2. Find and shrink minimal counterexample
python -m trace_lang agent-ce examples/discount.trace --fn discount
# Output: {"status": "counterexample_found", "minimal_args": [0], "diagnostic": "E_CONTRACT"}

# 3. Apply atomic AST patch with revision check
python -m trace_lang patch examples/orders.trace patch.json --output patched.trace

Level 3: Pure .trace DSL & Formal Machine Checking

Trace programs express pure computation, typed contracts, and persistent UUIDs:

@revision(1)
@id("type.Cart")
type Cart = { items_count: Int, subtotal: Int }

@id("fn.apply_coupon")
fn apply_coupon(cart: Cart, discount: Int) -> Int
  require cart.subtotal >= 0 && discount >= 0
  ensure result >= 0
{
  if discount >= cart.subtotal then 0 else cart.subtotal - discount
}

Verify formal proofs with Lean 4:

python tools/check_formal.py --lean <path-to-lean-4.35.0>
# Output: {"status": "checked", "lean_theorems": 27, "admissions": 0}

---

📈 Benchmarks

Empirical performance evaluation from benchmarks/agent_efficiency/:

Metric	Baseline (Python/Git)	Trace Agent Engine	Gain
Context Window Consumption	2,840 bytes (full file)	1,326 bytes (dependency slice)	53.3% - 80%+ Saved
Diagnostic Traceback Size	822 bytes (stack trace)	188 bytes (shrunk counterexample)	77.1% Saved
Agent Repair Convergence	3 - 5 turns (trial & error)	1 turn (Pass@1)	3x Faster Convergence
Crash Side-Effect Leakage	Frequent duplicate API calls	0 leaked side effects	100% Mathematical Safety
Multi-Agent CAS Collision	Silent overwrite / torn AST	1 winner + E_ID_CONFLICT abort	100% Atomic Serialization

---

🏗️ Repository Architecture

├── trace_lang/               # Core Python implementation (Zero external dependencies)
│   ├── sdk.py               # Progressive Adoption SDK (@flow, @step, @contract)
│   ├── lens.py              # Trace Lens embedded local Web DevTools & API
│   ├── saga.py              # Crash-safe Saga coordinator & SQLite journal
│   ├── identity.py          # Persistent AST Identity CAS engine & lineage index
│   ├── agent_tools.py       # Context slicing, counterexample shrinking, atomic patches
│   ├── syntax.py            # Trace parser, lexer, and AST formatter
│   └── engine.py            # Runtime interpreter & contract evaluator
├── formal/                  # Lean 4.35.0 Formal Verification Proofs (27 Theorems)
│   ├── CoreTyping.lean      # Type uniqueness & preservation semantics
│   ├── Identity.lean        # Monotonic retirement & CAS safety theorems
│   └── Saga.lean            # Reverse compensation ordering & failure blockade
├── tests/                   # 188 Unit & Industrial Chaos Tests
│   ├── test_sdk.py          # Level 0 Python SDK tests
│   ├── test_lens.py         # Trace Lens devtools HTTP server tests
│   ├── test_saga_chaos.py   # os._exit crash, reverse replay, blockade & lock tests
│   └── test_identity_concurrency.py # Multi-process CAS stress tests
├── benchmarks/              # Agent efficiency & token savings benchmark suite
└── docs/                    # Architecture, SAGA model, and Open-Core strategy

---

📜 Open-Core & Commercial Strategy

Trace follows an Open-Core model:

• Community Core (Open Source, Apache 2.0): Single-node Saga coordinator, AST Identity, Python SDK, Agent CLI, and Trace Lens Community.
• Enterprise & Cloud (Commercial / BSL): Multi-node distributed Raft Saga cluster, tamper-evident cryptographic compliance gateway, enterprise RBAC/SSO, and Trace Lens Pro.

For full architectural breakdown and commercialization details, read docs/OPEN_CORE_STRATEGY.md.

---

🤝 Contributing

Contributions are welcome! Please read CONTRIBUTING.md and SECURITY.md before opening pull requests. All PRs touching core semantics must pass the Lean 4 formal gate.

---

📄 License

Trace is open-source software licensed under the Apache 2.0 License.