基于形式化 λA 演算的智能体编程语言 + PaaS 执行平台
三条主线: 理论技术(形式化证明)→ 工程实现(可运行代码)→ 案例场景(真实部署)
lambdagentpaas 是目前唯一用形式化证明保证 Agent 组合安全、成本上界和终止性的平台。不同于其他框架"运行时试错"的方式,它让 Agent 先编译后执行——在运行前就能静态回答四个关键问题:
╔══════════════════════════════════════════════════════════════════════════╗
║ L3 应用层 — 真实案例场景 ║
║ ║
║ ┌─────────────────┐ ┌─────────────────┐ ┌─────────────────┐ ║
║ │ qaagent67wiki │ │ qaagent67lite │ │ agent67v2 │ │ research67│║
║ │ 海事法规问答 │ │ 轻量级问答 │ │ 编程助手 │ │ 科研助手 │║
║ │ │ │ │ │ │ │ │║
║ │ 1326 海事法规 │ │ BM25+Wiki │ │ 43 工具 │ │ 8 子智能体│║
║ │ Wiki v2 三步流程 │ │ 无需 Vector │ │ 6 子智能体 │ │ 论文+实验 │║
║ │ 持续生长+WikiGrow│ │ <500文档轻部署 │ │ Handoff + Skill │ │ 迭代优化 │║
║ └────────┬────────┘ └────────┬────────┘ └────────┬────────┘ ║
║ │ │ │ ║
╠═══════════▼═════════════════════▼═════════════════════▼══════════════════╣
║ L2 工程实现层 (agentpaas) ║
║ ║
║ ┌──────────────────────────────────────────────────────────────────┐ ║
║ │ REST API (28 端点) + MCP Server (5 工具) + GitHub Action │ ║
║ │ /agents /run /analyze /lint /cost /type-check /jobs │ ║
║ └────────────────────────────┬─────────────────────────────────────┘ ║
║ │ ║
║ ┌────────────────┬─────────────┴─────────────┬──────────────────┐ ║
║ │ Instance 机制 │ 双引擎执行层 │ 多租户 │ ║
║ │ │ │ │ ║
║ │ template/ │ ┌──────────────────────┐ │ RBAC + Quota │ ║
║ │ instance/ │ │ Recursive (Python栈) │ │ 审计日志 │ ║
║ │ workspace/ │ │ CEK Machine (Paper II)│ │ API Key │ ║
║ │ 深度合并 │ │ Adaptive (自动选择) │ │ │ ║
║ └────────────────┘ └──────────┬───────────┘ └──────────────────┘ ║
║ │ ║
║ ┌───────────────────────────────▼──────────────────────────────────┐ ║
║ │ Static Analysis — 四道编译时安全网 │ ║
║ │ ┌─────────┐ ┌─────────┐ ┌──────────┐ ┌──────────────┐ │ ║
║ │ │ Lint │→ │T-Compose│→ │Cost Pred │→ │ Store Indep. │ → 执行 │ ║
║ │ │26 规则 │ │类型检查 │ │分级类型 │ │Pair 汇合 │ │ ║
║ │ └─────────┘ └─────────┘ └──────────┘ └──────────────┘ │ ║
║ └────────────────────────────────┬─────────────────────────────────┘ ║
║ │ ║
╠════════════════════════════════════▼══════════════════════════════════════╣
║ L1 理论技术层 (lambdagent / λA 演算) ║
║ ║
║ ┌──────────────────────────────────────────────────────────────────┐ ║
║ │ from_config 编译器 │ ║
║ │ YAML → λA 项 → 类型化 AST → Engine 可执行 │ ║
║ └────────────────────────────┬─────────────────────────────────────┘ ║
║ │ ║
║ ┌────────────────┬─────────────┼─────────────┬─────────────────────┐ ║
║ │ Layer 3 │ Layer 2 │ Layer 1 │ 核心 λA 构造子 │ ║
║ │ Orchestration │ Pattern │ Skill │ │ ║
║ │ │ │ │ 11 单智能体: │ ║
║ │ YAML 声明式 │ review │ 原子能力 │ ├─ Lam (LLM) │ ║
║ │ 业务编排 │ fan_out │ 可复用 │ ├─ Tool (外部) │ ║
║ │ │ pipeline │ 带类型签名 │ ├─ Compose (>>) │ ║
║ │ │ escalation │ │ ├─ If (分支) │ ║
║ │ │ map_reduce │ │ ├─ Loop (Y组合子) │ ║
║ │ │ debate │ │ ├─ Route (case) │ ║
║ │ │ │ │ ├─ Pair/Fst/Snd │ ║
║ │ │ │ │ ├─ Guard (验证) │ ║
║ │ │ │ │ └─ Memory (状态) │ ║
║ │ │ │ │ │ ║
║ │ │ │ │ 5 多智能体: │ ║
║ │ │ │ │ GroupChat/Handoff │ ║
║ │ │ │ │ AsyncPar/Channel │ ║
║ │ │ │ │ SharedMemory │ ║
║ └────────────────┴─────────────┴─────────────┴─────────────────────┘ ║
║ ║
║ ┌──────────────────────────────────────────────────────────────────┐ ║
║ │ 形式化理论基础 (三篇论文) │ ║
║ │ │ ║
║ │ Paper I λA 类型系统 → 11 构造 + 26 lint + 类型安全定理 │ ║
║ │ Paper II 操作语义 → 23 规则 + CEK + 6 代数定律 + 汇合定理 │ ║
║ │ Paper III 类型与效果 → 15 类型规则 + 效果代数 + 分级类型 │ ║
║ └──────────────────────────────────────────────────────────────────┘ ║
║ ║
║ ┌──────────────────────────────────────────────────────────────────┐ ║
║ │ LLM Wiki 知识层 v2 (Karpathy 模式 + 持续生长) │ ║
║ │ index.md + sources/ + entities/ + topics/ + analyses/ │ ║
║ │ 三步流程: Ingest(交叉引用) → Query(多页综合) → Lint(自动修复) │ ║
║ │ WikiGrow 主动生长 | WikiStatus 健康评分 | 6 个工具 │ ║
║ └──────────────────────────────────────────────────────────────────┘ ║
╠══════════════════════════════════════════════════════════════════════════╣
║ L0 基础设施 (Infrastructure) ║
║ ║
║ LLM Providers (7) Storage Integration ║
║ Anthropic/OpenAI/Ollama SQLite/PostgreSQL MCP / A2A 协议 ║
║ DashScope/DeepSeek Redis/ChromaDB Git Worktree ║
║ Claude Code/Moonshot Filesystem Docker Sandbox ║
╚══════════════════════════════════════════════════════════════════════════╝
lambdagentpaas 的核心壁垒是三篇论文建立的形式化理论——这是其他框架无法快速复制的。
| 定理 | 内容 | 工程价值 |
|---|---|---|
| 定理 5.3 类型安全 | 良类型项要么规约到值,要么是受控 guard 失败 (Progress + Preservation) | Agent 组合不会出现"未定义行为" |
| 定理 5.4 有界终止性 | fix_n(λself. body) 在至多 n 步内终止 |
ReAct 循环保证不会无限跑 |
| 命题 30 Pair 汇合 | 在 writes(f) ∩ writes(g) = ∅ 下,Pair(f,g) 输出分布与调度顺序无关 |
并行 Agent 保证不冲突 |
Paper I — λA 类型化 Lambda 演算
11 个项构造子:
e ::= x | λx:τ. e | e₁ e₂ (标准 λ)
| e₁ >> e₂ (组合)
| if e₁ then e₂ else e₃ (条件)
| fix_n e (有界不动点)
| ⟨e₁, e₂⟩ | π₁e | π₂e (序对)
| tool[f] (外部神谕)
| case e of {l_i ⇒ e_i} (多路分发)
| guard e P (精化/验证)
| mem e σ (环境扩展)
| lam π θ (LLM 神谕)
Paper II — 操作语义 + CEK Machine
CEK 状态: ⟨C, E, K, σ, c⟩
C: 当前控制 (项或值)
E: 环境 (绑定)
K: 延续栈 (continuation)
σ: 存储 (memory)
c: 成本向量 (tokens, latency, money)
核心转移规则:
C-Lam (LLM Yield):
⟨lam π θ v, E, K, σ, c⟩ ═══Yield(llm)═══> ⟨str(r), E, K, σ, c+c_llm⟩
C-Tool (Tool Yield):
⟨tool[f] v, E, K, σ, c⟩ ═══Yield(tool)═══> ⟨f(v), E, K, σ, c+c_tool⟩
6 条代数定律 (Theorems 36-41):
1. 结合律: (f >> g) >> h ≡ f >> (g >> h)
2. 左单位: Id >> f ≡ f
3. 右单位: f >> Id ≡ f
4. 循环展开: Loop(b,c,n) ≡ If(c, Id, b >> Loop(b,c,n-1))
5. 路由分配: Route(c,{l_i:f_i}) >> g ≡ Route(c,{l_i:f_i >> g})
6. 对对称: Pair(f,g) ≡ swap ∘ Pair(g,f)
Paper III — 类型与效果系统
类型语法 (Definition 1):
τ ::= Str | Num | Bool | Json(S) | τ₁×τ₂ | τ₁ →^ε τ₂ | {x:τ | P(x)}
核心类型规则:
T-Compose:
Γ ⊢ f : A →^ε₁ B Γ ⊢ g : B' →^ε₂ C B <: B'
─────────────────────────────────────────────────────
Γ ⊢ f >> g : A →^{ε₁·ε₂} C
效果代数:
ε ::= pure | llm(m) | io | state(s) | ε₁·ε₂ | ε₁∥ε₂ | εⁿ
分级类型 (Graded Types) — 静态成本上界:
g = (p, t, l, m)
p ∈ [0,1] 成功概率下界
t ∈ ℕ token 消耗上界
l ∈ ℝ≥0 延迟上界 (秒)
m ∈ ℝ≥0 金钱成本上界 (美元)
组合规则:
g₁ · g₂ = (p₁·p₂, t₁+t₂, l₁+l₂, m₁+m₂) (串行)
g₁ ∥ g₂ = (p₁·p₂, t₁+t₂, max(l₁,l₂), m₁+m₂) (并行)
gⁿ = (pⁿ, n·t, n·l, n·m) (迭代)
把上述理论从论文转化为生产级 Python 代码。
lambdagent (核心 DSL) 11,300 LOC
├── primitives.py 11 个核心构造子
├── extensions.py Par, Route, Guard, Memory
├── multiagent.py 5 个多智能体构造
├── types.py 15 条类型规则实现
├── effects.py 效果代数
├── cost_grade.py 分级类型 + validate_cost
├── cek_machine.py Agent CEK Machine
├── rewrite.py 6 条代数定律 (rewrite 优化)
├── patterns.py 6 个协作模式
├── handlers.py Production/Test/Trace 处理器
├── fromconfig/
│ ├── compiler.py YAML → λA 编译器
│ ├── lint.py 26 条 lint 规则
│ └── schema.py YAML schema 校验
├── agentruntime/
│ ├── engine.py 统一 Engine 接口
│ ├── recursive_engine.py Python 调用栈引擎
│ ├── cek_engine.py CEK Machine 引擎
│ ├── adaptive_engine.py 自动选择引擎
│ └── react_engine.py ReAct 7 阶段循环
└── builtin_tools/ 52 个内置工具
├── file_tools.py ReadFile/EditFile/WriteFile/...
├── qa_tools.py QA Agent 工具 (qaagent67)
└── wiki_tools.py Wiki Agent 工具 (qaagent67wiki)
agentpaas (PaaS 层) 2,000 LOC
├── api/v1/ 28 个 REST 端点
│ ├── agents.py Agent CRUD + run + stream
│ ├── analyze.py 5 个 analyze 端点
│ └── jobs.py 异步 Job API
├── engine/
│ ├── instance.py Instance 机制 + 深度合并
│ └── dispatcher.py Sync/Async/Stream 分派
├── registry/ Agent 注册 + 版本 + 流量
├── tenant/ RBAC + Quota + 隔离
└── db/ SQLite/PostgreSQL (FIX-06 索引)
lambdagent_guard 400 LOC
├── core.py GuardConfig + RuntimeMonitor
├── langchain.py guard_langchain()
├── crewai.py guard_crewai()
└── autogen.py guard_autogen() + 终止修复
测试: 503 tests, 0 failed, 0 回归
双引擎可切换 — Recursive 快,CEK 安全,Adaptive 自动:
# YAML 配置
runtime:
engine: cek # recursive | cek | adaptive
costBudget: 5.00 # CEK 专属: 超额自动暂停
maxSteps: 10000
# Python API
result = Runtime.execute("config.yml", "input", engine_mode="cek", cost_budget=5.0)
Instance 机制 — 一个模板多个实例:
agentexample/qaagent67wiki/ ← 模板 (Git 跟踪)
agent-config.yml ← 默认配置
agentexample/instances/maritime/ ← 海事实例 (数据不跟踪)
instance.yml ← 路径覆盖 (深度合并)
wiki/ ← 累积知识
knowledge/ ← 原始文件
workspace/run_YYYYMMDD_HHMMSS/ ← 每次 run 隔离
Run Workspace — 每次执行完整隔离:
每次 POST /agents/{id}/run 自动创建:
{instance_dir}/workspace/run_20260406_001234/
├── input.txt
├── output.txt
├── trace.json
├── config.snapshot.yml
└── cost.json
永不删除历史 run, 可审计可回放
MCP Server — 一行配置接入 Claude Code / Cursor:
{ "mcpServers": { "lambdagent": { "command": "python3", "args": ["-m", "lambdagent.mcp_server"] } } }
暴露 5 个 MCP 工具: lint_agent_config, estimate_agent_cost, check_agent_types, check_parallel_safety, monitor_agent_cost
真实规模 (2026-04-06 运行数据):
📚 海事法规知识库
源文件: 1326 份海事法规和政策文件
摘要页: 508 个 sources/
实体页: 1410 个 entities/
├─ 机构类: 364 个 (交通运输部 150 refs, 海事局 45 refs, IMO 40 refs, ...)
├─ 概念类: 532 个 (行政审批/领海基线/适任证书/...)
├─ 法规类: 503 个 (海商法 8 refs, 海上交通安全法 7 refs, ...)
├─ 规章类: 4 个
└─ 地点/文件/网站: 6 个
主题页: 1073 个 topics/
├─ 船舶安全 (119 文档)
├─ 船员管理 (94 文档)
├─ 环境保护 (50 文档)
├─ 海洋环境保护 (31 文档)
├─ 船舶检验 (19 文档)
└─ ...
分析页: 1 个 analyses/ (查询结果自动回填)
技术栈:
model:
provider: ollama # 本地部署
name: qwen2.5:32b # 32B 本地模型
baseUrl: http://localhost:11434
runtime:
engine: cek # CEK 引擎 + 成本熔断
costBudget: 1.00
mcp:
localTools:
- WikiIngest # LLM 阅读 → 写 wiki 页面 → 更新索引
- WikiQuery # 读 index.md → 查 wiki 页面 → 回答
- WikiLint # 矛盾/孤页/断链检测
- WikiSearch # 关键词搜索
- WikiStatus # 统计信息
与传统 RAG 的差异:
| 维度 | 传统 RAG | qaagent67wiki (Karpathy 模式) |
|---|---|---|
| 喂文件 | 分块 → 向量库 | LLM 阅读 → 写 wiki 页面(摘要+实体+主题) |
| 提问 | 搜索碎片拼凑 | 读已编译的 wiki 页面 |
| 知识积累 | 不积累 | 越用越丰富,交叉引用持续增长 |
| 矛盾检测 | 无 | WikiLint 自动检查 |
| 可浏览性 | 向量库不可读 | Markdown 文件,Obsidian 可直接浏览 |
| 成本 | 每次查询消耗 LLM | Ingest 时一次性消耗,Query 时只读文件 |
架构: 协调者 + 6 个专业微代理,通过 Handoff + SkillRegistry 动态分派。
v1: λ = Memory(Loop(Brain >> Route(42 tools))) # 单体, 慢
v2: λ = Memory(Loop(Coordinator >> Handoff(Registry))) # 多智能体, 快
├─ code-agent (13工具: 文件/代码/Git)
├─ shell-agent (1工具: Bash)
├─ web-agent (10工具: 搜索/知识库/文档)
├─ memory-agent (17工具: 记忆/任务/调度/画像)
├─ system-agent (4工具: 浏览器/应用/系统/截图)
└─ researcher (17工具: 读论文→复现→实验→记录)
三大改进:
编译器扩展: from_config() 新增 subAgents 支持, 子代理 inline 配置 + 懒编译。
agentexample/agent67v2/
├── agent-config.yml # 统一配置 (协调者 + 6个子代理 inline)
├── orchestrator.yml # 协调者独立配置
├── DESIGN.md # 架构设计文档
├── run.py # 交互式运行
├── launch_paas.py # PaaS 部署
├── agents/ # 5 个微代理 YAML
├── core/
│ ├── coordinator.py # 协调者 ReAct 循环
│ └── bootstrap.py # 从 YAML 构建完整 Term
├── skills/
│ └── registry.py # 微代理 Skill 注册
└── tools/
└── tool_search.py # ToolSearch 懒加载
独立可复用的技能包, 封装 "读论文→复现→实验→记录" 四阶段研究流程。
| Skill | 职责 | 工具 |
|---|---|---|
paper-reader |
搜索→阅读→提取关键信息 | WebSearch, WebFetch |
code-reproducer |
克隆→理解→运行→对比 | Bash, ReadFile, CodeSearch |
experimenter |
设计实验→执行→分析 | Bash, WriteFile, RunTests |
lab-notebook |
整理笔记→报告→知识库 | WriteFile, KBAdd, MemoryStore |
research-pipeline |
完整流程 (组合) | reader >> reproducer >> experimenter >> notebook |
三种使用方式:
agentpaas agent create --name researcher --config lambdagent/skillpacks/research/agent-config.ymlSkillRegistry().get("paper-reader").apply("论文标题")agent67/agent67v2 内置: ResearchWorkflow 工具 / call_research 代理
lambdagent/skillpacks/research/
├── __init__.py
├── skills.py # 4个Skill + 1个Pipeline
└── agent-config.yml # PaaS 可部署编排器
基于 Karpathy LLM Wiki 模式, v2 实现完整的 Ingest→Query→Lint 三步流程 + 主动生长。
| 步骤 | v1 | v2 新增 |
|---|---|---|
| Ingest 抽取要点 | ✅ | ✅ |
| Ingest 补充交叉引用 | ❌ | ✅ 扫描已有页面自动补 [[链接]] |
| Ingest 更新相关页面 10+ | ❌ | ✅ 反向更新已有实体页来源引用 |
| Query 综合多页信息 | 🔶 | ✅ 实体优先 + 标签路由 + [[链接]]跟踪 |
| Lint 查过期引用 | ❌ | ✅ 检测 >90天 未更新 |
| Lint 自动修复 | ❌ | ✅ auto_fix=true 创建断链占位页 |
| WikiGrow 主动生长 | ❌ | ✅ 发现缺失概念 → 自动创建页面 |
| WikiStatus 生长指标 | ❌ | ✅ 交叉引用数/页、健康评分 |
6 个 Wiki 工具: WikiIngest, WikiQuery, WikiLint, WikiSearch, WikiStatus, WikiGrow (新增)
详见: docs/wiki-v2.md
适用于资料少 (< 500 文档) 的领域: 财务、行政、产品手册等。
| lambda (重量级) | lite (轻量级) | wiki (纯 Wiki) | |
|---|---|---|---|
| 检索路径 | BM25+Vector+Graph+Wiki | BM25+Wiki | Wiki only |
| 依赖 | Embedding 服务 + ChromaDB | 无外部依赖 | LLM only |
| 文档量 | 500+ | < 500 | 任意 |
| 部署 | 需 GPU/NPU | 任意机器 | 任意 |
| 适用 | 海事/金融等大规模 | 财务/行政/产品 | 知识编译 |
agentexample/qaagent67lite/
├── agent-config.yml # BM25+Wiki, 无 Vector/Graph
├── DESIGN.md # 设计文档
└── scripts/
├── setup.py # 一键部署 (提取→索引→Wiki编译)
└── instance.yml.template # 实例配置模板
左右双面板, 5 种模式任选, 按域自动适配默认值。
┌──────────────────────┬──────────────────────┐
│ [左侧下拉 ▼] │ [右侧下拉 ▼] │
│ ○ Lite (BM25+Wiki) │ ○ LambdaRAG (4路) │
│ ○ LambdaRAG (4路) │ ○ Lite (BM25+Wiki) │
│ ○ Wiki Only │ ○ Wiki Only │
│ ○ BM25 Baseline │ ○ BM25 Baseline │
│ ○ Direct LLM │ ○ Direct LLM │
└──────────────────────┴──────────────────────┘
| 领域 | 左默认 | 右默认 | 自动检测 |
|---|---|---|---|
| 海事 | LambdaRAG | Wiki | domain 含 "maritime" |
| 其他 | Lite | Wiki | 默认 |
通过 instance.yml 可自定义: demo.leftDefault / demo.rightDefault
| 案例 | 领域 | 使用的 λA 构造 |
|---|---|---|
| research67 | 科研助手 | 8 个子智能体协作,从 IDEA.md → 论文完稿,使用 review + fan_out_merge |
| data67 | 数据分析 | Loop + Pattern 循环优化分析报告 |
| agentbuilder67 | 元智能体 | 用 LLM 自动构建新的 Agent 配置 |
✓ 三篇论文的形式化证明 (其他框架无)
✓ 类型安全定理 (Progress + Preservation)
✓ 终止性定理 (有界不动点)
✓ 并行汇合定理 (Store Independence)
✓ 成本单调性 (CEK 成本向量)
✓ 6 条代数定律 (可安全重构)
✓ 13,700+ LOC 生产级 Python 代码
✓ 503 个测试, 0 失败
✓ 双引擎可切换 (Recursive/CEK/Adaptive)
✓ 28 个 REST API + 5 个 MCP 工具
✓ Instance 机制 (一模板多实例)
✓ Run Workspace 隔离
✓ 跨框架守卫 (LangChain/CrewAI/AutoGen)
✓ qaagent67wiki: 1326 份海事法规, 2989 个 wiki 页面, Wiki v2 持续生长
✓ qaagent67lite: 轻量级问答 (BM25+Wiki), 适合 <500 文档场景
✓ agent67v2: 多智能体协作, 6个微代理 + Handoff + SkillRegistry
✓ research skills: 独立技能包, 读论文→复现→实验→记录
✓ 7+ 个内置 Agent 示例
✓ Demo 对比界面: 5 种模式左右任选对比
✓ 本地 LLM (Ollama) 零 API 成本运行
lambdagentpaas 是把"理论"、"代码"和"案例"三者打通的 Agent 平台:
三者缺一不可:只有理论是学术玩具,只有工程是无保证的工具,只有案例是孤立的演示。三位一体才是能站得住脚的平台。
agentexample/agent67v2/ # 多智能体协作版
├── __init__.py
├── agent-config.yml
├── orchestrator.yml
├── DESIGN.md
├── run.py
├── launch_paas.py
├── agents/__init__.py
├── agents/code-agent.yml
├── agents/shell-agent.yml
├── agents/web-agent.yml
├── agents/memory-agent.yml
├── agents/system-agent.yml
├── core/__init__.py
├── core/coordinator.py
├── core/bootstrap.py
├── skills/__init__.py
├── skills/registry.py
├── tools/__init__.py
└── tools/tool_search.py
lambdagent/skillpacks/ # 技能包
├── __init__.py
└── research/
├── __init__.py
├── skills.py
└── agent-config.yml
agentexample/agent67/tools/
└── research_workflow.py # agent67 科研工具
agentexample/qaagent67lite/ # 轻量级问答
├── agent-config.yml
├── DESIGN.md
└── scripts/
├── setup.py
└── instance.yml.template
docs/wiki-v2.md # Wiki v2 文档
lambdagent/fromconfig/compiler.py # subAgents 编译 + inline 模式
lambdagent/builtin_tools/wiki_tools.py # Wiki v2: 交叉引用/Query增强/Lint修复/WikiGrow
lambdagent/builtin_tools/registry.py # 注册 WikiGrow
agentexample/agent67/agent-config.yml # +ResearchWorkflow
agentexample/agent67/core/assistant.py # +research_workflow 注册
agentexample/qaagent67wiki/agent-config.yml # Wiki v2 prompt + WikiGrow
agentexample/qaagent67lambda/scripts/app.py # Demo 双下拉 + lite_answer
docs/system-overview.md # 本文件