Eigenius

Type: kb/types/note.md

Evidence basis: source inspection of Eigenius at commit 4bc3bb2 (2026-08-12), including its agent method documents, captured 2026-08-18; Docker, provider, recovery, cancellation, reasoning, and Lean paths were not run.

Eigenius has two agentic layers. Its runtime is an externally driven typed knowledge, execution, and verification substrate: a client chooses an operation, the Rust kernel evaluates the program and commits results, and a Deno orchestrator supplies registered IO handlers. The active LLM handlers do not contain a repeated planner/tool-use loop. Separately, the repository ships agent-facing reference documents that tell a host agent how to frame, ground, execute, and audit reasoning through the substrate. The README says these documents are not auto-loaded skills; a user or host must supply them. Eigenius is therefore an agent-operated substrate with an optional natural-language control protocol, not a runtime that starts or owns its own model loop. This classification follows agent-is-a-tool-loop: one model call inside an evaluator is not by itself an agent, while a procedure followed by the host can still organize a loop outside the runtime.

A curated facade over shared kernel state

The MCP registry exposes fourteen tools: seven exploratory reads, four commit or program operations, and three health or task observations. It omits branch and tag mutation, merge, consolidation, garbage collection, and task cancellation. Its mutation surface still includes Eigon loads and program execution. The selection is a useful capability menu, but it is only one entry surface.

The HTTP adapter creates a fresh MCP server and transport for each request, then connects them to a long-lived shared kernel client. Its statelessness concerns the lifetime of protocol objects, not the lifetime or isolation of graph state. Stdio MCP likewise connects to an already-running kernel. Callers entering through either mode therefore operate against shared durable state rather than private per-request state. (HTTP adapter; stdio entry point)

MCP curation also does not define the deployed authority boundary. The orchestrator registers an EigeniusKernel passthrough, while the kernel serves the full RPC service. The inspected routers contain no credential, caller-identity, scope, authorization-interceptor, or TLS checks. The protobuf service includes branch and tag mutation, merge and resolution, consolidation, garbage collection, load, program execution, reflection, and cancellation—operations wider than MCP. (Orchestrator server; kernel lifecycle)

The shipped Compose file publishes ports 8080 and 50051 and mounts the Docker socket into the orchestrator. In that deployment shape, a caller able to reach the services is not confined by the MCP tool list and may reach mutation surfaces backed by a process with root-equivalent Docker-daemon authority. This is conditional on reachability: the inspected files do not establish internet exposure, and an operator could add controls outside this Compose definition.

The kernel owns execution; models supply bounded effects

Ordinary RunProgram is synchronous. With a persistent backend, it first creates a durable task record; it then evaluates and commits before returning. The recursive evaluator gives explicit order to effectful computation: a let binding's value precedes its body, a component argument precedes dispatch, a function precedes its application argument, a pair's left side precedes its right side, and construction fields follow stored order. The inspected evaluator contains no machinery that discovers independent let dependencies and dispatches them concurrently. That is narrower than the automatic scheduling described in the D3 and D6 design records. This finding does not cover element-level parallelism inside Map or Reduce, whose helper loop was not inspected. (program service; evaluator; D6)

Effectful component applications cross a kernel-selected boundary to registered orchestrator handlers. CompleteText and CompleteJson each make one Anthropic completion per invocation. The caller may supply model and generation parameters. JSON completion additionally validates the response against a kernel-generated JSON Schema, then expands short names into IRI-keyed resources. The separate LlmAdapter is an interface with unfinished implementation work, not an active planner. A model thus produces one component value under kernel control; it does not select the program's next action. (text completion; JSON completion; LLM adapter)

The agent loop is a manually loaded method

The repository's agent guide teaches a coding agent the platform model, languages, MCP tool choices, and common workflows. Its reasoning protocol supplies the higher-level loop: frame and ground an objective, plan on the chain, execute while producing evidence, compose warranted conclusions, and audit the resulting graph. The companion grounding method makes retrieval and citation part of that loop. These are natural-language system-definition artifacts executed by the host model. They do not run unless the host reads and follows them, and the runtime does not persist a controller that schedules their phases.

