fabio-rovai/tardygrada
GitHub: fabio-rovai/tardygrada
一种纯C11实现的轻量级编程语言，用于构建密码学验证的多智能体系统，通过BFT共识和本体论锚定防止AI幻觉。
Stars: 11 | Forks: 0
[](https://github.com/fabio-rovai/tardygrada/actions/workflows/ci.yml)
# Tardygrada
**LangChain 是 50,000 行 Python。CrewAI 是 153,000 行。LlamaIndex 是 237,000 行。Tardygrada 用 15-53 行代码取代了它们。**
```
tardy terraform /path/to/any-agent-framework
# CrewAI: 153,245 行 -> 53 条指令
# LlamaIndex: 237,414 行 -> 15 条指令
# LangGraph: 101,662 行 -> 39 条指令
# MetaGPT: 89,734 行 -> 11 条指令
```
Tardygrada 是一种编程语言，其中每个值都是一个活跃的 agent。程序编译为 MCP 服务器。每个输出在成为 Fact 之前都经过密码学验证。二进制文件 212KB。零依赖。纯 C11。
## 为什么
每个 agent 框架都做同样的事情：调用 LLM，将结果传递给下一个 LLM，并希望它是正确的。它们都没有验证输出。它们都没有证明 agent 做了这项工作。它们都没有将声明立足于现实。
Tardygrada 做到了。一个 agent 说“神秘博士是在 BBC 电视中心创作的”，系统将其分解为三元组，通过本体论进行立足，运行 3 次独立的验证通过及拜占庭多数投票，只有在此之后才将其冻结为不可变的、经过密码学签名的 Fact。
如果系统没有知识来验证声明，它会说“我不知道”，而不是编造内容。在没有本体论的情况下，0% 的错误接受率。拥有一个本体论时，100% 的正确接受率。
## 30 秒演示
```
# 构建 (耗时 < 1 秒)
git clone https://github.com/fabio-rovai/tardygrada && cd tardygrada && make
# 验证声明
tardy run "Doctor Who was created at BBC Television Centre in 1963"
# 将任意 agent framework 转换为 Tardygrada
tardy terraform /path/to/crewai
# 将 .tardy 程序作为 MCP server 运行
tardy serve examples/medical.tardy
```
## 语言
```
agent MedicalAdvisor @sovereign @semantics(
truth.min_confidence: 0.99,
) {
invariant(trust_min: @verified)
// Claims from external agents -- verified before becoming Facts
let diagnosis: Fact = receive("symptom analysis") grounded_in(medical) @verified
// Shell commands as agent bodies -- output captured and verified
let patient_data: str = exec("sqlite3 patients.db 'SELECT * FROM current'")
// Multi-agent coordination with debate + scoring
coordinate {analyzer, validator} on("verify diagnosis") consensus(ProofWeight)
let name: str = "Tardygrada Medical" @sovereign
}
```
每个关键字都做实事：
- `receive()` 创建一个由外部 agent 通过 MCP 填充的待处理槽位
- `exec()` 派生 /bin/sh，捕获 stdout，存储为 agent 值
- `grounded_in()` 通过 SPARQL 将声明立足于 OWL 本体论
- `@sovereign` 意味着：mprotect + ed25519 + SHA-256 + 5 个 BFT 副本
- `invariant()` 定义在每次操作时检查的宪法规则
- `coordinate` 分发到 brain-in-the-fish 辩论引擎（或回退到收件箱）
- `fork` 将另一个 .tardy 文件 terraform 到当前上下文中
## 工作原理
```
External agent submits claim via MCP
|
Decompose into triples (47 English patterns, 3 independent passes)
|
Ground against ontology
|-- Self-hosted: triples as @sovereign agents (in-process, 200ns)
|-- External: open-ontologies via unix socket (SPARQL + OWL reasoning)
|-- Offline: honest UNKNOWN (no fake confidence)
|
8-layer verification pipeline
|-- 1. Decomposition agreement
|-- 2. Ontology grounding (catches hallucination)
|-- 3. OWL consistency (catches contradictions)
|-- 4. Probabilistic confidence scoring
|-- 5. Protocol structure validation
|-- 6. Triple connectivity certification
|-- 7. Cross-layer contradiction detection
|-- 8. VM work verification (catches laziness)
|
BFT consensus: 3 independent passes, 2/3 must agree
|
Verified -> frozen (mprotect + SHA-256 + ed25519), provenance locked
Failed -> 11 structured failure types + feedback-driven retry
```
## 什么是真实的（非营销）
**数学证明：**
- BFT 共识安全性：在 Coq (Rocq 9.1) 中证明。如果 < N/2 个副本被破坏，则原始值获胜。
- 不可变性：mprotect 由 CPU/MMU 强制执行。硬件会在任何写入尝试时发生故障。
- 签名：通过 Monocypher 使用真正的 ed25519。不是 HMAC 存根。
**结构强制：**
- 懒惰检测：VM 独立记录所有操作，并与最低工作规范进行比较。
- 幻觉预防：声明立足于本体论。未知 = 未知，而不是“已验证”。
- 宪法不变量：在每次读取、写入和生成时检查。不是可选的。
**诚实的局限性：**
- 懒惰检测能捕捉零工作和浅层工作的 agent。一个聪明的 agent 如果只做最低限度的可行工作，则能通过。
- 幻觉预防仅适用于本体论拥有数据的声明。它无法验证它不知道的内容。
- 文本分解器（47 种模式）是基于规则的，而不是 ML。它能处理常见的英语，但不能处理复杂的句子。
## 三个项目，一个技术栈
```
Tardygrada (C, 212KB) -- the language, compiler, VM, MCP server
|
brain-in-the-fish (Rust, 25K) -- debate, scoring, moderation engine
| coordinate keyword connects here
open-ontologies (Rust, 10K) -- OWL reasoning, SPARQL, knowledge graphs
grounded_in() connects here
```
Tardygrada 是前门。brain-in-the-fish 是执行引擎。open-ontologies 是知识层。每一个都可以独立工作。它们共同构成了一个经过验证的 agent 技术栈。
## 分层不可变性
| 级别 | 机制 | 破坏条件 |
|-------|-----------|--------------------------|
| `x: int = 5` | 来源追踪 | 任何写入（在审计日志中跟踪） |
| `let x: int = 5` | mprotect (OS kernel) | 内核漏洞利用 |
| `let x = 5 @verified` | + SHA-256 哈希检查 | 内核漏洞利用 + SHA-256 原像 |
| `let x = 5 @hardened` | + 3 个 BFT 副本 | 破坏多数副本 + SHA-256 |
| `let x = 5 @sovereign` | + ed25519 + 5 个副本 | 以上所有 + 伪造 ed25519 |
## 基准测试
```
Read @verified (SHA-256): 197ns 5,000,000 ops/sec
Read @sovereign (BFT+sig): 1,538ns 650,000 ops/sec
Verification pipeline: 692ns 1,400,000 ops/sec
Message send: 190ns 5,300,000 ops/sec
Spawn @sovereign: 19,820ns 50,000 ops/sec
```
自托管本体论（pizza，581 个三元组）：比 Rust+Oxigraph 等效实现快 40 倍。
## 与其他框架对比
| 框架 | 大小 | 依赖 | 验证 | 来源 |
|-----------|------|------|-------------|-----------|
| LangChain | 50K+ 行 | 30+ 个包 | 无 | 无 |
| CrewAI | 153K 行 | 30+ 个包 | 无 | 无 |
| LlamaIndex | 237K 行 | 40+ 个包 | 无 | 无 |
| AutoGen | - | pyautogen + OpenAI | 无 | 无 |
| MetaGPT | 90K 行 | 90 个依赖 | LLM 自我审查 | 无 |
| browser-use | 89K 行 | - | 无 | 无 |
| PraisonAI | 50MB, 4553 个文件 | 100+ | 提示护栏 | 无 |
| **Tardygrada** | **212KB** | **零** | **8 层 + BFT** | **ed25519 + SHA-256** |
## terraform
```
# 将任意 agentic repo 转换为 .tardy
tardy terraform /path/to/crewai
# 输出: .tardy 文件 + 编译检查 + 统计数据
# 检测: CrewAI, AutoGen, LangChain, LangGraph, LlamaIndex
# 映射: agents -> receive(), tools -> exec(), tasks -> verified claims
```
## 构建
```
make # < 1 second, produces 212KB binary
make run # run tests
make bench # run benchmarks
```
C11 编译器。无外部库。无 malloc。仅直接系统调用。
## 许可证
MIT。参见 [LICENSE](LICENSE)。
## 研究基础
基于以下技术构建：[ARIA Safeguarded AI](https://www.aria.org.uk/programme/safeguarded-ai/)（AI 形式化验证）、[HalluGraph](https://arxiv.org/abs/2406.12072)（知识图谱幻觉检测）、[AgentSpec](https://arxiv.org/abs/2401.13178)（运行时 agent 强制执行）和 [Bythos](https://arxiv.org/abs/2302.01527)（Coq 证明的 BFT 共识）。
标签：AI安全, Anti-Hallucination, BFT, C11, Chat Copilot, Coq, CrewAI替代, DevOps工具, DLL 劫持, LangChain替代, MCP服务器, Terrascan, 可视化界面, 可解释性, 大语言模型, 客户端加密, 密码学验证, 形式化验证, 抗幻觉, 拜占庭容错, 智能体框架, 本体论, 编程语言, 编译器, 零依赖, 静态二进制