Paper deep dive
Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning
Hans-Martin Will, Allen L. Brown, Matthew Fuchs
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:As "AI Scientists" emerge to drive research via the Model Context Protocol (MCP), systems relying on ephemeral scripts will fail. The sheer scale of stateful, interconnected evidence requires a machine-walkable warranty grounded in a purpose-built database architecture. Eigenius is an open-source, typed knowledge-graph DBMS built on a single premise: answering the audit question ("what do you know, and what is your warranty?") requires a unified kernel. By tightly coupling the type system, storage engine, and integration protocol, Eigenius turns data provenance into a structural invariant rather than a property reconstructed across subsystem boundaries. The kernel rests on three pillars: a dependent type theory woven through the core, institutions acting as strongly typed integration boundaries, and a content-addressed immutable storage layer. On this foundation, epistemic status (declared/observed/derived/verified) is enforced as a strict commit-time invariant. Cross-system translations (comorphisms) are checked at commit and materialized directly into the graph as durable, first-class resources. To eliminate O(N^2) polystore bottlenecks, shared on-chain intermediate representations (IRs) collapse multi-system translations to identity. Crucially, this architecture unifies both domains of scientific epistemology: it relies on justification logic for empirical science, while embedding a fast, in-process term checker to safely evaluate formal mathematical proofs (via Lean 4) without IPC overhead. In an end-to-end recomputation of a published Nature study from fragile scripts to a materialized evidence graph, all 52 derived conclusions hold from pinned data, surfacing four machine-checked discrepancies in the original study.
Tags
Links
- Source: https://arxiv.org/abs/2608.04457v1
- Canonical: https://arxiv.org/abs/2608.04457v1
PDF not stored locally. Use the link above to view on the source site.
Full Text
32,890 characters extracted from source content.
Expand or collapse full text
Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning Hans-Martin Will The Eigenius Project United States A. L. Brown Jr. Docimion United States Matthew Fuchs Docimion United States Abstract As “AI Scientists” emerge to drive research via the Model Context Protocol (MCP), systems relying on ephemeral scripts will fail. The sheer scale of stateful, interconnected evidence requires a machine- walkable warranty grounded in a purpose-built database architec- ture. Eigenius is an open-source, typed knowledge-graph DBMS built on a single premise: answering the audit question (“what do you know, and what is your warranty?”) requires a unified kernel. By tightly coupling the type system, storage engine, and integration protocol, Eigenius turns data provenance into a structural invariant rather than a property reconstructed across subsystem boundaries. The kernel rests on three pillars: a dependent type theory woven through the core, institutions acting as strongly typed integration boundaries, and a content-addressed immutable storage layer. On this foundation, epistemic status (declared/observed/derived/ver- ified) is enforced as a strict commit-time invariant. Cross-system translations (comorphisms) are checked at commit and materialized directly into the graph as durable, first-class resources. To elimi- nate푂(푁 2 )polystore bottlenecks, shared on-chain intermediate representations (IRs) collapse multi-system translations to iden- tity. Crucially, this architecture unifies both domains of scientific epistemology: it relies on justification logic for empirical science, while embedding a fast, in-process term checker to safely evaluate formal mathematical proofs (via Lean 4) without IPC overhead. In an end-to-end recomputation of a published Nature study from fragile scripts to a materialized evidence graph, all 52 derived con- clusions hold from pinned data, surfacing four machine-checked discrepancies in the original study. Keywords Knowledge graphs; epistemic provenance; institution theory; Gro- thendieck construction; formal verification; Lean 4; dependent type theory; typed merge; content-addressed storage; MCP 1 Introduction Scientific data consumption is shifting. As end-to-end “AI Scientists” (e.g., OpenAI Rosalind, Claude Science) emerge, autonomous agents are driving research loops, firing thousands of inferences via the Model Context Protocol (MCP) [23]. However, current data infras- tructure is unready. Today, scientific arguments are captured as ephemeral webs of linked scripts and narrative prose. Manual audit- ing across these fragile pipelines was once inconvenient but possible for humans. For an autonomous agent, a cryptographically secure, fully walkable proof chain is a load-bearing pillar. Formalizing this requires managing millions of stateful, interlinked concepts—from gigabyte-scale matrices to granular logical warrants—demanding a purpose-built database architecture. The core ambition of a machine-auditable scientific foundation is not new. In 2008, Pharos [1] articulated a clear vision: enforcing the scientific method by making inference and workflow machine- auditable. Pharos shipped a credible prototype, eventually produc- tized as Microsoft Amalga Life Sciences 2009 [2]. However, that vision outpaced its infrastructure. Without a trusted kernel acting as a switchboard, the system relied on fragile peer-to-peer bridges— stitching together SQL Server, DataNet via TSVs and .NET stored procedures, and the HOL theorem prover via F#. Lacking a formal protocol like institutions to integrate these distinct forms of reason- ing, there was no central place for a unifying type theory to live. While the mathematical theories required to solve this long predate Pharos, their necessity as load-bearing database infrastructure was not yet appreciated. Eighteen years later, synthesizing them into a unified engine has become critical. We introduce Eigenius, an open-source 1 typed knowledge- graph DBMS that revisits this architecture from the ground up. We argue that a purpose-built kernel—wholly owning the type system, storage layer, and integration protocol—provides structural guarantees that a loosely coupled stack of best-of-breed tools cannot match. By integrating dependent type theory, Grothendieck institutions, and content-addressed storage, Eigenius turns the audit story into a structural invariant of the data model rather than a fragile reconstruction across subsystem seams. Contributions. C1. A self-describing typed-graph data model that unifies empir- ical justification logic and formal mathematical proof. Epistemic stratification (declared/observed/derived/verified) is enforced as a strict commit-time invariant. For formal verification, an embedded in-process term checker safely evaluates opaque proof payloads and binds them to the graph’s schema without IPC overhead. C2. An integration protocol that introduces Goguen and Burstall institutions to the database world as a strongly typed generalization of the stored procedure. Cross-system translations (comorphisms) are statically checked at commit and their outputs materialized directly into the chain as durable resources. C3. A solution to the푂(푁 2 )polystore adapter bottleneck. By lifting a shared, strongly typed intermediate representation (IR) natively into the graph’s schema, comorphism transformations between systems sharing that IR collapse to pure identity. C4. An end-to-end recomputation and re-encoding of a published Nature study, proving the necessity of a database architecture for complex arguments. Moving from ephemeral scripts to a fully ma- terialized evidence graph, 52 of 52 derived conclusions hold from pinned data, surfacing four discrepancies. 1 The academic prototype and experimental codebase are available for inspection at https://github.com/eigenius/eigenius 1 arXiv:2608.04457v1 [cs.DB] 5 Aug 2026 Will et al. 2 Pharos and the Agent Inversion To understand Eigenius’s design, it is useful to examine the ar- chitectural ceiling hit by Pharos [1]. Pharos attempted to build a machine-auditable database by federating a graph store (DataNet) with probabilistic reasoning (Infer.NET) and formal proofs (MeTaL). This federated approach exposed a fundamental limit: each sub- system had its own typing and durability story. Schema lived in a different ontological category than instance data; bridges were opaque custom code; and standard storage recursion could not ex- press institution-dispatched queries that both read and write the chain mid-evaluation. Eigenius replaces this federated stack with a unified mathemati- cal kernel (Table 1). The agent inversion. The last row of Table 1 highlights the shift making this unified architecture mandatory: the transition from human researchers to autonomous AI agents. A coding agent con- verges on a correct program through a tight loop with a compiler and linter, turning errors into localized, machine-checkable signals. An agent reasoning in prose has no such loop. Supplying one for scientific thinking motivates what follows: capturing knowledge as typed resources makes the structural type checker the agent’s compiler, while commit-time epistemic gates act as its test suite. Closing that loop with an agent reasoning natively through the substrate is future work; this paper reports the database kernel required to run it. 3 Data Model and Epistemic Stratification Everything in Eigenius is a Resource (IRI identity, class-membership claims, typed properties), extending Atomic Data [15] with a de- pendent type system and institution machinery. The ontology is self-describing; schema and data are unified, so declaring a class simply means committing a resource. The unit of commit is a layer— an immutable resource set with a parent pointer. Layer identity is content-addressed (SHA-256 of canonical CBOR [7]), forming a Merkle commitment to graph history where class resolution walks the chain. Branches and merges make the layer history a lattice whose joins are typed merges (Witness, Rename, SchemaQuotient, Re- structure). These act as chain-level functorial data migrations [6]: typed transformations between schema-and-instance states, not textual reconciliations. Epistemic stratification. A prover discharges a mathematical claim because its leaves are axioms; a scientific claim’s leaves are observations and conventions — an instrument reading, a chosen훼— that no prover can discharge. So the kernel checks the composition while the grade records what stands behind each leaf: a justification logic [18] whose warrants are deliberately not all factive. Every resource carries an epistemic status computed from its provenance graph: Declared (authority without evidence, checked for well-formedness), observed (recorded with external provenance), derived (produced by a typed computation), and verified (carries a formally re-checked proof term). The categories are structural base classes (DeclaredResource,ObservedResource, etc.) enforced by the validator at commit. The protocol that moves a resource between categories is the same protocol the system uses to plug in reasoning. Institutions declare commit-time triggers: the kernel fires matching queries on every commit. The handler returns a typedVerdict(Holds/Fail s ); promotion to verified means “the formal verifying institution returned Holds.” The verdict itself is chain-resident. Scope. Eigenius’s audit chain is re-walkable: an auditor replays the recorded warrants from the graph alone. Making it re-runnable — governing the processes that produce warrants, not merely record- ing them — is the companion system KlinikOS [26], described sepa- rately. Verification as a dependent pair. DataNet kept a type and its inhab- itants in two referentially-linked tables. In dependent type theory, that referential integrity is aΣ-type: a pair(푇,푡)with푡:푇, which Eigenius makes first-class as a single resource. Because EigenTT fully represents logical propositions natively, the kernel validates a claim’s proposition푃:Sort0 (Prop) strictly upon standard ingestion. However, elevating a claim to verified status requires committing it as a fully inhabited dependent pair(푃,푡). While empirical reasoners supply structural terms to produce derived resources (§6), a formal institution uses Lean 4 to supply a verbatim proof payload for푡. Only for claims seeking verified status does the kernel invoke its in-process verifier to statically re-check this opaque payload. The payload meets the kernel through an export comorphism휄relabel- ing the proposition, ensuring푃= 휄푇. At commit, the kernel checks the native proposition it owns, leaving the heavy proof obligation to the institution. The regulator’s question, “how do you know X is safe?”, is a typed query against the chain. 4 Institutions, Comorphisms, and EigenQL To integrate external reasoners (ODE solvers, theorem provers) into a DBMS, the standard tool is the stored procedure. Because stored procedures assume a flat relational world, Eigenius introduces insti- tutions [3] as a strongly typed generalization for knowledge graphs. Scientific arguments constantly cross seams. Eigenius models these crossings as comorphisms: strongly typed ETL pipelines exe- cuted natively inside the engine. What category theory describes as a Grothendieck construction, the database sees as a federated query planner that routes execution based on the rich EigenTT type of the payload. An institution registers itself via ontology resources, declaring its typedExportFormats,ImportFormats, andComorphisms. The DBMS kernel interacts with them through three trait methods: extract_typed, reify, and query. A comorphism pipeline extracts a payload of type푆, applies a transformation푚:푆 → 푇, and reifies output푇into a target re- source. Because this executes inside the kernel, the engine statically type-checks at commit that푚’s signature perfectly matchespay load(export)→ payload(import). Type-incorrect translations are rejected exactly like schema violations, turning cross-system data exchange into a commit-time invariant. Institutions run either out- of-core on a containerized substrate (Julia/R) or are linked directly into the kernel binary for fast, in-process checking (Lean 4). Justification and statistics as pluggable logic. The epistemic grad- ing from §3 is not hardwired into the engine; justification logic itself 2 Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning Table 1: Pharos (2008) vs. Eigenius (2026), by architectural concern. ConcernPharos (2008)Eigenius (2026) Schema realizationCompiled to SQL Server tables; instances stored as rowsSchema is data: value and type are one resource, read as aΣ- type (푇,푡) Storage substrateSQL Server; query planning inheritedRocksDB KV store; content-addressed immutable layers; four typed merges Recursion / querySQL Server TVFs driven by SPARQL compilation Kernel-owned seminaive-fixpoint evaluator overDEFINEd rules Shared payload languageNone; bespoke per-pair translationChain-mirrored MLTT fragment; comorphisms collapse to iden- tity Reasoning integrationBespoke bridges (MeTaL↔DataNet); proof translation is infras- tructure Grothendieck institutions checked at commit; proofs/outputs are chain-resident data Evidence modelA conclusion’s support lives inside MeTaL or Infer.NET as en- gine state A statistics institution recomputes results; a reasoning insti- tution checks each justification-logic term [18] against chain- resident witnesses Primary userHuman researcher; audit by inspection Designed for AI agents over MCP; the chain is the audit sub- strate User surfaceSPARQL window, graph viewer, VS-style workbenchMCP tools for agents; React notebook for humans; TypeScript SDK is an attached institution. The replication in §6 demonstrates this by composing two pluggable reasoners. First, a statistics institution connects empirical computation to the commit path. It fires on a committed statistical-analysis plan—a recipe, not a claim: resource wrn:wrn_dep_plan : stats:StatisticalAnalysisPlan stats:sample_set = wrn:wrn_dep_sampleset; stats:alpha = 0.05; stats:directionality = OneSidedWitnessed( "urn:...:msi_directionality_witness"); stats:variance_assumption = RankBased(); stats:outlier_exclusion = Identity(); No푝-value and no conclusion appear anywhere in it; even the choice of a one-sided test cites a chain resource rather than being a free parameter. On commit, a verification trigger recomputes from pinned data and emits two coupled derived residents: a verdict, and a result whosecanonical_propositionisstats:lt(stats:mean_d iff_of(s),0)— the proposition tested — carrying anIsDerivedA switness. The chain commits a rerunnable procedure, not a bare claim. Second, a reasoning institution discharges the conclusions stand- ing on those empirical results. Each conclusion is a proposition paired with a justification term — a typed accounting, in the sense of Artemov’s justification logic [18], of how it was reached. While the kernel provides the generic typing rule to discharge leaves (syn- thesizing the witness inhabitant from the layer’s witness index, so a leaf naming no chain-resident warrant fails to type-check), the actual justification logic is just another institutional plugin. A de- rived leaf is a statistics result, a declared leaf a named bridge or rule; the four-warrant taxonomy is thus a justification logic enforced by composition across the engine’s query and commit paths. Materializing the boundary: durable translations. In traditional federated databases or reasoning orchestrators (like Hets [8]), cross- system translations are ephemeral: computed in volatile memory to bridge a gap, then discarded. Because Eigenius treats both schemas and proofs as typed graph resources, a crossing’s warranty—its source resource퐶 푆 payload푆 payload푇 target resource퐶 푇 chain resource (content-hash IRI) extract (source institution) 푚 : 푆 →푇 (typed term) reify (target institution) commit + verification kernel type-checks푚 at commit Figure 1: The comorphism pipeline. The kernel type-checks the transformation푚against the export and import payload types at commit; the reified target resource is then reinserted into the chain as a first-class, content-addressed resident. typed translation—is just data. The reify step’s output (Figure 1) is not a transport-only intermediate; it is materialized back into the chain at a deterministic content-hash IRI (urn:eigenius:comorphis m-output:tail:hex), or at a caller-named IRI under anINTOclause. Identical translations naturally deduplicate via content addressing; commit-time triggers fire on the newly materialized translation; and downstream queries pattern-match it exactly like native data. The seam is crossed once, and the translation becomes a durable, verifiable graph resident. Eliminating adapter cost via shared graph IRs. Polystore systems rely on pairwise adapters to move data between subsystems, cre- ating an푂(푁 2 )integration bottleneck. Eigenius flattens this cost by lifting a shared, strongly typed Intermediate Representation (IR) directly into the graph’s schema. When institutions agree on a payload drawn from the kernel’s own type theory, the adapter degenerates to pure identity. For example, the mathematical payload language isFormulaTer m—a typed AST modeled natively in the graph. The operator catalog 3 Will et al. is a set of chain resources, rank-checked at commit. All five Julia institutions (Symbolics, IntervalArithmetic, Catalyst, OrdinaryDif- fEq, and JuMP-HiGHS) consumeFormulaTermas their native input. Because they share this graph-native IR, all comorphisms between them are identity transformations. The푂(푁 2 )polystore integration cost is eliminated by mod- eling a shared, strongly typed intermediate representation natively in the graph. EigenQL: typed Datalog with institution dispatch. The query lan- guage is a typed stratified Datalog with aggregation,DEFINEd recur- sion, and two clauses particular to the institutional setting.FIBER dispatches execution into an external institution mid-query.INTO acts as an inline materialization step: it pins the external engine’s response back into the chain at a named IRI, lifting it through the commit pipeline. The query below matches docking results, coerces each through thedock_to_assaycomorphism inline, dispatches the coerced value into the assay institution’s validation query, and pins the typed verdict back into the chain: USING "urn:eigenius:dock:DockingResult" USING INSTITUTION "urn:...:assay" AS assay MATCH DockingResult(?d) compound: ?c FIBER assay:validate_prediction candidate: dock_to_assay(?d) -- inline comorphism AS ?v INTO "urn:eigenius:run:val_42" RETURN [Validation] compound: ?c, verdict: ?v TheINTOtarget becomes a chain-residentValidationresource atu rn:eigenius:run:val_42. Neither clause fits a traditional TVF:FIBE R invokes complex typed reasoners outside the RDBMS, andINTO safely triggers validated materialization mid-evaluation. 5 Formal Verification as a Database Invariant While empirical science captures its warrants via justification logic andDerivedResourcecommitments (§3), pure mathematics requires absolute proof. To enforce the stricterVerifiedResourcegrade, the database must ingest, store, and statically re-check the proof itself on the commit path. Doing so requires solving three architectural challenges. Challenge 1: Proofs as native graph data. To persist verifiable claims, the DBMS requires a schema capable of expressing logical propositions. Eigenius uses EigenTT, a dependent type theory in the CIC family [9], as its native data definition language. EigenTT represents a verified claim as a dependent pair(푇,푡). The proposi- tion푇is expressed natively via EigenTT; graph ontology classes resolve directly as ground types by walking the layer chain. The witness푡, however, is not represented in EigenTT. Instead, the ver- batim Lean-4 proof bytes become an opaque blob associated with theVerifiedResource, cleanly separating the database’s schema from the prover’s artifact. Challenge 2: The in-process commit gate. The second challenge is validating this opaque witness푡without crippling throughput. Lean 4 acts strictly as an off-chain authoring environment. Calling out to an external orchestrator at commit would incur massive IPC overhead. Instead, Eigenius brings verification in-process. The Verdict(“Holds”) LeanProof Term patient_1 : Patient LeanProofPayload (export bytes) LeanPackageMirror bootstrap head layer verdict_subject claim_iri proof_payload mirror_iri source_layer mirrored_classes claim_iri and mirrored_classes converge on the same class: the cycle closes Figure 2: The closed audit chain: every edge is a content- addressed chain reference, and the cycle fromVerdictback to the ontology class is re-walkable and re-checkable from the graph alone. kernel’s type checker runs the exported proof bytes through a minimal Rust term checker,nanoda_lib[12,13], linked directly into the database binary. Sharing the binary shortens the audit path without merging trust surfaces: a panic in the term checker is confined to the verification fiber and cannot corrupt the core ontology. Successful reasoning traces persist as chain resources, doubling as a native memoization cache. Challenge 3: The binding problem. How does the database guar- antee that an abstract Lean 4 theorem applies to the specific data stored in the graph? The chain shapes carrying a claim include aLe anPackageMirror(the source-layer anchor and mirrored mappings), a LeanProofPayload (the verbatim bytes), and a LeanProofTerm. A commit-time query fires on everyLeanProofTermand performs a strict three-part check: (1) proof validity via the in-process term checker; (2) mirror correspondence, mapping eachEigeniusFFI.* constant in the proposition back to a chain class IRI (ensuring it references the schema); and (3) anchor consistency, hashing the mirror’s archive against the declared content hash. All three must pass to yield Verdict::Holds. The closed audit chain. This architecture closes the audit loop within the database (Figure 2). An auditor walks from aVerdictto the proof term, payload, and chain class, re-fetching every byte from the content-addressed store. They can re-run the in-process check with no contact to intermediate middleware. To mark a resource verified is not to ask the user to trust the database software, but to store the machine-checkable mathematics as a queryable chain resident. 6 Implementation and Evaluation Prototype and baseline flows. The Rust prototype includes RocksDB storage, a gRPC API, and a React notebook. An MCP server [23] exposes kernel ops to autonomous agents. Eight institu- tions run live across two extensibility paths: five Julia institutions on the runtime substrate, Lean 4 in-process, and the statistics and reasoning institutions. To demonstrate that the kernel supports both domains of scien- tific epistemology, the repository contains two baseline flows. The mathematical path is exercised by a Lean-verification flow whose 4 Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning EigenQL queries walk the closed audit chain from aVerdict::Hol dsback to the chain class. The empirical path is demonstrated by a kinase-screening flow that lifts 24 IC 50 measurements to typed reasoning through identity comorphisms across the Julia stack. Microbenchmark: Typed ingestion at scale. To evaluate the over- head of treating every record as a typed, commit-verified resource, we ingest the WordNet and UMLS lexicons. This data materializes as 9.19M chain resources at 361 bytes each (6.6M lexical entries, 4.8M surface forms). Import takes the standard commit path with no bulk-load bypass, sustaining roughly 5,200 validated resources/s on one core of a 22-CPU laptop. The commit gate is where the cost lies: structural class layers load at∼28k resources/s, while lexical entries, which rigorously type-check each sense against its category, load at∼4k resources/s. Macro-evaluation: Replicating a published study. The substrate’s flagship evaluation scales the empirical path to an end-to-end re- computation of a high-profile Nature study — Chan et al. [24] (WRN helicase in microsatellite-unstable cancers). We chose it as a stress test because its argument crosses multiple domains: genome-wide dependency screens, wet-lab validation, in vivo models, and a DNA- damage mechanism. From content-addressed, hash-pinned source data, two institu- tions compose over one layer chain. A statistics institution re-runs each statistic and commits a derived result with anIsDerivedAswit- ness. A reasoning institution reads those witnesses and discharges the study’s domain conclusions, each aReasoningSentencewhose certificate is a justification term type-checked against the asserted proposition. Every claim carries one of four warrant grades, making its epistemic status a queryable property of the chain rather than a prose caveat. On a clean database, 52 of 52 derived conclusions hold, discharging the study’s conclusions from pinned data. The value of this massive structural re-encoding is what it sur- faces: recomputation exposed four discrepancies between the pa- per’s prose and its own data, including a corrected sample size (푛=54→51, rows dropped as missing) and a pseudoreplication whose honest푝-value differs by thirteen orders of magnitude. These are recorded not as footnotes but as machine-checkable facts carry- ing both warrants side by side. Forcing every bridge to be a declared resource makes the surface of assumptions inspectable by an agent or human. Every analysis class in the paper runs live—from ali mma differential-dependency call over a 187 MB matrix to per-cell mechanism assays—and the few readouts that remain merely cited say so on the chain. Next step: the narrative itself. The replication formalizes the study’s steps and deviations; the prose argument connecting them stays off the chain. We are closing that gap with a dependently- typed categorial grammar engine that lands the narrative as typed chain-resident terms: prose is paraphrased into controlled English — one statement per sentence — then parsed compositionally, fol- lowing MTT-semantics [27] and the CCG-with-dependent-types lineage of lightblue [28]. The controlled-English stage provides a narrow target the model produces reliably and a categorial grammar parses deterministically. Because the terms land in the kernel’s own type theory, the argument — not just its steps — becomes a chain resident under the same institution checks as the data it describes. The engine is headed for registration as a further institution, and because full EigenTT serves as a cross-domain representation, the identity collapse above extends to prose: one more logic in the diagram, not a layer above it. 7 Discussion Related work. Eigenius synthesizes ideas across database and formal-methods traditions by pulling their mechanisms into the kernel. Versioning and federation: Versioned stores like Dolt [17] and TerminusDB [19] share immutable history, but reconcile untyped rows. Eigenius’s merges are strongly typed functorial migrations [6]. Polystore systems integrate heterogeneous storage, but rely on adapters rather than native comorphisms that reinsert results into the chain. Provenance and shapes: Provenance vocabularies [21] and graph shapes [22] (over RDF [14] and Atomic Data [15]) model audit relationships post hoc; Eigenius enforces stratification as a commit-time invariant. AI and orchestration: Hets [8] orchestrates institutions ephemerally. Finally, while neurosymbolic lifting [25] argues LLM outputs need compositional reconstruction, we argue this must land in a verifiable chain rather than trusting external sources. What we got wrong. The institution protocol was originally built around Wasm components, assuming strict sandboxing was the right boundary. While theoretically elegant, real-world reasoners (ODE solvers, biostatistics) wrap heavy native libraries that do not compile cleanly to Wasm. We abandoned Wasm for sibling contain- ers because supporting scientific ecosystems proved more impor- tant than lightweight sandboxing. Additionally, the kernel/orches- trator boundary remains in flux and represents ongoing technical debt. Open problems. The deepest open questions are theoretical. First, the interface between the type theory and the layer graph requires a formal account: proving that a typed merge over the layer lat- tice preserves well-typedness is our central foundational target. Second, the validator and comorphism type-checker are presently trusted; mechanizing them is the natural next step. Finally, beyond the Nature replication, the ultimate evaluation is closing the loop: proving that an AI Scientist operating strictly over our MCP end- points can soundly traverse, mutate, and verify a scientific graph without human intervention. Acknowledgments This work builds on the ideas behind the original Pharos research artifact, created at Microsoft Research’s Health Solutions Group; the authors thank Rick Sax, Andy McGregor, and the wider Pharos team for that foundation. References [1] A.L. Brown, Jr. Enforcing the scientific method. In Provenance and Annotation of Data and Processes, page 2. Springer, 2008. [2]Microsoft. Microsoft introduces groundbreaking technology for life sciences. Press release for Amalga Life Sciences 2009, Apr. 28, 2009. https://news.microsoft.com/source/2009/04/28/micr osof t- introduces- groundbreaking- technology- for- life- sciences/. [3]J.A. Goguen and R.M. Burstall. Institutions: Abstract model theory for specification and programming. JACM, 39(1):95–146, 1992. [4] R. Diaconescu. Institution-independent Model Theory. Springer, 2nd edition, 2025. [5] E.F. Codd. A relational model of data for large shared data banks. Commun. ACM, 13(6):377–387, 1970. [6] D.I. Spivak. Functorial data migration. Information and Computation, 217:31–51, 2012. 5 Will et al. [7]C. Bormann and P. Hoffman. Concise Binary Object Representation (CBOR). RFC 8949, Request for Comments, IETF, 2020. [8] T. Mossakowski, C. Maeder, and K. Lüttich. The heterogeneous tool set, Hets. In TACAS 2007, LNCS 4424, p. 519–522. Springer, 2007. [9] T. Coquand, Y. Kinoshita, B. Nordström, and M. Takeyama. A simple type-theoretic language: Mini-T. In From Semantics to Computer Science, p. 139–164. CUP, 2009. [10] A. Abel, T. Coquand, and P. Dybjer. Normalization by evaluation for Martin-Löf type theory with typed equality judgements. In LICS 2007, p. 3–12. IEEE, 2007. [11]L. de Moura and S. Ullrich. The Lean 4 theorem prover and programming language. In CADE-28, LNCS 12699, p. 625–635. Springer, 2021. [12] M. Carneiro. Lean4Lean: Verifying a typechecker for Lean, in Lean. arXiv:2403.14064, 2024. [13] C. Bailey. nanoda_lib: A Lean 4 term checker library in Rust. https://github.com/ammkrn/na noda_lib. [14] R. Cyganiak, D. Wood, and M. Lanthaler. RDF 1.1 concepts and abstract syntax. W3C Recom- mendation, 2014. [15] J. Meindertsma. Atomic Data. W3C Community Group Specification, 2020–2026. [16] R. Hickey. Datomic: A database deconstructed. InfoQ talk, 2012. [17] V. Sanca and T. Heyse. Dolt: SQL with Git-like versioning. DoltHub, 2019–2026. [18] S. Artemov. The logic of justification. The Review of Symbolic Logic, 1(4):477–513, 2008. [19] TerminusDB Team. TerminusDB: A delta-encoded graph database with revision control. https://terminusdb.com/, 2024. [20] C. Lattner and V. Adve. LLVM: A compilation framework for lifelong program analysis and transformation. In CGO 2004, p. 75–86. IEEE, 2004. [21] L. Moreau et al. PROV-DM: The PROV data model. W3C Recommendation, 2013. [22] H. Knublauch and D. Kontokostas. Shapes constraint language (SHACL). W3C Recommenda- tion, 2017. [23]Anthropic. Model Context Protocol. Open specification, 2024–2026. https://modelcontextprot ocol.io. [24]E.M. Chan, T. Shibue, J.M. McFarland, et al. WRN helicase is a synthetic lethal target in microsatellite unstable cancers. Nature, 568:551–556, 2019. https://doi.org/10.1038/s41586- 019- 1102- x. [25]R. Pareschi. From dependency to compositionality: A neurosymbolic lifting of LLM outputs via combinatory categorial grammar. arXiv:2607.18961, 2026. [26]A.L. Brown, Jr. Distributed decentralized clinical trial: Design to executable digital twin. PCT International Patent Application No.PCT/US2026/018207, filed Mar. 6, 2026. Patent pending; international publication forthcoming. [27] S. Chatzikyriakidis and Z. Luo. Formal Semantics in Modern Type Theories. Wiley-ISTE, 2020. [28] A. Tomita et al. Natural language inference with a CCG parser and automated theorem prover for DTS (lightblue/wani). In BriGap-2, p. 1–7, 2025. 6