The Constellate Architecture

Version control for scientific state.

Will Blair

Abstract

Scientific work is now produced faster than science can absorb it. Models draft hypotheses, proofs, code, and analyses in minutes; the systems that decide what survives scrutiny, what failed, and what to act on next were built for a slower world. The scarce thing is no longer a producer of candidate results. It is a shared record that can move a candidate into accepted, reusable, correction-aware state.

Vela is that record: version control for scientific state, with a gate on what counts as verified. It compiles research activity into a signed, content-addressed, replayable frontier, tracking the change to what a field holds, not the document that triggered it. Agents and humans propose; frozen verifiers reproduce; a human key accepts; the frontier remembers.

This is not a proposal. The first proof shipped in the domain where verification is cheapest and most honest: mathematics. Improved Sidon-set bounds were adopted upstream into OEIS A309370; an Erdős-problem frontier reproduces every banked witness from a clean clone; a prover-in-the-loop foundry closed sorry-carrying formalization obligations with kernel-clean Lean proofs. The substrate is public at github.com/constellate-science/vela (v0.720, dual Apache-2.0 / MIT).

This document specifies the architecture: the state-transition primitive, the trust gate, git-native frontiers, the shipped wedge, the vocabulary, governance, and the path outward. The bit-level protocol specification lives next to the code, in docs/PROTOCOL.md, where it stays in sync with the reference implementation. The worldview, why this matters for disease and for physical scientific capacity, lives in the three essays this paper accompanies.

1. The Problem

A field advances by generating variation and then doing the slower work that follows: selecting what survives, retaining what failed so the next group does not repeat it, and carrying corrections back to the claims they overturn. AI has made the first half cheap and left the second half where it was.

Candidates are abundant now. What stays scarce is the step that moves one of them into accepted state the next decision can read. A paper records that an author claimed something. It does not tell the next system what changed, what depends on the claim, or what should be tested next. So a clinician reconstructs the field by hand, an agent recompiles the same scattered prose into a context window that closes when the conversation ends, and a correction travels by rumor to one lab while the work that depended on the original goes on unchanged.

The groups closest to the frontier of automated mathematics have reached the same diagnosis from the production side: the binding constraint is no longer generating proofs but integrating, verifying, and maintaining the ones already produced. The missing layer is the one that carries forward what survives.

2. The State Transition

The primitive is the scientific state transition: a reviewed change to what a field currently believes or can act on, with the evidence, scope, provenance, confidence movement, and downstream effects attached. Papers, datasets, and model outputs are artifacts around it.

A transition is small enough for an ordinary scientist to read and structured enough for another system to act on. The carriers are typed objects:

  • Finding (vf_*): the primary state object. An assertion with its evidence, conditions, confidence, and provenance.
  • Evidence atom (vea_*): an exact, source-grounded unit bearing on a finding.
  • Condition: the scope boundary, where a claim holds and where it stops.
  • Artifact (va_*): a content-addressed dataset, notebook, protocol, witness, or model output.
  • Proposal (vpr_*) and Scientific Diff Pack (vsd_*): the reviewable bundle of proposed changes.
  • Signed canonical event (vev_*): the authoritative state-transition record.

The discipline that makes this work is one sentence: activity is not state. A script that ran, a paper drafted, an agent trace, a benchmark report, are source material. Each becomes state only when it is converted into a proposed change, reviewed against a frontier, attested under governance, and recorded as a signed event that deterministic replay can reconstruct. Answer pages, graphs, and dashboards are projections over replayed state, not separate stores of truth.

3. The Trust Gate

A signed log is not a verified claim. Vela separates the two, and the separation is the protocol’s spine.

The log can be trustworthy by construction: content-addressed, signed, append-only, replayable. A claim becomes verified only by passing a gate. The gate status is a pure function of the verifier attachments on a finding, with no setter; it cannot be asserted, only derived. Where a claim is machine-checkable, the record ships a frozen exact verifier alongside it, and the next reader re-runs it from scratch to the same answer on any machine, with no model and no reviewer judgment in the path. The same verifier that admits a valid witness rejects an invalid certificate and a confident but false claim, and the rejection is the part that matters.

Verification answers one question, not four. A check can confirm that a proof runs, a bound holds, a synthesis completes. It cannot confirm that the statement checked is the one the field meant to ask, that the evidence behind it is enough to act on, or that an authority competent in the area accepts it. Those are four assurances, and only the first is mechanical. The transition carries all four as separate, inspectable layers: the verifier result, a human attestation that a formal statement faithfully encodes the informal claim (vsa_*), the evidence standing behind it, and the named authority that accepted it.

This statement-fidelity layer is load-bearing and easy to miss. A Lean theorem can type-check, be sorry-free, and pass an axiom audit, and still prove a statement that differs from the intended problem, or rest on an undischarged hypothesis passed as a theorem parameter. Axiom-clean is not the same as unconditional. The kernel certifies the derivation; a person stakes their name on the match between what was proved and what was meant. No AI sits in the trust path. Models produce candidates; only frozen verifiers and human keys move state.

4. Git-Native Frontiers

A frontier is a bounded, reviewable state object over a scientific question. As of v0.720, a frontier is a git repository, not a parallel one.

The working rule is build authority, borrow logistics. Git stores and transports. GitHub coordinates review and CI. Vela defines, verifies, and replays scientific state, and nothing else. A frontier lives as a directory with its .vela/events log committed; contributors fork, add or edit a witness, and open a pull request; a vela-check action re-derives the frontier from a clean checkout on every PR, runs vela reproduce over the frozen verifiers, runs structural checks, and verifies hash parity against the committed lock so the working tree is the signed state. Acceptance is a signed review event in the PR, under human key custody.

The hub is an index, not an authority. It offers cross-frontier search, reverse-dependency lookup, and projection APIs over git-replayed state; it can withhold or reorder, but it cannot fabricate or tamper without breaking signatures and hashes. The authoritative source is the committed event log, reproducible from a clean clone. Everything a site or dashboard shows is a stateless projection over that.

5. The Shipped Wedge

The architecture is not hypothetical where the gate is machine-checkable. The first frontiers are mathematical because that is where verification is cheap, exact, and reproducible, and where overclaiming is hardest to hide.

  • Sidon sets, OEIS A309370. Improved lower bounds were adopted upstream into the sequence (approved comments across n = 8 to 24), and a second sequence, A321531, lists exact new terms credited as extensions. This is external adoption, not a private demo: the published bounds are checked by anyone who reads the page, and every banked witness re-verifies under vela reproduce against the frozen vela-verify Sidon checker.
  • The Erdős frontier. Over a thousand problem records, with a witness-and-certificate corpus that reproduces from a clean clone, and a weekly watcher that ingests new upstream state.
  • The prover-lane. A prover-in-the-loop Lean foundry closed several sorry-carrying Erdős formalization obligations with kernel-clean proofs, the Lean kernel its only verifier. These are tractable formalization gaps, not solved open problems; some were known results or ported proofs, and the headline research-open problems stay open. The honest framing is the point: the value is the loop closing end to end under a verifier, not a breakthrough count.
  • The frozen verifier registry. vela-verify ships deterministic exact verifiers spanning Sidon, Golomb, cap sets, B_h sets, covering designs, constant-weight and linear codes, and Costas arrays. One judgment-and-obligation primitive works across all of them without a new protocol per domain.

What is true here matters as much as what is not. There is no external steward operating the record yet; the maintainer signs acceptances. There is no non-maintainer second producer who has consumed a root, written an update, and consumed the next root; that remains the decisive open adoption test. The reducer exists in Rust, with Python and a TypeScript cross-implementation harness that proves the mutation rules are protocol rather than a Rust artifact, not a published library. The wedge is math; empirical loops need richer state than formal ones.

6. Vocabulary and Ecosystem

The names are nested and worth stating precisely, because earlier working names are dead.

  • Constellate is the ecosystem: the open infrastructure for cumulative science, the umbrella brand.
  • Vela is the protocol and reference implementation, the signed-state layer.
  • Carina is the kernel of primitive types beneath the protocol.
  • Inside a running system the nesting is Constellation ⊃ Atlas ⊃ Frontier ⊃ Finding: a finding is the primary record, a frontier a bounded state object over a question, an atlas the composed graph of findings, the constellation the ecosystem-level view.
  • Canopus is the intended neutral steward, a stakeholder-governed nonprofit committed to open-infrastructure principles: services not access-gating, forkable content-addressed history, no single producer holding the pen. It is designed and documented, not yet operating independently.

The older working names, including the kernel name “Keel” and the “Lux” and “Horizons” project names, are retired and should not reappear.

7. Governance and Capture

When intelligence is abundant, the scarce resource is trust: state a next decision can act on without rebuilding it by hand. Votes, stars, and agent output are signals. Trust enters when someone recognized for a domain, under a revocable credential, signs a transition under rules other institutions can inspect, contest, and inherit.

