Synapse: provable non-corruption

Provable, not estimated.

For evaluators and adopters: this is the long-form argument behind one line in the README: that Synapse can prove specific non-corruption properties of an AI’s memory, offline, from your own git, rather than estimate them with a benchmark. It cites the command (syn verify) and the decisions (ADR-035/036/037) that make the claim true, and it states: plainly, > where the proof stops. The honesty is the point: a tool that says “tamper-evident, not tamper-proof” is worth more than one that hand-waves “cryptographically secure.”

Current implementation boundary (2026-10-12)

At 3ceddd0, verification covers the documented deterministic projection, not universal knowledge correctness. INV-5 validates declared supersession closure; it does not detect every unrecorded historical edit. INV-13 checks overlapping intervals, cycles and inverted intervals, not general prose contradiction. INV-8 is Skip because receipts are export-on-demand; a basic report permits skipped checks and can be unsigned if no key is available. ADR-034 reports commit signature presence; cryptographic commit/allowlist verification remains SYN-261.

The trust ladder below describes architectural assurance goals; L4 is not fully enforced in the current build. ADR-051, ADR-052 and ADR-053 record the extension path, with implementation issues. These designs do not add runtime guarantees by themselves.

1. The problem: AI memory drifts silently

An assistant with long-term memory accumulates facts. Over a long enough horizon, some of those facts get silently overwritten, contradicted, or mangled, and the failure is invisible, because the memory keeps answering confidently. The field’s published answer to this is better auto-correction plus judge-scored benchmarks: run a suite, have an LLM grade whether the memory stayed coherent, report a percentage. (HaluMem, for instance, measured auto-update correctness below 26%.)

A judge score is an estimate. It tells you, probabilistically, that memory tended to stay correct on a sample. It cannot hand you a specific, checkable guarantee about your workspace right now, it depends on a model’s judgement, and it cannot be reproduced bit-for-bit by a skeptical third party.

2. The thesis: prove three integrity classes, offline, per-fact

Every integrity system in the literature proves one of three things:

(A) Content integrity: this artifact is the one that was attested (a hash or signature over the bytes).
(B) History integrity: the append-only log was not reordered, truncated, or rewritten (a consistency proof).
(C) Derived-state integrity: the output was reproducibly derived from the input (a deterministic rebuild).

Synapse is structurally positioned to prove all three at once, offline, per fact: because the truth is your Markdown in your git, and the SQLite index is a pure function of it. That last property is the whole game: the index is a reproducible build of your files. Delete it, rebuild it, and you must get the same logical state back; if you don’t, something is wrong and the tool can say exactly which fact diverged.

This user-held source makes independent rebuild checks practical. A hosted or self-hosted system can adopt equivalent evidence mechanisms using exported sources, snapshots, authenticated logs and deterministic projections; Markdown is a useful implementation choice, not an exclusive prerequisite.

3. The mechanism: `syn verify`

syn verify assembles primitives Synapse already ships (audit verify + reindex + at/--as-of) and reframes them as proofs, each contributing one line to a signed, reproducible report. The same core::verify::run backs both doors: the CLI command and the MCP verify tool (docs/COMMANDS.md, docs/MCP.md).

The canonical dump (ADR-035). A raw .db is not byte-deterministic: rowids, FTS internals, and float vectors vary run to run. So verify never hashes the database file. It computes a canonical logical manifest: ordered rows, with the non-reproducible surface (FTS, pending queue, reindex ledger, vectors, mentions:* enrichment) excluded or pinned to model@precision. That manifest is byte-stable across calls and across a reindex --full: that stability is the foundation everything else stands on.

The invariants checked on a default run:

Invariant	Class	What it proves
INV-1 reindex fixpoint	(C)	`digest(reindex(markdown)) == digest(live index)` over the canonical dump, the index is a reproducible build of your files. The keystone.
INV-2 content integrity	(A)	every fact’s recorded `payload_sha256` matches its Markdown; no orphan facts, no orphan audit rows.
INV-3 history integrity	(B)	the audit hash-chain + signed checkpoint are intact (Tier-2), or the git DAG + per-author monotonic segments are (Tier-1).
INV-5 supersession closure	(A/B)	declared successors have closed predecessors; changes without declared supersession are outside this check.
INV-8 receipts	(A)	currently skipped: there is no stored-receipt set to verify.

Opt-in deepenings:

