Eigenius

An open-source platform for verifiable AI in science and engineering, built on a typed, versioned knowledge graph.

Modern language models can produce convincing text without producing trustworthy knowledge. Eigenius is a substrate for representing what the science actually says: typed resources with tracked provenance, replayable derivations, and — where the claim warrants it — machine-checked formal proofs.

The platform distinguishes four kinds of knowledge, each with stronger guarantees than the last:

• Declared — a human asserts it.
• Observed — measured or recorded with provenance.
• Derived — produced by a typed pipeline whose steps are auditable.
• Verified — derived and re-checked by a formal proof system (Lean 4 today).

When a result matters — a clinical trial conclusion, a materials-property prediction, a regulatory submission — you can tell what has been verified end-to-end versus what's plausible-sounding text without grounding.

Theoretical foundation: dependent type theory + Grothendieck institutions, integrating different formal logics and scientific disciplines under one typed substrate. Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning sketches the academic framing.

This is still a very early stage of this project. Anticipate features not working or missing functionality overall. Our goal is to close those quality gaps rather aggressively. Feel free to submit issues in the discussion forum or directly as issue.

Quick start

The fastest path is the Docker Compose stack (no Rust or Deno needed on the host):

docker compose up --build -d

# Open the notebook
open http://localhost:8080/notebooks/   # macOS; xdg-open on Linux

# Run the end-to-end CLI demo
./demo/run.sh

# Drive the platform from an LLM agent (Claude Code / Desktop / Cursor / ...)
claude mcp add --transport http eigenius http://localhost:8080/mcp

The first build takes a few minutes. Subsequent ups are fast. See Docker Compose below for state inspection, logs, and ANTHROPIC_API_KEY setup, MCP server for the agent surface, or Getting Started for a native-toolchain build.

What Eigenius gives you, today:

• Typed, versioned knowledge graph — immutable layers with content-addressed IDs, branches/tags/merges, conflict resolution with on-chain provenance, garbage collection. (D23, D20)
• Five live Julia institutions for scientific computing — Symbolics, IntervalArithmetic, Catalyst, DifferentialEquations, and JuMP — sharing a typed FormulaTerm representation, with cross-institution comorphisms (Catalyst→DiffEq, Symbolics→JuMP). (D27)
• Lean 4 verification institution — proof terms commit as chain resources; the kernel re-checks them in-process via nanoda_lib and lands a typed Verdict resource so verified is itself queryable. (D28)
• Native dependent-type surface — EigenTT carries an impredicative Prop universe with proof irrelevance, indexed inductive families with first-order pattern unification, and a chain-mirrored type fragment that lets axiom statements, propositions, and dependent motives round-trip as content-addressed chain artifacts. Authorable directly in ESL via axiom, indexed data, and match … returning fun (i : T) => body. (D46, , )

The notebook — start here

For most users, the notebook is the most accessible way to use the platform. It is a React SPA the orchestrator serves at http://localhost:8080/notebooks/; cells run ESL, EigenQL, TypeScript, and program invocations against the live kernel; outputs auto-render as typed inspectors, result tables, layer-stack diagrams, and program-trace trees.

If you have the docker stack up (docker compose up -d), the notebook is already there — it's bundled into the orchestrator image at build time and serves alongside the RPC paths on the same origin. Open the URL above and the stats-and-reasoning demo loads on first mount; click Run all and watch the ESL cells commit six raw IC₅₀ reads and a StatisticalAnalysisPlan, the statistics institution recompute the claim on commit, and the EigenQL cells return its Holds verdict and the reasoning institution's verdict on a justification:Conclusion that composes the statistical evidence with a classification rule.

See chapter 14 — Notebook for the full reference. The most comprehensive worked example is kinase-institutions.json — a three-part walkthrough that authors a flat kinase screening dataset (24 IC₅₀ measurements across 6 compounds × 4 targets), renders it across every Fluent chart kind, and then lifts the same domain to typed reasoning via Catalyst → DiffEq and Symbolics → JuMP comorphisms. Run the setup script once before opening it.

For collaborative chain work, chapter 15 — Tags, branches, and history covers the workspace rail's chain destinations (Branches, Tags, History) and the time-travel read-pin, and chapter 16 — Merge resolution covers folding one branch into another when contributions conflict: the six-state flow, the four strategies (Witness / Rename / SchemaQuotient / Restructure), the cascade gate, and chain-resident provenance records.

The same SDK that powers the notebook (@eigenius/client) is usable programmatically from any TypeScript runtime — see chapter 17 — TypeScript SDK.

User guides

Four task-first guides plus a consolidated bibliography, all grounded in the implementation:

• Platform user guide — chapters on operating the platform: installation, build, CLI reference, running locally, database management, the orchestrator, end-to-end demos, the runtime substrate (Julia v1) with per-institution slow-walks, deployment, troubleshooting, the notebook UX, tags / branches / history, merge resolution, the TypeScript SDK.
• ESL — Eigenius Surface Language — eleven chapters on the declarative surface (namespace, class, property, resource, axiom, def, data, program) and the ML-style expression sublanguage. Most important chapter: chapter 6 — Resources, types, and the layer, the bridge between the resource graph and the kernel's type theory.
• EigenQL — query language — twelve chapters on pattern matching, derived relations, expressions, FIBER institution dispatch (with INTO-pinned chain reinsertion), stratification, and the result-document format.
• Formula language — eight chapters on the chain-mirrored EigenTT fragment (urn:eigenius:formulas:FormulaTerm) shared by every numerical institution: Symbolics, IntervalArithmetic, Catalyst, DiffEq, JuMP-HiGHS. Covers the six-constructor inductive, Eigon-JSON encoding, operator catalog, the ESL formula(...) Pratt-parsed sublanguage, and identity-comorphism collapse across institutions.
• References — consolidated bibliography for the platform: works actually cited in design docs / papers / guides, foundational works the system relies on, philosophical and methodological precursors, and contemporary related work. Generated from the BibTeX files in by ; verified against Crossref / arXiv / live URLs by .

Guides landing page: docs/guides/. Full documentation index (guides + design documents + papers): docs/.

Status

The platform is operational end-to-end: kernel, orchestrator, and CLI connected via gRPC. The original phase plan (0–11e) is complete, and the work has since been tracked by design document rather than phase number. Landed since: the notebook + SDK (D22), institution realisation (D14), runtime substrate (D26 / D29 / D31), formula language (D32), the Lean 4 verification institution (D28 / D30 / D40), the dependent-type surface (D46 / D47 / D48), justification logic and the witness machinery (D39 / D49 / D73), the prose→propositions parsing pipeline (D62–D66, D71), and the type-theory/knowledge-graph fusion (D75 / D76 / D78 / D79). D77 and D80 are designed and not yet implemented.

The system can:

• Parse and serialize Eigon-JSON and CBOR documents
• Load the self-describing core, program, reflection, eigentt, institution, runtime, formulas, lean, reasoning, statistics, logic, lexicon and encoding ontologies (21 bootstrap layers)
• Build immutable layers with content-addressed identifiers (SHA-256 of CBOR)
• Validate resources against the full ontology constraint system (25 validation rules, numbered through Rule 24 — including inductive-declaration admission and reference integrity on the commit path)
• Resolve resources through parent-pointer layer chains
• Query the knowledge graph with EigenQL (typed stratified Datalog with aggregation)
• Type-check programs using EigenTT dependent type theory (NbE evaluator)
• Execute programs with local and remote IO components (remote ones via the orchestrator)
• Dispatch IO components to the Deno orchestrator via gRPC (ComponentExecutor service)
• Expose 16 kernel operations as MCP tools (query / inspect / load / validate-program / run-program / institutions / schema / branches / tags / tasks / topology / formalize-document / health) for LLM agents. HTTP transport at http://localhost:8080/mcp when the docker stack is up (point Claude Desktop / Claude Code at the URL); stdio also available via cd orchestration && deno task mcp for kernel-on-host development
• Track four epistemic categories: declared, observed, derived, verified
• Record tree-structured reasoning traces with memoization and incremental execution
• Validate epistemic base class requirements (DeclaredResource, DerivedResource, etc.)
• Persist layers, traces, and institution registrations in RocksDB — survives kernel restart
• Serve the kernel as a gRPC service (tonic) with streaming query results
• Compile ESL (Eigenius Surface Language) to Eigon-JSON — all CLI commands accept .esl files
• Register Grothendieck institutions with fiber reasoners and morphism validation
• Run programs as resumable tasks with checkpointing
• Resolve ontology classes as kernel types on demand via the layer chain (Phase 10, D18)
• Type-check inductive declarations against the kernel's admission gate — strict positivity, universe-polymorphic recursor motives, and constructor arity — on the commit path (D19, D46)
• Use Map and Reduce as type-level primitives with structural-recursion termination (Phase 11a)
• Declare institutions, export/import boundary formats, query classes, and triadic comorphisms as ontology resources committed to the layer chain (D14 §3–§5)
• Fire Decidable QueryClasses at type-check time, returning a projected to the kernel's reduction ( → , → failing neutral, → passthrough) (D14 §9.2)

See docs/design/implementation-plan.md for the full phased build plan.

Architecture

Everything in Eigenius is a Resource — classes, properties, data types, formats, and instance data are all represented uniformly with IRI identity and typed property values. The core ontology is self-describing: Class is an instance of Class.

• Rust Kernel — ontology validation, layer management, resource resolution, program execution, gRPC server. Uses BTreeMap for deterministic ordering and cache-friendly access.
• Deno Orchestrator — IO component dispatch, MCP server. Communicates with the kernel via Connect RPC/gRPC.
• Layer System — immutable layers with parent pointers (Arc<Layer>), forming a chain. Four bootstrap layers: core → program → reflection → institution. Resolution walks the chain top-down.
• Eigon-JSON / CBOR — the canonical serialization formats. @id is the only reserved key; all property keys are full IRIs. Three-layer type system: primitive data types, format constraints, and content types. CBOR for storage and gRPC wire format.
• Validation — 12 rules: required properties, inheritance, type checking, format/pattern validation, range/length constraints, class type checking, allowed values, domain checking, conditional requirements, open-world extra properties. Epistemic base classes enforce provenance requirements.
• EigenQL — typed stratified Datalog with aggregation. Supports USING, MATCH (typed/untyped/negated patterns), WHERE, GROUP BY, RETURN (with COUNT/SUM/AVG/MIN/MAX), ORDER BY, LIMIT/OFFSET, DISTINCT, DEFINE (recursive rules with a naive stratum-ordered fixpoint), dot-path navigation, NOT EXISTS. Full pipeline: lex → parse → stratify → type_check → evaluate.
• Program Model — programs are typed expressions (Let, Apply, Lambda, Case, Map, Reduce, etc.) that map 1:1 to EigenTT terms. Type-checked via NbE (Normalization by Evaluation) with Eigon ontology types as ground types. IO components dispatched to the orchestrator via gRPC with trace recording and memoization.
• Epistemic Model — four categories (declared, observed, derived, verified) enforced via base classes in the reflection ontology. Reasoning traces mirror the expression tree and serve as memoization cache.
• Grothendieck Institutions (D14) — domain-specific reasoning systems contribute structured fibres to the knowledge graph. Each institution is declared as ontology resources (Institution, ExportFormat, ImportFormat, QueryClass, Comorphism) committed to the layer chain, and implemented via the three-method Institution trait (extract_typed / reify / query). Comorphisms are triadic — source-side export + cross-institution EigenTT transformation + target-side import — with optional exact: bool Satisfaction-Condition annotation. The category-theoretic Grothendieck construction emerges from declared comorphisms; the kernel provides the dispatch and well-typedness machinery.