The engine records authority; it does not invent it. It captures the judgment of whoever is competent to decide, with scope and conditions attached, rather than ruling from above that a proof is canonical or a target validated. And no single root holds the answer: the same claim can be kernel-verified and not yet in a standard library, published and disputed, accepted inside one company and unrecognized by the registry a regulator reads. Each of those is a different authority applying a different standard. The protocol keeps one shared way to record a transition and lets each authority maintain its own root over it.

This makes governance a design requirement, not an afterthought. The capture point sits above the nominally open layer: a protocol can be open while the canonical registry of signers, reviewer reputation, and credential recognition is closed. Open code with a closed registry is captured infrastructure with a permissive license file. The defenses are structural: more than one implementation of the protocol, a registry that can be forked when its charter fails, signer recognition no single company controls, and review authority that can be revoked and audited.

8. The Adoption Path

The order of construction matters more than any single layer. Protocol first, then implementation, then ecosystem, then product; the reverse order codifies one implementation’s choices as the standard. The wedge expands by verification cost, not by ambition.

It starts where claims compile: formal mathematics, exact combinatorics, certificate-checkable search, benchmark replay. It moves outward to computational reproducibility (code and data hashes, environment locks, independent reanalysis), then to empirical domains as receipts, protocols, and governance mature. Where the standard is a wet lab and a year, the record still fills, but reality sets the pace, and a claim with no in-software verifier has no permissionless admission path; it requires review and named authority. The architecture does not launder weak evidence through strong language. A messy biological claim can be useful, citable, and reviewable without being “verified” in the exact-verifier sense, and the status ladder keeps those distinct.

9. Status and Open Problems

The substrate is public and shipping. v0.720 consolidated the kernel, made the event-log hash content-only so signing is orthogonal to content addressing, retired the finding-signature lane in favor of the signed event log as sole authority, demoted the hub to a read-only index, and moved frontiers to the git-native model. The trust gate, frozen verifiers, deterministic replay, the proposal-review-accept pipeline, and Lean verification records all run under a conformance gate that must stay green on every change.

The honest gaps are the roadmap:

  • No second producer. External adoption is proven only when an independent producer consumes a root, writes an accepted update, and the next producer consumes the new root. That number is still zero.
  • No external steward. Canopus is designed; the record is not yet operated by a neutral party.
  • Empirical state is harder. Formal frontiers close under cheap verifiers. Disease corridors need uncertainty, protocol versions, sample identity, calibration, and replication status, and the rate-limiting step stays at contact with reality.
  • Reducer breadth. Rust is reference-grade; the other implementations are partial or verification-only.

The bit-level specification, the canonicalization rules, the reducer mutation kinds, and the conformance criteria are maintained next to the code in docs/PROTOCOL.md, with the theory in docs/THEORY.md. They are the normative reference; this paper is the architecture, not the byte layout, so the two cannot drift.

10. How to Participate

The protocol, kernel, verifier registry, and tooling are open at github.com/constellate-science/vela under dual Apache-2.0 / MIT licensing. The fastest path to the protocol becoming canonical is independent reducers agreeing on byte-identical state, and independent producers writing into a frontier they do not own.

A contributor forks a frontier, adds or edits a witness, and opens a pull request; the gate runs vela reproduce and vela check from a clean checkout and verifies hash parity; a maintainer reviews and a human key signs the accepting event. Same input, same answer, any machine. That is the entire trust story, and it is the on-ramp.

Appendix. References and Lineage

The architecture stands on a few precedents and is sharpened against a few near-misses.

What it learns from. Git gave code a memory and made AI-scale software possible because the work already lives in objects an agent can inherit, test, merge, and distribute. The Protein Data Bank made AlphaFold possible by keeping experimentally determined structures shared, curated, and machine-readable; a model is bounded by the corpus it can learn from, and most fields keep no machine-readable record of their current state. Crossref, the IETF, and the W3C are the partial governance precedents for nonprofit infrastructure maintained across competing institutions.

Why it is not the previous attempts. Version control, data repositories, preprint servers, and the standards lineage that tried to wire them together (FAIR, nanopublications, the Open Research Knowledge Graph, the GitHub-of-science proposals) move artifacts well. A field can adopt every one of them and still have nowhere that the state of a claim changes when a result comes in. Those efforts also asked scientists for work on top of publishing, to annotate and structure and deposit, which is the wrong side of the ledger: a record gets written only when writing to it is the cheaper path, the way a commit is cheaper than mailing a patch around. The missing layer sits a level below the library, where state changes, and it has to be the easiest place to put a result rather than another chore after the paper is out.