tardygrada

KO | EN

gitlite — search

#javascript #llm #android #rust #deep-learning #linux #nodejs #windows #kubernetes #pytorch #mcp #ios #openai #open-source

(★ 20)

A verified runtime for trustworthy AI agents: every claim passes an 8-layer verification pipeline before it counts. Deterministic checks, explainable verdicts, no LLM judging an LLM. Pure C, zero dependencies, MCP-native.

tardygrada Latest Version Download

Download Latest Version (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

[![CI](https://github.com/fabio-rovai/tardygrada/actions/workflows/ci.yml/badge.svg)](https://github.com/fabio-rovai/tardygrada/actions/workflows/ci.yml)
[![License: MIT](https://img.shields.io/badge/License-MIT-blue.svg)](https://raw.githubusercontent.com/fabio-rovai/tardygrada/main/LICENSE)

<h3 align="center">A verified runtime for trustworthy AI agents.</h3>
Every claim an agent makes passes an 8-layer verification pipeline before it counts — deterministic checks, explainable verdicts, no LLM judging an LLM.

---

## What this is

Today's AI agents cannot prove their outputs are true. The standard mitigations
are structural non-starters: post-hoc monitors flag errors after they are acted
on, and LLM-judges inherit the failure mode they are meant to catch. Tardygrada
inverts the architecture: **outputs are gated before release**, by a pipeline
of independent checks that are deterministic wherever determinism is possible,
and every verdict names the layer and the evidence that decided it.

**Two things in one 350 KB C binary.**

1. **The verification runtime.** Catches contradictions between claims, claims
   that conflict with an attached ontology, numbers that don't add up, agent
   traces that *say* they did work but didn't, and tampered intermediate data.
   Plugs into Claude Code, Cursor, or Qwen Code as an MCP server.

2. **A language for verifiable agent programs.** `.tardy` files declare what an
   agent must establish (`receive()` slots), under what semantics
   (`truth.min_confidence`, `pipeline.min_passing_layers`), with what
   invariants. Compiled programs run as MCP servers — a curriculum a generic
   agent picks up, with the pipeline as the exam.

The pipeline (see [`src/verify/pipeline.h`](src/verify/pipeline.h)):

| # | Layer | Nature |
|---|---|---|
| 1 | Decompose — text to triples, independent decomposers | deterministic |
| 2 | Ontology grounding — triples vs knowledge graph | deterministic |
| 3 | Consistency — OWL reasoning for contradictions | deterministic |
| 4 | Probabilistic scoring — conjunction-safe aggregation | quantitative |
| 5 | Protocol — session-type compliance | deterministic |
| 6 | Formal certification — proof-certificate primitives | building block |
| 7 | Cross-representation bridge — layers must agree | deterministic |
| 8 | Work verification — laziness / fake-work detection | deterministic |

Verdicts are three-valued by design: `VERIFIED`, `CONFLICT`, or
`UNVERIFIABLE` — the runtime never converts "could not decide" into either
answer. Layer 4's aggregation is conjunction-safe (geometric mean plus a
weakest-link floor: one unsupported triple cannot hide behind nine strong
ones), and learned rule confidence is a capped Beta posterior — repetition
alone can never manufacture certainty, and contradicting evidence lowers it.

## Research programme

A Phase 1 feasibility study on this runtime runs from October 2026. The
scientific question is composition: the layers are individually
validated (numbers below), and Phase 1 measures whether their composition
lifts real-document detection past fixed gates — F1 ≥ 0.70 and precision
≥ 0.90 on ContraDoc-class data at p95 < 500 ms — with all evaluation code and
gates in [`evaluation/`](evaluation/), reproducible offline. The current
work item, derived from a measured failure analysis of the document detector's
evidence quality, is licence-based conflict detection: a differing-value pair
counts as evidence only when the predicate licenses uniqueness or the values
are demonstrably incompatible.

---

## Quick start

```bash
git clone https://github.com/fabio-rovai/tardygrada && cd tardygrada && make
# Builds in ~3 seconds. ~350 KB binary. Zero runtime deps.

# 60-second guided tour of every working feature
./demo/demo.sh

# Or step through it one section at a time
./demo/demo.sh --pause

# Try the verifier on a document
./tardygrada verify-doc README.md

# Start the persistent daemon
./tardygrada daemon start
./tardygrada status

# Open the live dashboard (treemap of the loaded ontology +
# claim verification panel; cells glow when a claim grounds)
make dashboard
# then visit http://127.0.0.1:8765
```

**Plug into Claude Code** (MCP):

```json
{
  "mcpServers": {
    "tardygrada": {
      "command": "/path/to/tardygrada",
      "args": ["mcp-bridge"]
    }
  }
}
```

The bridge exposes five tools: `verify_claim`, `verify_document`, `spawn_agent`, `read_agent`, `daemon_status`. Then in Claude: *"verify this document for contradictions"*.

**Plug into Qwen Code** (newline-delimited JSON-RPC adapter):

```json
{
  "mcpServers": {
    "tardygrada": {
      "command": "/bin/bash",
      "args": ["/path/to/tardygrada/hooks/targy-mcp-wrapper.sh"]
    }
  }
}
```

---

## Your first specialization

A worked example. A generic agent picks up the curriculum at
[`examples/code-review.tardy`](examples/code-review.tardy) and comes out a
code reviewer whose claims are gated by the pipeline.

```bash
# 1. Start the curriculum as an MCP server (stdio).
#    The agent CodeReviewer spawns with @sovereign trust, three
#    receive() slots, and pipeline.min_passing_layers = 5.
./tardygrada examples/code-review.tardy
```

What that prints:

```text
[tardygrada] agent CodeReviewer spawned
[tardygrada]   @semantics(truth.min_confidence: 0.85)
[tardygrada]   @semantics(pipeline.min_passing_layers: 5)
[tardygrada]   invariant(trust_min)
[tardygrada]   invariant(non_empty)
[tardygrada]   receive("code change description") -> pending
[tardygrada]   receive("author description of the change") -> pending
[tardygrada]   receive("complexity claim") -> pending
[tardygrada] MCP server starting on stdio
```

The three `receive(...) -> pending` slots are the curriculum the agent has to
fill in. Any MCP client (Claude Code, Cursor, a script) can submit claims to
them. The verification pipeline runs over each claim before it is allowed to
resolve.

**Submit a claim via MCP** (raw JSON-RPC, for illustration):

```json
{
  "jsonrpc": "2.0", "id": 1,
  "method": "tools/call",
  "params": {
    "name": "submit_claim",
    "arguments": {
      "agent": "complexity_claim",
      "claim": "The lookup is O(n) with a single pass over the input"
    }
  }
}
```

Then `verify_claim` on the same agent runs the 8-layer pipeline. If the
description elsewhere in the curriculum says the change adds a nested loop,
the lexical implicit-relation layer fires on the `nested_loop -> O(n^2)`
cue pattern and the claim resolves to `CONFLICT`, not `VERIFIED`.

That is the design in one example: *the agent is generic, the curriculum is
specific, and the verification pipeline decides what counts*.

---

## What works today (honest list)

| Capability | Status | Number |
|---|---|---|
| Real-document contradiction detection (ContraDoc, 891 docs) | Real benchmark on real data | **F1 0.57** (LexBase 0.16, FActScore 0.09) |
| Agent-trajectory hallucination detection (AgentHallu, 693 trajectories) | Real benchmark on real data | **F1 0.58** |
| Compositional contradiction suite (650 cases: 500 clear + 150 adversarial) | Designed-for-it; adversarial split added in v2.0 | **clear F1 1.00, 0 FP; combined 0.95; 18 µs/doc** |
| Laziness / fake-work detection (synthetic adversarial traces, 100) | Synthetic, designed-for-it | **F1 0.92, 0 false positives** |
| Memory tampering detection (OS mprotect + SHA-256 + ed25519) | Real OS-level enforcement | n/a |
| VM scaling (5 → 5,000 agents) | Real | ~92 ms total |
| MCP bridge (Claude Code, Qwen Code, Cursor) | Real, four of five tools fully wired (see below) | — |
| `tardy verify-doc` over MCP | Wired to the real pipeline as of v2.0 | — |

---

## What does NOT work, or works differently than you'd expect

**This section exists because previous READMEs hand-waved over these. They don't anymore.**

- **HaluEval F1 0.03.** This benchmark tests single-sentence factual errors against world knowledge ("Paris is the capital of Germany"). That is a retrieval problem, not a verification problem, and Tardygrada is bad at it. We catch claims that contradict *each other* or contradict an attached ontology — not isolated false statements. Use a retrieval-augmented LLM for HaluEval-style tasks.

- **`tardy terraform` is a skeleton extractor, not a framework rewrite.** It scans an existing CrewAI / LangGraph / LlamaIndex / AutoGen / etc. repo and emits an agent-shaped `.tardy` skeleton with stubbed tool bodies. Each tool body must be wired to a real implementation by the user. Treat the output as migration scaffolding around the verification pipeline, not as a working drop-in for the framework. Files in `terraform_prs/` are demonstration scaffolds, not running ports.

- **The lexical baseline in benchmarks is NOT SelfCheckGPT.** The in-repo `lexical_baseline_evaluate` is a deterministic hand-coded antonym/negation heuristic. It is *not* the published SelfCheckGPT (which uses LLM sampling + NLI). The legacy name `selfcheck_evaluate` and the column header `SelfCheck` were renamed in v2.0; benchmark output now prints `LexBase`. See `evaluation/baselines.h` for what the heuristic actually does.

- **`tardy_llm_decompose` does not call an LLM by itself.** It's lexical pattern matching on cue terms (Bonferroni, ISA mismatch, blood type compatibility, etc.). The function was renamed to `tardy_lexical_decompose` in v2.0. The old name is kept as a backwards-compatible inline shim. A separate, opt-in path in `src/mcp/server.c` *does* call Anthropic when `TARDY_LLM_DECOMPOSE=1` is set — that path is unrelated to this file.

- **Coq proofs cover the abstract BFT algorithm, not the C implementation.** `proofs/consensus.v` is real, complete, and `Qed.`-closed (no `Admitted`). It proves abstract majority-vote safety. It does NOT prove the C code is a refinement of that abstraction; the implementation is a faithful translation by hand.

- **`tardy run` works on three classes of claim today.** Computational
  claims (`tardy run "5 + 5 = 10"` → `VERIFIED 0.99`), fundamental-
  constant claims (`tardy run "The speed of light is 299792458 meters per second"`
  → `VERIFIED 0.99`), and world-fact claims that ground against the
  bundled ontology (`tardy run "Paris is in France"` → `VERIFIED 0.85`,
  `tardy run "Tokyo is in Japan"` → `VERIFIED 0.85`, `tardy run "Doctor Who was created at BBC Television Centre"`
  → `VERIFIED 0.78`). Claims with no grounding evidence return
  `ontology_gap` (`tardy run "The cat is invisible"`) rather than a
  false positive. Add your own `.nt` ontology to extend coverage —
  see `tests/wikidata_common.nt` for the format.

---

## Catches what (with examples that actually work)

### Contradicting claims across a document

```bash
./tardygrada verify-doc paper.md
# === Tardygrada Document Verification ===
# File: paper.md
# Sentences: 87
# Triples extracted: 121
# [CONFLICT] Lines 42 vs 89:
#   "We used no external APIs"
#   "API costs totalled $2,400"
#   -> claims no APIs but reports API costs
#   Confidence: 0.85
```

Three layers run together: triple consistency (same subject + predicate, different object), numeric checks (the math doesn't add up), and the lexical implicit-relation layer (cue patterns).

### Lazy / fake-work agents

`laziness_bench` produces synthetic agent traces designed to test the detector. Catches: did-nothing-but-produced-output, skimmed-instead-of-analyzed, fabricated-evidence-of-work, copied-another-agent's-answer, verified-itself-in-a-circle. F1 0.92 across 100 adversarial traces.

### Tampered intermediate data

Values created with `let x = 5 @verified` are protected at the OS page-table level (`mprotect`) plus a SHA-256 read-time check. `@hardened` adds replicas + a Byzantine vote. `@sovereign` adds ed25519 signatures and BFT consensus. Tampering requires breaking SHA-256 or forging an ed25519 signature.

---

## How verification works

```mermaid
graph LR
 subgraph Pipeline["Verification Pipeline (8 layers)"]
 direction LR
 C["Claim"] --> D["Decompose"]
 D --> G["Ground"]
 G --> CON["Consistency"]
 CON --> P["Probabilistic"]
 P --> PR["Protocol"]
 PR --> F["Certification"]
 F --> CR["Cross-Rep"]
 CR --> W["Work Verify"]
 W --> V{"VERIFIED / CONFLICT / UNVERIFIABLE"}
 end
```

Layers 1, 2, 3, 4, 5, and 8 are deterministic and run on every check. Layers 6 and 7 are formal-methods primitives that ship as building blocks; they are not auto-invoked.

```mermaid
graph LR
 subgraph Trust["Tamper protection levels"]
 direction LR
 MUT["Mutable"] --> DEF["Default (OS-locked)"]
 DEF --> VER["Verified (+ SHA-256)"]
 VER --> HARD["Hardened (+ replicas)"]
 HARD --> SOV["Sovereign (+ ed25519 + BFT)"]
 end
```

```mermaid
graph TB
    subgraph Tardygrada["Tardygrada"]
        CLI_CMD["CLI"] --> DAEMON_S["Daemon"]
        DAEMON_S --> VM["VM Core"]
        VM --> VERIFY_S["Verification"]
        VM --> ONTO["Knowledge Base"]
        VM --> CRYPTO_S["Cryptography"]
    end

subgraph External["Optional integrations"]
 BITF["brain-in-the-fish (multi-agent debate)"]
 OO["open-ontologies (OWL reasoning)"]
 end

VM -- "coordinate" --> BITF
    VM -- "grounded_in" --> OO
```

---

## The language (for power users)

```text
agent MedicalAdvisor @sovereign @semantics(truth.min_confidence: 0.99) {
    invariant(trust_min: @verified)
    let diagnosis: Fact = receive("symptom analysis") grounded_in(medical) @verified
    let data: str = exec("sqlite3 patients.db 'SELECT * FROM current'")
    coordinate {analyzer, validator} on("verify diagnosis") consensus(ProofWeight)
}
```

Every value is an agent. `receive()` accepts claims from external systems (over MCP). `@sovereign` means cryptographically signed and replicated. `coordinate` dispatches multi-agent debate.

You don't need to write Tardygrada to use Tardygrada. The CLI, daemon, and MCP bridge cover every common case.

---

## Reproduce the benchmarks

```bash
cd evaluation && make

./laziness_bench       # 100 synthetic traces, F1 0.92
./scaling_bench        # 5 -> 5000 agents, near-linear
./contradoc_bench      # 891 real ContraDoc documents, F1 0.57
./agenthallu_bench     # 693 real AgentHallu trajectories, F1 0.58
./halueval_bench       # 500 HaluEval examples, F1 0.03 (intentional weakness)
./vitaminc_bench       # 500 VitaminC fact-verification cases
./hallucination_bench  # 650 cases (500 clear + 150 adversarial); clear F1 1.00, 18 us/doc
./ablation_bench       # layer-by-layer contribution
```

External datasets (`contradoc.json`, `agenthallu_flat.json`, `halueval_500.json`, `vitaminc_500.json`) are checked into the repo. Everything is reproducible offline.

---

## Hardening (v2.0)

- Daemon socket: created with mode 0600 (owner-only). Previously default umask, often world-readable on shared boxes.
- Daemon recv timeout: 5 s. Closes slow-loris DoS against the single-threaded dispatcher.
- Build flags: `-fstack-protector-strong -D_FORTIFY_SOURCE=2 -fPIE`. Linux additionally `-pie -Wl,-z,relro,-z,now`.
- Optional Anthropic API key (set when `TARDY_LLM_DECOMPOSE=1`): no longer placed on the command line for `curl`. Written to a 0600 temp file passed via `-K`, unlinked after the call. Not visible in `ps auxe` or `/proc/PID/cmdline`.
- Claude API request body: user claim is JSON-escaped before embedding. Closes a quote/backslash injection.

---

## Research foundations

Built on:

- [AgentSpec](https://arxiv.org/abs/2503.18666) (ICSE 2026) — runtime enforcement
- [Bythos](https://arxiv.org/abs/2302.01527) (CCS 2024) — Coq BFT verification
- Minsky frames (1974), CRDTs (Shapiro 2011), Datalog (1986)

Evaluated against:

- [SelfCheckGPT](https://arxiv.org/abs/2303.08896) (EMNLP 2023) — *cited as inspiration; the in-repo lexical baseline is NOT a re-implementation, see above*
- [FActScore](https://aclanthology.org/2023.emnlp-main.741/) (EMNLP 2023)
- [ContraDoc](https://aclanthology.org/2024.naacl-long.362/) (NAACL 2024)
- [HaluEval](https://huggingface.co/datasets/pminervini/HaluEval)

- [Mundler et al.](https://arxiv.org/abs/2305.15852) (ICLR 2024)
- [Fang et al.](https://arxiv.org/abs/2409.11283) (AAAI 2025)

---

## Companion projects

- **[open-ontologies](https://github.com/fabio-rovai/open-ontologies)** — ~11k lines of Rust. OWL reasoner, optionally invoked by the verifier as the ontology grounding source.
- **brain-in-the-fish** — ~24k lines of Rust. Multi-agent coordination/debate substrate, optionally invoked for `coordinate { ... } consensus(...)` blocks.

Both run as separate processes; Tardygrada speaks to them over local IPC.

---

## License

MIT. See [LICENSE](LICENSE).

---

## Versioning

This is v2.0. See [CHANGELOG.md](CHANGELOG.md) for the v1 → v2 scope realignment — what was renamed, what was scoped down, and what was hardened.

tardygrada

tardygrada Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

tardygrada

tardygrada Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

Download README