Phase 19 complete (19a–19i): D26 runtime substrate landed end-to-end with the Julia v1 instantiation (D27 — five worked institutions: Symbolics, IntervalArithmetic, Catalyst, DiffEq, JuMP-HiGHS); D29 mirror generator with closure walker; D31 install lifecycle; D32 formula language as EigenTT fragment with the ESL formula(...) sublanguage; comorphism chain reinsertion (D14 §9.3) wired through both ESL Exp::InstitutionInvoke and EigenQL FIBER ... INTO. The kinase-institutions notebook (notebooks/examples/kinase-institutions.json) exercises the entire stack end-to-end.

Phase 20a complete (20a.0–20a.8): the first verification institution. D28 Lean 4 institution landed end-to-end through the substrate's authoring side (lean4export against pinned LeanEnvironment images) and an in-process verification side (nanoda_lib re-check with axiom-allowlist enforcement); D40 chain-mirrored lean:LeanExpr / lean:LeanLevel / lean:LeanName inductives; D30 faithful translation spec with the substrate LeanMirrorGenerator producing baked EigeniusFFI Lake packages; three-part correspondence check (D28 §5.5) wired through AutoOnLoad. The lean-verification notebook (notebooks/examples/lean-verification.json) walks the closed audit chain D28 §5.7 promises. Phase 20b (Mathlib-scale operational landing per D28 §11.2) is consumer-triggered; not architecturally required.

Type-theory layer 2 landed (D46 / D47 / D48): EigenTT now carries an impredicative Prop universe with proof irrelevance and a Sort(n)-laddered universe (D46), a chain-mirrored type fragment eigentt:TypeExpr with a bidirectional Exp ↔ Value::Json codec (D47, extended for term-level constructors), and indexed inductive families with a first-order pattern unifier, dependent constructor checking, per-arm index-coherence, and singleton elimination for propositional indices (D48). The companion eigentt:Axiom chain class admits propext and Quot.sound as kernel built-ins on the same footing. The ESL surface for proposition and indexed-type authoring landed across three layers — axiom Name : <type-expr> declarations, data Vec(A) : Nat -> Set { … } with index telescopes and typed ctors, and match … returning fun (i : T) => body Lambda motives — making the type-theoretic refinements directly authorable. D39 v2 (justification logic) consumes the whole stack: propositions live in Prop, the JustifiedBy predicate is an indexed inductive over JustificationTerm, and grounding witnesses project the reflection ontology's existing class-membership facts into the type system.

See docs/design/architecture-v0.3.md for the full architecture specification.

Docker Compose

The demo can also run via Docker Compose without installing Rust or Deno locally.

# Build and start both services:
docker compose up --build -d

# Run the demo:
./demo/run.sh

# Stop:
docker compose down

The kernel reads ANTHROPIC_API_KEY from the host environment for D71 formalization runs on a branch with no recorded draws; with it unset, such a run fails closed.

Inspecting the kernel's persistent state

The kernel writes its RocksDB store to a named docker volume (eigenius_db) mounted at /var/lib/eigenius/db inside the kernel container. The volume survives docker compose down; use docker compose down -v to wipe it (the next up re-seeds at schema v1).

# Peek at the on-disk RocksDB files via the running kernel container
docker compose exec kernel ls -la /var/lib/eigenius/db
docker compose exec kernel du -sh /var/lib/eigenius/db

# Or attach a throwaway alpine container with just the volume mounted
# (useful when the kernel container won't start):
docker run --rm -it -v eigenius_eigenius_db:/data alpine sh
# inside: ls -la /data ; du -sh /data ; exit

# Show what docker thinks it knows about the volume
docker volume ls | grep eigenius_db
docker volume inspect eigenius_eigenius_db

# Inspect platform state through the kernel API (preferred — RocksDB's SST
# files are not directly readable; go through the kernel surface):
eigenius --endpoint http://localhost:50051 branch list
eigenius --endpoint http://localhost:50051 branch show main

# Reset the dev DB and start fresh:
docker compose down -v          # wipes the volume
docker compose up -d            # next `up` re-seeds at schema v1

The volume name on the host is <project>_eigenius_db — typically eigenius_eigenius_db if you run from the repo root. See D24 — Schema Versioning for what gets stamped at seed time and why a down -v reset is sometimes needed after a kernel upgrade.

Reading the kernel logs

The kernel uses tracing and emits structured JSON when running in docker (no TTY). Standard docker compose logs controls visibility; RUST_LOG and EIGENIUS_LOG_FORMAT control verbosity and shape.

# All kernel logs since startup
docker compose logs kernel

# Follow (Ctrl-C to stop)
docker compose logs -f kernel

# Last N lines, then exit
docker compose logs --tail=100 kernel

# Bounded by time
docker compose logs --since 5m kernel

# Both services side-by-side
docker compose logs -f kernel orchestrator

# Pipe structured JSON through jq
docker compose logs --no-log-prefix kernel | jq 'select(.fields.operation)'

# Just RPC failures
docker compose logs --no-log-prefix kernel | jq 'select(.fields.error_kind)'

For more verbose output during debugging, add to the kernel.environment block in docker-compose.yml:

- RUST_LOG=eigenius_kernel=debug,info
- EIGENIUS_LOG_FORMAT=pretty   # human-readable instead of JSON

eigenius_kernel=debug turns on per-RPC and per-chain-walk events; info keeps the rest of the workspace at the default level. trace is rarely useful — that's where high-volume per-resource events live.

MCP server (for LLM agents)

The orchestrator exposes a curated subset of the kernel surface as Model Context Protocol tools, so an LLM agent can drive Eigenius as part of its reasoning — query the graph, run programs, inspect provenance, discover institutions.

16 tools are wired across three groups:

Group	Tools
Explore	eigenius_query, eigenius_inspect, eigenius_list_branches, eigenius_list_tags, eigenius_list_institutions, eigenius_get_schema, eigenius_layer_topology
Mutate	eigenius_load (with D41 policy / explicitTombstones), eigenius_validate_program, eigenius_run_program, eigenius_run_program_by_iri, eigenius_formalize_document
Observe	eigenius_health, eigenius_list_tasks, eigenius_get_task_status, eigenius_get_formalization_result

Branch / tag mutation, merge submission, consolidation, GC, and task cancellation are deliberately not exposed — those are stateful or destructive flows that belong to the notebook UI or the operator CLI.

Setup

The orchestrator mounts MCP at http://localhost:8080/mcp (Streamable HTTP, stateless + JSON-response mode). With the docker stack up, point any MCP-aware client at that URL.

Claude Code (CLI or VS Code extension):

claude mcp add --transport http eigenius http://localhost:8080/mcp
claude mcp list                                     # verify ✓ Connected

Claude Desktop — native HTTP transport support is uneven across builds; use the mcp-remote stdio bridge instead. Requires Node.js installed on the host (for npx):

{
  "mcpServers": {
    "eigenius": {
      "command": "npx",
      "args": ["-y", "mcp-remote", "http://localhost:8080/mcp"]
    }
  }
}

Some builds do accept { "type": "http", "url": "http://localhost:8080/mcp" } directly — try that first if you prefer; fall back to mcp-remote if the app reports "MCP failed to connect."

Config file locations:

• Windows: %APPDATA%\Claude\claude_desktop_config.json
• macOS: ~/Library/Application Support/Claude/claude_desktop_config.json
• Linux: ~/.config/Claude/claude_desktop_config.json

Cursor / other IDE agents — { "type": "http", "url": "..." } works on most builds. If it doesn't, use the mcp-remote form above.

For a stdio transport (kernel-on-host development, no orchestrator container required), run cd orchestration && deno task mcp and point the client at that subprocess. See platform guide §7.6 for the full client wiring.

The agent guide

The packaged skills are not currently recommended. The MCP server itself is available and works as documented above. The three agent skills that drive it — eigenius, grounding, reasoning — are parked under docs/method/ rather than installed, because a series of in-flight kernel changes makes the workflows they encode unreliable. Read them for the mental model; do not rely on them as a current procedure. (docs/method/eigenius.md still says 14 tools, and still lists WASM institutions, since removed.)

docs/method/eigenius.md teaches a coding agent the platform's mental model, the three surface languages, the MCP tool selection table, minimal Eigon-JSON / ESL / EigenQL shapes, common workflows, and the pitfalls that trip agents up (mandatory is_a, synthesized IRI row keys in query results, persistent-backend requirements, D41 multi-layer outcomes, …).

It is a reference document, not an auto-loaded agent skill — point the agent at the file, or paste the relevant section. Two companions sit beside it: reasoning.md (capturing reasoning as a typed chain) and grounding.md (retrieval and citation anchors).

After claude mcp add, ask the agent something like "check the eigenius health" or "list the classes loaded in eigenius".

Smoke-test with the MCP Inspector

npx @modelcontextprotocol/inspector --url http://localhost:8080/mcp

Opens a web UI for poking at the tools interactively. If eigenius_health returns { healthy: true, ... }, the whole chain (client → orchestrator → kernel) is good.

Repository Structure

kernel/          Rust kernel crate
  src/ontology/    IRI, Resource, Value, Eigon-JSON / Eigon-CBOR, well-known constants
  src/layer/       Layer, LayerBuilder, LayerId (content-addressed), merge/ (D20/D36/D37/D38)
  src/lattice.rs   Branch-ref CAS, LCA + iri_sources_since, trivial-merge driver
  src/gc.rs        Garbage collection over the reachable layer graph (D24)
  src/validation/  Validator: 12 commit-time rules (type-check, format, pattern, range, length,
                   class-types, allows-only, domain, conditional, inductive, is_a, ...)
  src/query/       EigenQL: lexer, parser, type checker, stratification, evaluator/
  src/nbe/         EigenTT type theory: terms, values, eval, readback, type checker
  src/program/     Program model: expression parser, ground type resolution, executor
  src/esl/         ESL compiler: lexer, parser, compiler to Eigon-JSON (incl. `merge_comorphism`, `lambda`, `pi`)
  src/capability/  Institution capability registration (external + in-process backends), chain-scan auto-registration
  src/institution/ D14 Institution trait, InstitutionIndex (chain-derived), InstitutionRuntime, AutoOnLoad dispatch
  src/runtime/     Runtime-substrate dispatch (D26 worker IPC, mirror-derived call routing)
  src/commit/      D41 commit pipeline: single-layer pipeline + multi-layer orchestrator, persister, hooks
  src/context/     ExecutionContext (snapshot isolation, read/write control)
  src/bootstrap/   Ontology loader and system initialization (six bootstrap layers)
  src/storage/     Storage interface traits (LayerStore, ResourceStore, branch/tag CAS)
  src/server/      gRPC service implementations (per-RPC modules: branches, consolidate, gc,
                   inspect, lifecycle, load, programs, query, reflect, tags, tasks, ...)
  src/task/        Task model: TaskRecord, Checkpoint, resume sweep
  src/observability/  Tracing spans, RPC guards, operation labels
storage/         Storage backend implementations
  rocksdb/         RocksDB backend (durable layers, traces, branch refs, institution registrations)
  tikv/            TiKV backend (placeholder)
crates/
  runtime-substrate/       D26 substrate: worker spawning + UDS IPC + mirror generation
  eigenius-julia/          Julia worker host (spawns the Julia process, marshals FormulaTerm)
  eigenius-lean/           Lean 4 institution: orchestrator-facing authoring surface
  eigenius-lean-runtime/   Lean 4 image / Lake-package build driver (substrate side)
  eigenius-lean-worker/    In-process Lean re-checker via `nanoda_lib` (verification side, D28)
  eigenius-config/         Workspace configuration parsing
julia/           Julia v1 institutions + substrate host (D27)
  runtime-worker/    The Julia process the runtime-substrate spawns (FormulaTerm marshalling, RPC dispatch)
  common/            Shared helpers consumed by every Julia institution
  institutions/      Symbolics, IntervalArithmetic, Catalyst, DiffEq, JuMP
  comorphisms/       Catalyst → DiffEq, Symbolics → JuMP, Symbolics → IntervalArithmetic
  research/          Experimental institutions
lean/            Lean 4 verification institution worker + shared support (D28 / D30 / D40)
  runtime-worker/    Authoring-side Lake package: `lean4export` against the pinned LeanEnvironment image
  common/            Shared Lean helpers (mirror plumbing, EigeniusFFI surface)
  research/          Experimental proofs and mirror-validation fixtures
cli/             Command-line interface (load, validate, query, run, serve, tasks, capability,
                  db {branch,tag,merge,consolidate,gc,export,stats}, mirror / env / institution, ...)
ontologies/      Ontology definitions (chain-bootstrapped on startup)
  core/            Core ontology — self-describing bootstrap (incl. MergeComorphism + MergeResolutionRecord)
  program/         Program ontology — expression classes, Lambda, Pi, Components
  reflection/      Reflection ontology (reasoning traces, derivation, epistemic status)
  institution/     Institution ontology (D14: Institution / ExportFormat / ImportFormat / QueryClass / Comorphism / Verdict)
  notebook/        Notebook ontology (Notebook + Cell + CellType — backs `Publish` from the UI)
  formulas/        Formula language (D32: FormulaTerm InductiveType + Operator catalog)
  runtime/         Runtime-substrate ontology (D26: RuntimeEnvironment, RuntimeKind, …)
  examples/        Example ontologies and programs
notebooks/       React notebook SPA (D22) — bundled into the orchestrator image
  src/             Source: cell editors + output renderers + workspace rail (Branches/Tags/
                   History/Merge/Compaction/GC/Layer/Institutions/Health/Topology destinations)
  examples/        Bundled notebooks (stats-and-reasoning, kinase-institutions, D36 merge tests, lean-verification)
  e2e/             Playwright specs (stats-and-reasoning, kinase-charts, merge-resolution)
clients/
  eigenius-ts/     `@eigenius/client` — TypeScript SDK that wraps the orchestrator's RPC surface
                   (incl. branch/tag/merge/preview/submit surfaces with witness-search-branches)
proto/           gRPC protobuf definitions
orchestration/   Deno/TypeScript orchestration layer (IO component dispatch, MCP server, notebook static-file route)
  src/                       Orchestrator source
  runtime-substrate-native/  napi-rs addon embedding the Rust runtime substrate inside Deno
  tests/                     Deno integration tests
deploy/          Dockerfiles (kernel, orchestration) + Azure ContainerApps Bicep IaC
demo/            End-to-end demo scripts (`run.sh`, `d41-commit-pipeline/run.sh`, …)
docs/            Documentation
  design/          Design documents (D1–D41) + architecture-v0.3 + implementation plan
  guides/          User guides — platform (18 chapters), ESL, EigenQL, formula, references
  notes/           Working notes (e.g. manual-test scenarios)
  references/      BibTeX bibliography
  papers/          Drafts + working papers
scripts/         License-header application, BibTeX-to-Markdown, citation verification,
                 lexicon reseed, parse-rate measurement, alignment-snapshot build
experiments/     Measured work with committed baselines — parsing (corpus, gold readings,
                 recorded LLM draws), lexicon alignment, benchmark tasks, the WRN publication
                 chain. `results/` is gitignored; the distilled baselines are not.
website/         Astro/Starlight documentation site
patches/         Vendored crate patches (e.g. `tonic-web`)
data/            Small fixed inputs used by demos and tests
references/      Reference implementations and papers consulted during development
                 (`nanoda_lib` for EigenTT, `openccg` read-only, `publications/` PDFs)

Getting Started

Prerequisites

The platform builds and runs on Linux (native or Windows with WSL 2) and macOS. The demo rig is a Rust kernel, a Deno orchestrator, and a CLI, all tied together by gRPC. Optional pieces (GitHub issue workflow, Docker-based deployment) add their own tools.

Core toolchain (required)

• Rust (stable, 1.97+ — matches deploy/Dockerfile.kernel; earlier versions may fail to build some workspace dependencies). Install via rustup.
• Deno — orchestration layer (orchestration/).
• System packages (Ubuntu / WSL 2):

  sudo apt-get install -y build-essential pkg-config libssl-dev protobuf-compiler libclang-dev
  

  • build-essential — C/C++ toolchain for RocksDB's native sources.
  • pkg-config + libssl-dev — TiKV client dependency.
  • protobuf-compiler — protoc for the gRPC build scripts.
  • libclang-dev — bindgen needs it to compile RocksDB headers.
• just (task runner, optional but matches the commands in this README):

  cargo install just
  

GitHub workflow (optional, recommended)

The project tracks correctness hazards and phase work as GitHub issues. The gh CLI is the usual entrypoint for reading / filing them:

# Ubuntu / WSL 2
sudo apt-get install -y gh
gh auth login

Docker (optional)

The end-to-end demo can run entirely in containers — skips Rust and Deno on the host. Install Docker Engine and Compose v2 per your distribution's instructions; then see the Docker Compose section below.

Domain corpora (optional — lexicon / knowledge-graph sources)

Three third-party corpora can be imported as typed layers: WordNet (the general lexicon behind the DCG / natural-language engine, D63) and NCBI Gene and UMLS (domain knowledge-graph sources, D65). None is vendored (references/ is gitignored); each is provisioned on demand by a deterministic importer (no LLM) that validates through the kernel and, with --endpoint <addr>, persists the layer like any other. Emitted .esl docs are gitignored (regenerable) and carry their source's license notice.

# WordNet 3.0 — the DCG lexicon
scripts/provision-wordnet.sh                 # download + convert + validate (full, ~minutes)
scripts/provision-wordnet.sh --seed gene     # a small seeded slice (fast, for trying it out)

# NCBI Gene — typed ncbi:Gene mirror + lexicon (public-domain; auto-downloaded)
scripts/provision-ncbi-gene.sh               # Homo sapiens (TAX_ID=9606 by default)

# UMLS — typed umls:Concept mirror + lexicon. LICENSED: you must supply your own
# Metathesaurus Level-0 zip at references/umls-<release>-metathesaurus-level0.zip.
scripts/provision-umls.sh                     # WRN-relevant semantic-type subset
scripts/provision-umls.sh --all               # all semantic types (large)

See Installation §2.6 for the full list of flags, env overrides, and the UMLS licensing constraints.

Building the lexicon image

The importers above load a corpus into a running kernel. For everyday work you want the other thing: a snapshot — a prebuilt RocksDB store carrying the whole lexicon, that a kernel can be started against directly. The demos, the parse harness and the D71 formalization service all expect one.

It is built in three steps, and each exists for a reason worth knowing:

# 1. RESEED — build a store from scratch against the CURRENT bootstrap.
#    `--umls-all` is not optional for a snapshot you intend to parse with: the
#    bare form loads an 8-TUI subset, which silently changes every measurement.
#    ~20 min, ~2.8 GiB out.
scripts/reseed-lexicon-db.sh --umls-all

# 2. ALIGN — layer the curated alignments on top of a copy of that store:
#    the wordnet↔umls concept merges, and the D68 claim-kind alignment that
#    lets «These findings» resolve to a landed claim.
scripts/build-alignment-snapshot.sh \
    --base ../db-snapshot/wordnet-umls-<date> \
    --out  ../db-snapshot/wordnet-umls-aligned-<date>

# 3. STAGE — copy it into the kernel's docker volume. `just up` does NOT do
#    this; it starts against whatever the volume already holds.
just stage-snapshot           # newest aligned snapshot, autodetected
just which-snapshot           # what is staged right now (reads its PROVENANCE)

A reseed is only needed when the BOOTSTRAP changes — the ontologies compiled into the kernel. kernel/tests/bootstrap_manifest_pinned.rs fails the moment one does, names the layer that moved, and lists the follow-through; an existing store would otherwise refuse to resume with ManifestDrift. Importing a corpus does not require one.

Two things the snapshot carries so you do not have to load them. The D62 encoding contract (encoding.esl) is in the kernel's bootstrap chain, because the kernel names its IRIs. The claim-kind alignment is layered by step 2, because it references wn: / umlscui: concepts that exist only after a lexicon import. Both used to be --chain-load steps that five separate callers each remembered.

For formalization specifically the kernel needs the live proposers and the WordNet Morphy dictionary, neither of which is in the default image:

scripts/provision-wordnet.sh download   # compose bind-mounts references/WordNet-3.0/dict
ANTHROPIC_API_KEY=sk-... just up         # the kernel is built with --features use-llm by default

Without the dict the served parser falls back to a no-op lemmatizer and every sentence comes back as a grammar cut; the startup log line Parse lemmatizer: … says which one loaded.

Note for WSL 2 users: all of the above installs into the WSL distribution (Ubuntu or similar), not Windows itself. VS Code's WSL remote extension is the smoothest way to edit the repo from Windows while compiling inside WSL 2.

Build and Test

just build        # cargo build --workspace
just test         # cargo test --workspace + deno test
just check        # fmt + clippy + deno lint

GPU acceleration for vector embeddings (optional)

D43 vector retrieval ships BGE-small-en-v1.5 via HuggingFace Candle, wired into the eigenius serve binary so the embedder pool is registered at startup and the post-Load sweep fires automatically against any layer that declares a core:VectorIndex Resource. The default build is CPU-only and requires no extra toolchain.

To opt into GPU inference at build time:

just build-gpu      # CUDA — needs CUDA 12.x toolkit (`nvcc`) + matching driver
just build-metal    # Apple Silicon
cargo build-gpu     # equivalent cargo alias, builds the CLI only

Both forward --features cuda (or metal) to eigenius-embedder-candle. The select_device() helper inside the embedder probes the accelerator at construction and falls back to CPU with a stderr warning if the device isn't usable.

At runtime, point the service at the embedder via eigenius.toml:

[embedder]
enabled = ["bge-small-en-v1.5"]
device = "auto"      # auto | cpu | cuda | metal — defaults to "auto"
batch_size = 32
fail_fast_on_missing_model = true   # refuse to start if a VectorIndex declares an embedder we don't ship

The same knobs are available as env vars (EIGENIUS_EMBEDDER_ENABLED, EIGENIUS_EMBEDDER_DEVICE, EIGENIUS_EMBEDDER_BATCH_SIZE, EIGENIUS_EMBEDDER_FAIL_FAST_ON_MISSING_MODEL) — env beats file, file beats schema defaults. With enabled = [] (default), the service still starts but vector retrieval is unavailable; that's the right shape for deployments that only use text retrieval.

For Docker, an opt-in GPU variant of the kernel image is in deploy/Dockerfile.kernel.gpu and a matching compose override in docker-compose.gpu.yml reserves a GPU on the host via nvidia-container-toolkit. Bring up the GPU-accelerated stack with:

docker compose -f docker-compose.yml -f docker-compose.gpu.yml build
docker compose -f docker-compose.yml -f docker-compose.gpu.yml up -d

Requirements: an NVIDIA driver, nvidia-container-toolkit registered as a Docker runtime (verify with docker info | grep -i nvidia), and Docker Compose v2 (Engine ≥ 23). The first boot downloads the BGE-small model files (~130 MB) into a named volume so subsequent boots reuse them.

Measured speedup, 1 007 GO Class corpus, batch=32, RTX 4070 (see docs/notes/d43-implementation-notes.md for full timings + caveats):

device	sweep	per-query
CPU, per-text	162 s	~130 ms
CUDA, batched	3.62 s	~30 ms

CLI

# Validate an Eigon-JSON file against the core ontology
cargo run -p eigenius-cli -- validate ontologies/examples/animals.json

# Load an Eigon-JSON file (validates and commits as a new layer)
cargo run -p eigenius-cli -- load ontologies/examples/animals.json

# Query the knowledge graph with EigenQL
cargo run -p eigenius-cli -- query 'USING "urn:eigenius:core:Class" MATCH Class(?c) { short_name: ?name } RETURN [] { short_name: ?name }'

# Query with a loaded file
cargo run -p eigenius-cli -- query --file ontologies/examples/animals.json 'MATCH "urn:eigenius:example:Dog"(?d) { "urn:eigenius:example:name": ?name } RETURN [] { "urn:eigenius:example:name": ?name }'

# Run a program's static checks (parse + output schemas; not a type-check)
cargo run -p eigenius-cli -- program-validate ontologies/examples/simple-program.json --ontology ontologies/examples/animals.json

# Execute a program with input data
cargo run -p eigenius-cli -- run ontologies/examples/simple-program.json ontologies/examples/animals.json --ontology ontologies/examples/animals.json

# Inspect a core ontology resource
cargo run -p eigenius-cli -- inspect "urn:eigenius:core:Class"

# Version
cargo run -p eigenius-cli -- version

ESL — Eigenius Surface Language

ESL is a human-friendly surface syntax that compiles to Eigon-JSON. It uses a two-layer design: HCL-style blocks for structural declarations (classes, properties, resources) and ML-style expressions for program bodies.

namespace core = "urn:eigenius:core";
namespace demo = "urn:eigenius:demo";

class demo:Document {
    description = "A text document for analysis.";
    requires demo:text;
}

property demo:text : core:string {
    description = "The text content of a document.";
}

resource demo:doc_001 : demo:Document {
    demo:text = "Eigenius is a typed knowledge graph platform.";
}

program demo:fetch : demo:Document -> demo:Document {
    let reply : demo:Document = HttpRequest(input);
    Construct demo:Document { demo:text = reply.demo:text }
}

This compiles to about 80 lines of Eigon-JSON. All CLI commands accept .esl files directly — the format is auto-detected by file extension.

# Compile ESL to Eigon-JSON (output to stdout)
cargo run -p eigenius-cli -- compile demo/document.esl

# Load and validate an ESL file
cargo run -p eigenius-cli -- load demo/document.esl

# Validate without loading
cargo run -p eigenius-cli -- validate demo/document.esl

The kernel's gRPC service also accepts ESL via content_type: "application/esl".

See docs/design/d7-esl-surface-syntax.md for the full specification.

Running the End-to-End Demo

The demo health-checks the orchestrator, loads a document into the kernel as Eigon-JSON and as ESL, and inspects and queries the result. Requires three terminals.

Prerequisites

# Rust kernel
cargo build -p eigenius-cli

# Deno orchestrator
cd orchestration && deno cache src/main.ts && cd ..

Terminal 1: Start the orchestrator

cd orchestration
deno run --allow-net --allow-env --allow-sys=hostname src/main.ts

Terminal 2: Start the kernel

cargo run -p eigenius-cli -- serve --orchestrator http://localhost:8080

Terminal 3: Run the demo

./demo/run.sh

This will:

1. Health-check the orchestrator
2. Load a document (Eigon-JSON) into the kernel
3. Inspect the core Class resource
4. Query all classes across core, program, and reflection ontologies
5. Load the same document as ESL directly into the kernel

Individual commands

You can also run individual commands against the kernel:

# Load resources (JSON or ESL)
cargo run -p eigenius-cli -- --endpoint http://localhost:50051 load demo/document.json
cargo run -p eigenius-cli -- --endpoint http://localhost:50051 load demo/document.esl

# Query
cargo run -p eigenius-cli -- --endpoint http://localhost:50051 query 'MATCH "urn:eigenius:core:Class"(?c) { short_name: ?name } RETURN [] { class: ?c, name: ?name }'

# Inspect
cargo run -p eigenius-cli -- --endpoint http://localhost:50051 inspect "urn:eigenius:core:Class"

Design Documents

The full set lives under docs/design/; the index below groups the load-bearing specs by area. Cross-cutting roots: Architecture v0.3 (authoritative system spec) and the Implementation Plan (phased build plan).

Foundations

Document	Description
D1: Eigon Serialization Format	Eigon-JSON / CBOR: IRI identity, three-layer type system, canonical form
D2: EigenQL Specification	Typed stratified Datalog: MATCH / DEFINE / FIBER, aggregation, full grammar
D3: Program Model	Program expression language, component model, scheduling
D5: gRPC API Specification	RPC surface, streaming query, error model, CLI/orchestration integration
D6: Execution Architecture	Kernel ↔ orchestrator boundary, activity dispatch, MCP placement
D7: ESL Surface Syntax	Two-layer design: HCL-style structural blocks + ML-style expressions

Type theory and programs

Document	Description
D6b: Reasoning Trace Schema	Trace classes, provenance chain, epistemic status, universe stratification
D9: NbE Unification & Type Extensions	EigenTT NbE, ground-type resolution, capability modes, trace storage
D11: Codata and Streams	⚠️ Superseded — the codata half is retired; §5.3/§5.4 (task state, concurrency) survive
D18: Ontology-as-Types Resolution	find_sigma_field chain resolution, CheckCtx, inference-mode rules
D19: Inductive and Sized Types	Inductive types and indexed families. The sized-termination and codata halves are retired
D32: Chain-Mirrored EigenTT Inductives	formulas:FormulaTerm and the ESL formula(...) Pratt-parsed sublanguage
D39: Justification Logic Institution (v2 draft)	Artemov-style JustificationTerm + type-theoretic JustifiedBy : JustificationTerm → Prop → Type indexed predicate with opaque ChainWitness grounding projected from the reflection ontology's existing class-membership and Trace-emission events
D46: Prop Universe and Proof Irrelevance

Storage, lifecycle, commit

Document	Description
D4: Storage Key Encoding	Key encoding for RocksDB / TiKV, column families, index layout
D13: Durable Kernel State	serve --db, seeded bootstrap, drift-refusal, restart re-registration
D21: Task Traces and Checkpointing	Per-task trace keys, checkpoint primitive, resume sweep, task RPCs
D23: Out-of-Core Layer Architecture	Topology/content split, per-layer blooms, CAS, GC, per-layer triple index
D24: Schema Versioning Policy	On-disk SCHEMA_VERSION, migration framework, boot-time check (+ Schema Changelog)
D25: Chain Consolidation	Background compaction of long chain spans into single resolved layers
D33: Partial-Order Chains	Lifting the chain abstraction from a linear DAG to a partial order
D41: Commit Pipeline	Single-layer pipeline + multi-layer orchestrator, FIFO drain, emission policy