The method combines hard and procedural controls. A ReasoningSentence carries a proposition, a justification term, and a certificate. On the institutional load path, ValidateJustification type-checks the certificate against JustifiedBy(justification, proposition); a Fails verdict rejects the commit. A committed sentence then becomes a citable Verified witness in the kernel's witness index. The sentence bears the proposition and warrant; the emitted verdict records that the gate ran, and is not itself the proposition to cite. (reasoning validator; witness index; D54 lemma citation)

This separates execution history from warrant. A ProgramTrace records what an effectful program did. A justification certificate records why a proposition is admitted, relative to its cited witnesses and assumptions. Some other protocol checks—including discovery and graph-reachability checks—are EigenQL queries the method tells the host agent to run. They are not a universal kernel scheduler or a gate automatically applied to every mutation. The method's four epistemic grades are therefore an authoring and warrant discipline with hard enforcement at named boundaries, not proof that every resource in every commit path has the same factivity or verification history.

Persistence does not imply a uniform verification history

Eigenius applies different commit pipelines to different mutation routes. A load can proceed through build, structural validation, retroactive validation and cascade, AutoOnLoad institution dispatch, and persistence; successful persistence can then trigger vector sweeps. Kernel-emitted follow-up layers take a build-and-persist route that intentionally skips structural validation. Program runs use WithRetroactive, not WithInstitutions, so generated outputs do not pass through AutoOnLoad. Normal program completion commits produced resources, any output or program resources needed for reference integrity, and a ProgramTrace, then reports the branch compare-and-swap or merge result. The ReasoningSentence gate belongs to the institutional load path; it does not turn an ordinary program result into a checked justification. (commit pipeline; program commit path)

The graph is typed, and some paths can reject malformed resources or failed institutional claims. But a persisted resource does not, by that fact alone, reveal which checks ran. Ontology shape describes an admissible form; it does not prove that a particular pipeline validated every committed value.

Successful program output is unconditionally classified as DerivedResource, marked epistemic:derived, and linked to its trace. The trace mirrors effectful structure and can include component identity, input hash, output, provider and model, token counts, latency, and a cache field. Pure leaves have no trace nodes. These records witness that the kernel carried out a derivation path. Because stamping follows successful execution regardless of content truth, it does not establish the factual correctness of an LLM completion, external computation, or source encoding. That limit is the concrete Eigenius instance of the distinction in trace-extracted-memory-earns-authority-per-operation-not-at-capture. (trace representation; reflection ontology)

Durable tasks provide positional replay, not exactly-once effects

With persistent storage, each run gets a UUID task in one hardwired nil-UUID session and pins the branch head seen at entry. Task metadata, positional outputs, and checkpoints are stored under session and task keys. A step commit can atomically batch updated metadata, output bytes, and checkpoint state. This is durable replay state, but its identity is positional: (session_id, task_id, step_seq). On a hit, the evaluator parses and returns the saved output without checking component IRI, input hash, arguments, or layer. (task storage; effect hooks)

Remote execution occurs before the positional step is committed. From that call order, a crash after the external side effect completes but before commit_step lands can cause the effect to be dispatched again. The implementation therefore supplies at most one stored observation for each successfully committed position; it does not establish exactly-once external execution. This is a code-path inference, not a fault-injection result.

Startup recovery is also weaker than normal completion. It does not load last_checkpoint, advance the step counter past it, or feed checkpoint state into resumed evaluation. Instead, it starts at the program root, where already committed positional outputs may be reused. It rebuilds the pinned chain, but a missing input IRI—including an originally inline input—can be replaced with an empty resource, and recovery supplies no institution index or runtime. On success it marks the task complete without running the normal output-and-trace commit path or populating result_layer_head. Recovery selects Running and Suspended records, runs up to four concurrently, and passes a max_attempts value that the resume function does not use. Resume may reuse work, but it is not equivalent to normal durable completion. (startup recovery)

Program cancellation is not operational in this path. CancelTask changes persisted status to Cancelling, but it neither signals the live task context nor reaches a cancellation check in the effect engine. Restart ignores Cancelling, and MCP does not expose cancellation. Eigenius does implement cooperative cancellation for vector sweep and reindex drivers, so the narrower conclusion is about program tasks, not all background work. (task RPC; sweep driver)