--deep adds INV-4 (replay determinism): replaying the accepted-decision journal in a scratch index is deterministic. (See §5 on why this is framed as determinism, not store reconstruction: that distinction is deliberate and honest.) It also adds INV-13 (logical coherence, SYN-316): a deterministic, model-free sweep for contradictory facts (overlapping valid-time values for one field, supersession cycles, inverted intervals). This is the one check that catches a corruption introduced by a direct Markdown edit that bypasses the gate: INV-1 proves the index is a faithful build of the Markdown, but if the Markdown itself was hand-edited into a contradiction, only INV-13 sees it.
--rebuild makes INV-1 diffoscope-style: on a mismatch it doesn’t just say “diverged,” it names every diverging fact. “Your memory is a reproducible build of your files, and if it isn’t, here is exactly which fact broke.”
--since <witness> adds INV-12 (offline consistency): it proves your audit history is an append-only extension of a previously published witness, using git ancestry + segment-prefix stability, with no remote and no network (ADR-037).

The proof artifact. A signed synapse.verify-report/1, shaped like an in-toto Statement: {subject:{workspace, git_ref, inputs_hash}, predicate:{tool_version, invariants:[{id,status,evidence}], checkpoint, witness_status, ts}, sig, pubkey}. When an identity key is available, it is signed with the existing ed25519 identity (reusing the SYN-247 receipt path); otherwise signature/public_key remain absent. It is reproducible: anyone with your repo at git_ref re-runs syn verify and gets a bit-identical inputs_hash and the same verdicts.

Two further integrity properties (port parity (CLI ≡ MCP for every read) and temporal correctness (at <ref> -- search --as-of reconstructs the state that held)) are proven by the differential and property-based test suites (SYN-264/265), not as lines in the per-workspace report. They are invariants of the build, checked in CI, rather than of your workspace at verify time.

4. The ladder: L1 → L4

A workspace earns a higher rung as its trust root strengthens. The ladder is framing for “how strong is this proof,” borrowed in spirit from SLSA; it is not a network service:

L1: Audited. Append-only audit trail exists; decisions are recorded.
L2: Hash-chained. The trail is self-chained and an ed25519 checkpoint is signed; local tampering is evident.
L3: Git-witnessed. The workspace is versioned; integrity rides git’s Merkle DAG and a published witness can catch a history rewrite (--since).
L4: Signed-identity (target). Genuine signature validation against known, non-revoked identities would attest authorship (ADR-030). ADR-034 only ships posture; SYN-261 and ADR-053 track enforcement.

5. The honest ceiling

A proof you can trust is a proof that states its own limits. Synapse’s are written into the ADRs, not buried:

Tamper-evident, not tamper-proof (ADR-037). A lone local clone cannot detect its own owner’s rewrite: there is no witness to contradict a history that was rewritten and re-signed end to end. syn verify therefore prints its trust root: local-only, checkpoint-witnessed, or remote/published-witness. A tracked remote, or a published syn audit witness, is what lets a third party hold the owner to their history. This is exactly where competitors say “cryptographically secure” and stop; Synapse says where the evidence ends.
Replay is determinism, not store reconstruction (ADR-036). It is tempting to claim “replay the audit log and you get the store back.” For a state-based, hand-editable Markdown store with a hash-only log and a wall-clock, that reconstruction is unsound, and ADR-036 says so explicitly. So INV-4 proves the weaker, true thing: replay is deterministic (pinned via a clock seam), and reconstruction of state is the job of INV-1/INV-7 (rebuild from the files), not of replay. verify --deep is a bounded journal-integrity check, not a store-from-log rebuild. Stating this is what keeps the keystone claim (INV-1) credible.
Canonicalisation is the one real prerequisite. Because the database isn’t byte-deterministic, the entire argument rests on the canonical logical manifest (ADR-035) being stable and complete. That is a property to keep tested, not assume.
Current local baseline. No mandatory Rekor/Fulcio, OIDC or Trillian witness-net, no runtime model-checker, no RDF/OWL, no IPFS/CID. Synapse adopts the proofs from that literature (Merkle DAG, consistency proofs, reproducible-build comparison, in-toto attestation shape) and runs them over git and ed25519 it already has: offline, dependency-light, deterministic over ML.

6. Interoperability and evidence

User-held content, explicit acceptance history and rebuild checks are useful in both standalone and embedded use. Other systems may expose snapshots or authenticated event logs through a provider adapter. Describe the evidence each provider supplies instead of assuming that a hosted system cannot produce it. Synapse complements existing knowledge/retrieval tools.

The assurance boundary is what the report actually checks, from which trusted baseline, with which signer/authority/witness evidence. Proposed transition journals, stored receipts and strict profiles improve that boundary; probabilistic prose diagnostics remain separate.

Synapse: Operational memory for agents