Layer reconciliation and merge

Document	Description
D20: Layer Reconciliation	Witness / Rename / SchemaQuotient / Restructure strategies, conflict surface
D36: Merge Resolution UX	Notebook merge flow: six-state machine, cascade gate, on-rail workspace
D37: Lambda Surface and Typed Merge Comorphisms	merge_comorphism ESL surface, EigenTT lambda well-typedness
D38: Merge Provenance and Witness Discovery	Chain-resident MergeResolutionRecord, off-span witness search

Institutions and verification

Document	Description
D14: Institution Realisation	Institution trait (extract_typed / reify / query), ontology-first declarations, triadic comorphisms, Verdict dispatch. Supersedes D10.
D26: Runtime Substrate	Language-agnostic substrate for embedded scientific runtimes (Julia, Python, …); image-vs-graph boundary, digest-anchored deployment
D27: Julia Institutions	First runtime-substrate instance with five reference institutions (Symbolics, IntervalArithmetic, Catalyst, DiffEq, JuMP)
D28: Lean 4 as Verification Institution	Lean 4 proof checker as a verification institution via nanoda_lib
D29: Eigon → Julia Mirror Spec	Mirror generator: closure walker, content-addressed Julia packages
D30: Eigon → Lean Faithful Translation	LeanPackageMirror, audit anchor, baked EigeniusFFI Lake package
D31: External Institution Lifecycle	mirror create → env build → env create → institution install lifecycle
D40: Chain-Mirrored Lean Expressions

WASM extensibility (removed 2026-07-08)

Document	Description
D12: WASM Extensibility	Historical — WASM module lifecycle, host imports, capability levels, fuel/memory limits

Notebook, SDK, and workspace

Document	Description
D22: Notebook UX and TypeScript SDK	React notebook, @eigenius/client, notebook ontology, content-addressed publish
D34: Notebook Chain Workspace	Workspace rail destinations (branches / tags / history / merge / GC)

Domain and vision

Document	Description
D35: Software Engineering Knowledge Graph	Applying the platform to its own codebase as a worked domain
Manifesto	Project ethos and posture
Vision	Long-horizon target for the platform
Life Science Requirements	Driving requirements from clinical / translational use cases

Prose to typed propositions

Document	Description
D62: Encoding Engine — prose to trees	The categorial-grammar approach: lexicon:Cat as an inductive, the ⟦cat⟧ → sem_type homomorphism, CN-as-types, and the felicity obligation that a lexical entry's semantics must inhabit the type its category denotes
D63: DCG engine — English grammar	The grammar itself — multimodal slashes after Baldridge, coordination, comparatives, the closed-class inventory, and lexicon augmentation from WordNet + UMLS
D64: LLM anaphora resolution	The proposer suggests a referent among assembled candidates; the kernel re-gate is the veto. Holes are typed by their restrictor, so «these findings» resolves only to findings
D65: Lexicon runtime — lazy and scoped	Making a multi-million-entry lexicon usable at parse time: declared value/text indexes, lazy probing instead of full-layer scans
D66: Definitional lifting and witness normalization	Landing parsed sentences as chain resources, and normalizing the witness keys they produce
D70: Named entities — syntax vs denotation	Separating how a name is spelled from what it denotes
D71: Document formalization service	The pipeline as a service operation — FormalizeDocument, its result surface, and the MCP tools that drive it

Reasoning, witnesses, and the fusion arc

Document	Description
D52: Measurement statistics institution	The in-process statistics institution — ANOVA family, sample sets, effect sizes, outlier policy; emits one InstitutionEmittedDerivation per effect
D54: Reasoning lemma citation	Citing a committed ReasoningSentence as a lemma, and what its witness entitles
D57: Schema.org vocabulary mapping	Lifting an external vocabulary through the OCI runtime as an attested derivation
D73: Justification logic — witnesses and traces	The polynomial as primitive; how JustifiedBy relates to the trace store
D75: Fusing EigenTT and the knowledge graph	The diagnosis: the layer chain is Γ_env and a resource is a record were one problem. Eight witnessed defects; three follow-ons
D76: The typing environment	Seam A — the chain becomes Γ_env. De-inlining Exp, declaration-level universe parameters, Const(iri, levels), δ in conversion, a derived recursor motive
D78: Resources as records	Seam B — validation becomes clause-8 evaluation against Val::Record
D79: The representation of inductive types

Evaluation methodology

Document	Description
D50: Benchmark Evaluation Approach	Dormant 2026-09-05. Experimental design testing whether forcing the agent to capture reasoning as typed justified propositions improves performance — three conditions (baseline / chain-of-thought / Eigenius-structured), 15 ScienceAgentBench + 11 EngiBench Level 3 tasks, six per-family base ontologies, scoring and pilot phasing
D51: Benchmark Implementation Gaps	Dormant 2026-09-05. Companion to D50 — the eight implementation gaps ordered along the critical path (D49 machinery, Lean → Reasoning comorphism, D39 v2 artifacts, MCP surface, base ontologies, agent skill, three-condition harness, per-task wiring), per-gap effort sizing and sequencing

Contributing

Contributions are welcome — bug reports, design discussion, and patches alike. The project is early; the structural decisions matter more than feature velocity, so please open an issue before any non-trivial change so we can align on shape first.

• Bugs and feature requests: open an issue.
• Discussion: general design questions and ideas live in GitHub Discussions.
• Patches: fork, branch, run just check (fmt + clippy + lint) and just test, then open a PR. All commits must pass CI.
• Code style: cargo fmt --all is enforced; clippy runs with -D warnings.
• Design docs under docs/design/ are the source of truth for system shape — substantive changes should land as an updated design doc alongside the code.

By contributing, you agree your contributions are licensed under Apache-2.0.

License

Apache-2.0