Cross-run cache identity and trace visibility are narrow

Deterministic-component memoization is separate from per-task positional replay. Its executable key is SHA-256(component_iri || canonical CBOR(input)). It omits component arguments, the pinned layer, and component-definition version, although D6, D21, and trace comments describe wider identities. The code therefore does not establish that reuse remains equivalent when those omitted parts of the semantic context change. This does not mean every cached value is wrong; it means the implemented key supports a narrower guarantee than the design text. (memoization path; D21)

A cache hit returns the saved output without a trace node and does not rewrite the cache flag to true. Current traces and their metrics therefore do not reliably reveal reuse, despite the cache fields described in the reflection ontology and README.

External-runtime controls stop short of full provenance and authority isolation

Published runtime scripts resolve against the pinned read layer. Docker execution requires an image digest and creates an auto-removing container for each invocation. The spawner explicitly treats Docker-socket access as root-equivalent and the host as the security boundary. These controls constrain each invocation, but the process that enforces them still holds root-equivalent Docker access. In the shipped deployment, unauthenticated callers who can reach a program-execution surface can ask that process to run only the operations mediated by registered handlers; the cited code does not show arbitrary Docker-daemon control from RPC. The concrete container-option builder was not part of this evidence set, so this review does not claim default network or Linux-capability restrictions as observed implementation facts. (Docker spawner)

The substrate constructs a partial RuntimeInvocation with observed language, optional image digest, timestamps, numerical metadata, and an optional resolved method. Ordinary RunRuntimeScript and CallRuntimeMethod handlers log its byte size and discard it, returning only the output through the component response. Normal program execution therefore commits a ProgramTrace, not the full invocation record described by D26 and D56. This finding is limited to the ordinary component path; the inspected evidence does not establish whether the separate external-institution response later persists its partial record. (invocation builder; runtime-script handler; runtime-method handler)

Lean checks proof terms within conditional correspondence bounds

Lean verification is an in-process institution selected by a chain declaration. Its checker stages supplied lean4export bytes, requires the named theorem, and asks nanoda to check every declaration. Parse or load failure, a missing target, a type error, or a disallowed axiom yields Fails. The executable institution uses a fixed allowlist: propext, Classical.choice, Quot.sound, and Lean.trustCompiler. (checker; institution)

After nanoda accepts a proof, a present mirror anchor triggers checks of embedded-file hashes, source-layer ancestry, and claim-class coverage. A present mirrored proposition must reference that class. These correspondence checks are conditional: missing mirror_iri, claim_iri, or proposition skips the corresponding checks. Holds directly supports proof validity under the allowlisted axioms. It supports correspondence to a graph claim only when the optional anchors are present and pass. The path checks supplied proof terms; it neither synthesizes a proof nor establishes that natural-language material was faithfully encoded. formal-systems-assess-explanatory-reach-through-causal-and-proof supplies the general reason for keeping proof validity and translation fidelity separate.

Comparison judgment

At this commit, Eigenius warrants credit for typed kernel-controlled evaluation, explicit effect boundaries, a manually loaded host-agent reasoning protocol, checked justification certificates on its intended load path, durable graph mutation, pinned reads, derivation traces, path-specific validation and institution hooks, digest-pinned external execution, and optional proof checking. It should not be compared as if it supplied an internally owned or automatically adopted agent loop, authority confinement by MCP, uniform verification, truth-certified derivations, exactly-once effects, checkpoint-equivalent continuation, operational program cancellation, complete cache identity, complete runtime provenance, or unconditional graph-to-proof correspondence.

The README and design records describe intended architecture ahead of several executable paths: automatic scheduling, asynchronous tasks, checkpoint resume, bounded retry, wider cache identity, cancellation, and complete runtime provenance. Those documents are useful for direction, but the narrower code paths govern present-tense claims here. Because the Docker, LLM-provider, task-recovery, cancellation, and Lean integrations were inspected rather than executed, this review establishes code correspondence at the pinned version, not observed end-to-end behavior.

Relevant Notes: