-
-
Notifications
You must be signed in to change notification settings - Fork 0
docs(research): formal synthesis paper unifying substrate + e2e framework #52
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
Show all changes
6 commits
Select commit
Hold shift + click to select a range
9048a1b
docs(research): add formal synthesis paper unifying substrate + e2e f…
CodeWithJuber 203ebbd
docs(research): reconcile 14→15 citation count provenance
CodeWithJuber e4dc9ac
fix(pages): don't let an empty Unreleased section blank the status pa…
CodeWithJuber c293b90
fix(security): allowlist bibliography citation-key false positives in…
CodeWithJuber 156a086
docs(roadmap): bump Now marker to v0.12.1
CodeWithJuber b0d892b
Merge master into docs/formal-synthesis-paper
CodeWithJuber File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,15 @@ | ||
| title = "forgekit gitleaks config" | ||
|
|
||
| [extend] | ||
| useDefault = true | ||
|
|
||
| # generic-api-key false-positives: these are bibliography datasets where every entry has a | ||
| # "key" field holding a BibTeX-style citation key (e.g. "wang2023voyager", "ebbinghaus1885"). | ||
| # The literal field name "key" next to a quoted alphanumeric value trips the default | ||
| # generic-api-key rule even though there is no secret here — just citation metadata. | ||
| [allowlist] | ||
| description = "Bibliography citation-key fields, not secrets" | ||
| paths = [ | ||
| '''^research/formal-synthesis/graded_reference_set\.json$''', | ||
| '''^research/formal-synthesis/merged_references\.json$''', | ||
| ] |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,83 @@ | ||
| # Formal Synthesis — A Theory of the Cognitive Substrate for Coding Agents | ||
|
|
||
| This directory contains a formal, mathematical unification of three independently | ||
| developed bodies of work that all describe the **same architecture** for making a | ||
| frozen language model reliable at coding: | ||
|
|
||
| 1. **The Cognitive Substrate** — five faculties a frozen model structurally lacks | ||
| (memory, learning, imagination, self-correction, impact-awareness) and six | ||
| operating mechanisms M1–M6, with two runnable prototypes. | ||
| 2. **The End-to-End Agent Reliability Framework** (`FRAMEWORK.md`) — failure modes | ||
| F1 (partial work) and F2 (session amnesia), the change-closure fixpoint Δ*, | ||
| invariants I1–I4, algorithms A1–A7, and correctness theorems T1–T6. | ||
| 3. **forgekit / claude-e2e-kit** — the deployed implementation: committed-file | ||
| memory, deterministic lifecycle hooks, and auto-invoked skills. | ||
|
|
||
| The synthesis proves these are **one object in three vocabularies**. | ||
|
|
||
| ## The central result | ||
|
|
||
| > **Reliability = a probabilistic instruction layer × a deterministic interception | ||
| > layer. Neither layer alone suffices.** | ||
|
|
||
| Instructions (`CLAUDE.md`, rules, skills) *raise* the probability `p < 1` that the | ||
| model behaves correctly, but can never reach `p = 1` — so the residual silent-miss | ||
| rate over `n` tasks is `1 − pⁿ → 1`. A deterministic layer (hooks that execute | ||
| regardless of the model's choice) multiplies that residual down by a factor | ||
| `(1 − cⱼ)` per check — but cannot catch the *semantic* class (undecidable, by Rice's | ||
| theorem), so it needs the soft layer to shrink what reaches it. The paper states this | ||
| as **Theorem D** and proves it. It is the formal content of the practitioner's rule: | ||
| *never trust the output of a probability engine; earn trust with an external check.* | ||
|
|
||
| ## Three anchor identities (not analogies — the same mathematics) | ||
|
|
||
| | Substrate | Framework | Relationship | | ||
| |---|---|---| | ||
| | Impact-Oracle blast-radius | change-closure `Δ*` (least fixpoint of `X ↦ X ∪ N(X)`) | **identical** — reverse reachability, run to fixpoint ⇒ perfect recall | | ||
| | M2 assumption gate | amnesia equation `assumption ≈ argmax P(convention \| training)` | **identical** — the gate supplies missing context or halts, never guesses | | ||
| | substrate's two layers | design law "Π₃ probabilistic, Π₂ deterministic" | **identical** — Theorem D | | ||
|
|
||
| ## Contents | ||
|
|
||
| | File | What it is | | ||
| |---|---| | ||
| | `substrate_synthesis.pdf` | The formal synthesis paper (42 pp): definitions, Theorem D + proof, the unified A1–A7 TASK loop, invariants I1–I4, theorems T1–T6 with proofs, the 16-row crosswalk, the full 14-mapping Qur'anic epistemology, both prototypes with honest metrics. | | ||
| | `substrate_synthesis.html` | Same paper, self-contained HTML. | | ||
| | `crosswalk.json` / `crosswalk.md` | The three-way term-by-term correspondence (substrate ↔ framework ↔ forgekit), with the P1/P2/P3 → Π₁/Π₂/Π₃ notation reconciliation. | | ||
| | `graded_reference_set.json` / `.md` | The 15 new sources independently verified and graded (9 confirmed, 6 traceable, 0 unverifiable), including the disambiguation of the two future-dated arXiv IDs. | | ||
| | `merged_references.json` | Full 47-entry bibliography (32 original + 15 new, deduped). | | ||
| | `figures/schematic_duality.png` | The two-layer duality architecture. | | ||
| | `figures/schematic_taskloop.png` | The unified 7-stage TASK loop (each stage bound to faculty · algorithm · Qur'anic anchor). | | ||
|
|
||
| The **two runnable prototypes** referenced throughout the paper already live in this | ||
| repo and are not duplicated here: | ||
|
|
||
| - `../python-prototypes/impact_oracle/` — Prototype I, the impact oracle (A1 / Δ*). | ||
| Runnable, 36 tests. Perfect recall on impacted files. | ||
| - `../python-prototypes/router_gate/` — Prototype II, complexity-router + | ||
| assumption-gate (A7 + A6 / M1 + M2). Runnable, 19 tests. 62.1% real cost saved, | ||
| live-measured. | ||
|
|
||
| ## Honesty commitments (carried from the source work) | ||
|
|
||
| - **The prototypes are demonstrations, not benchmarks.** The router/gate's perfect | ||
| accuracy is on a 30-task hand-labelled set whose thresholds were tuned against it — | ||
| it shows the rubric *can separate* the cases. The cost figures, by contrast, are | ||
| exact arithmetic on **real measured token counts** from live model calls, and the | ||
| correctness sub-experiment actually executed the cheaper models' code against tests. | ||
| - **The impact oracle does not win on F1** (0.75 vs grep's 0.79). Its property is | ||
| **perfect recall** — the safety guarantee for "what will my edit break?". | ||
| - **Every future-dated / recent citation was verified by direct fetch, not inferred.** | ||
| Both 2026 arXiv IDs resolve to real preprints; one (`2601.05111`) is a *different* | ||
| paper from the founding Agent-as-a-Judge work (`2410.10934`), and both are recorded. | ||
| - **The Qur'anic lens is framing, never technical authority.** It supplies the | ||
| vocabulary of epistemic obligation — *lā taqfu*, *tabayyun*, *al-amāna* — that names | ||
| *why* each safeguard is mandatory; the engineering stands on its own merits. | ||
|
|
||
| ## Relationship to forgekit | ||
|
|
||
| `forgekit` is one binding of this theory (and `claude-e2e-kit` is its Claude-specific | ||
| reference realization). The paper's §11 gives the exact object-by-object mapping: | ||
| `Π₁` = the committed `docs/*.md` store, `Π₂` = the `session-context` / `docs-guard` / | ||
| `intent-router` hooks, `Π₃` = `CLAUDE.md` + `.claude/rules/`. The two prototypes here | ||
| are the mechanical cores of the `/impact` skill and the effort-router. | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,130 @@ | ||
| { | ||
| "meta": { | ||
| "title": "Three-way crosswalk: Cognitive Substrate theory <-> End-to-End Reliability Framework <-> forgekit / claude-e2e-kit", | ||
| "sources": { | ||
| "S": "Cognitive Substrate for Coding Agents (v2 whitepaper) \u2014 faculties F_i, mechanisms M1-M6", | ||
| "E": "End-to-End Agent Reliability Framework (FRAMEWORK.md) \u2014 F1/F2, I1-I4, A1-A7, T1-T6, Delta*", | ||
| "K": "forgekit / claude-e2e-kit implementation \u2014 hooks, skills, agents, committed files" | ||
| }, | ||
| "notation_reconciliation": { | ||
| "collision": "Both frameworks independently use the labels P1/P2/P3.", | ||
| "substrate_P": "In the substrate paper, P1/P2/P3 are PROPERTIES of the frozen model: P1 statelessness, P2 frozen weights, P3 bounded/undifferentiated context.", | ||
| "framework_P": "In the e2e framework, P1/P2/P3 are the three required PRIMITIVES: P1 persistent store, P2 lifecycle interception, P3 instruction channel.", | ||
| "resolution": "In the synthesis, the substrate model-properties keep P1/P2/P3; the framework primitives are RENAMED Pi1 (persistent store), Pi2 (lifecycle interception), Pi3 (instruction channel). Every use of the primitives in the synthesis is written Pi-n to remove the collision." | ||
| } | ||
| }, | ||
| "rows": [ | ||
| { | ||
| "concept": "The frozen core", | ||
| "substrate": "y = f_theta(x): stateless map, fixed weights, bounded context (properties P1,P2,P3)", | ||
| "framework": "the agent/model whose behavior instructions can only raise the PROBABILITY of (p<1)", | ||
| "forgekit": "Claude / Codex / Cursor / Gemini / Aider \u2014 the model the kit wraps, never modifies", | ||
| "relation": "identical object: all three treat the model as a fixed probabilistic map to be wrapped, not retrained" | ||
| }, | ||
| { | ||
| "concept": "Impact-awareness / partial-work failure", | ||
| "substrate": "Faculty: impact-awareness gap; the developer silently simulates 'what will this edit break'. Prototype I = Impact Oracle (reverse-dependency blast radius with confidence decay)", | ||
| "framework": "F1 partial work; dependents operator N(X); required change closure Delta* = least fixpoint of X |-> X \u222a N(X); Done predicate; Algorithm A1 IMPACT-CLOSURE", | ||
| "forgekit": "/impact skill; documentation-map.md (R_declared); grep identifier sweep (R_discovered)", | ||
| "relation": "IDENTICAL MATHEMATICS. The Impact Oracle computes N(X) by reverse reachability on the dependency graph; Delta* is exactly the oracle's transitive blast-radius set. The oracle adds a confidence-decay weight the framework's set-theoretic N(X) leaves boolean." | ||
| }, | ||
| { | ||
| "concept": "Memory / session-amnesia failure", | ||
| "substrate": "Faculty: persistent memory gap; each context window is ephemeral. Validity-anchored memory (facts carry confirmed/discredited state updated by verified outcomes)", | ||
| "framework": "F2 session amnesia; continuity invariant I2 (essential(K_i) \u2286 P and loader L must load it); handoff operator H; K_{i+1}(0)=L(P)", | ||
| "forgekit": "docs/STATE.md (bounded snapshot) + docs/DECISIONS.md (append-only log); /handoff writes it; SessionStart hook injects it", | ||
| "relation": "Same failure, same fix (external bounded-compression checkpoint). Substrate adds validity-anchoring (prune by whether a past prediction was externally confirmed); framework adds the snapshot+WAL split (STATE mutable vs DECISIONS append-only)." | ||
| }, | ||
| { | ||
| "concept": "Why assumptions happen (the root the user named)", | ||
| "substrate": "M2 assumption/uncertainty gate: under-specified input -> the model confabulates a convention", | ||
| "framework": "amnesia equation: when f \u2208 essential(K) is missing from L(P), assumption \u2248 argmax P(convention | training data) \u2014 the mathematically EXPECTED result of missing context, not misbehavior. Invariant I3 (no fabrication)", | ||
| "forgekit": "CLAUDE.md No-assumptions rule; intent-router SPEC card ('state assumptions explicitly')", | ||
| "relation": "The framework gives the substrate's M2 gate its formal justification: assumption is argmax over the prior, so the fix is to supply context (raise what L loads) OR gate on missing context (halt), never to hope." | ||
| }, | ||
| { | ||
| "concept": "Self-correction / verification", | ||
| "substrate": "M6 inline verification; Prototype-II verify step; self-correction faculty", | ||
| "framework": "Algorithm A6 COMPLETION-GATE (deterministic Stop-hook floor); Hoare postcondition Done(t); the verification operator in A3 (verified-unaffected requires an actual grep, not an assumption)", | ||
| "forgekit": "docs-guard.sh Stop hook (blocks finish if code changed but no doc/state artifact did); reviewer agent verdict", | ||
| "relation": "Same verify-gate. Substrate framed it as a mechanism; framework proves it terminates (T1) and is sound (T3) and makes it the deterministic layer of the duality." | ||
| }, | ||
| { | ||
| "concept": "Complexity routing", | ||
| "substrate": "M1 complexity-aware router (transparent additive rubric); Prototype-II router", | ||
| "framework": "Algorithm A7 KNOWLEDGE-ROUTER (where every fact lives, keeps always-loaded context bounded); System 1/System 2 effort routing; intent DFA", | ||
| "forgekit": "intent-router.sh (UserPromptSubmit hook, keyword DFA, <10ms, zero-token); effort-routing rule in CLAUDE.md; per-agent model: fields", | ||
| "relation": "Two facets of one routing principle. Substrate M1 routes by TASK COMPLEXITY -> model tier (cost). Framework A7 routes by KNOWLEDGE TYPE -> storage home (context budget). Both are transparent/deterministic, both reject an opaque-LLM classifier for the same reason." | ||
| }, | ||
| { | ||
| "concept": "Task decomposition", | ||
| "substrate": "M3 task/session decomposition", | ||
| "framework": "HTN closure -> ordered task list (A1 output is the worklist); the meta-algorithm TASK(t)", | ||
| "forgekit": "sdlc-pilot 7-phase skill; subagents; git worktrees", | ||
| "relation": "Same: decompose the goal into the closure's ordered worklist before building." | ||
| }, | ||
| { | ||
| "concept": "Goal-anchoring", | ||
| "substrate": "M4 goal-anchoring (goal drift: to a text model a long story and long code are the same object)", | ||
| "framework": "BDI Desires = written goal + acceptance criteria in STATE.md; I2 keeps them across sessions; acceptance criteria written at SPEC, consumed at VERIFY", | ||
| "forgekit": "docs/STATE.md 'Current goal' + 'Acceptance criteria'; sdlc-pilot SPEC->VERIFY gate", | ||
| "relation": "Substrate names the drift; framework anchors it in a persisted, re-injected Desire so every session optimizes the same target." | ||
| }, | ||
| { | ||
| "concept": "Anti-over-engineering", | ||
| "substrate": "M5 anti-over-engineering (scope minimality; the residual whitespace)", | ||
| "framework": "amana / scope-boundedness (agent may not exceed asked scope); I3 (no invented structure)", | ||
| "forgekit": "CLAUDE.md effort routing 'trivial -> do it directly, no ceremony'; least-privilege defaults", | ||
| "relation": "Weakest-covered in all three; substrate marks it residual-gap, framework encodes it as a stewardship bound, kit as an effort-routing default." | ||
| }, | ||
| { | ||
| "concept": "World-model of the codebase", | ||
| "substrate": "Faculty: world-model; Prototype-I codebase world-model (AST -> persistent dependency graph)", | ||
| "framework": "the typed artifact graph (A, tau, R = R_declared \u222a R_discovered)", | ||
| "forgekit": "documentation-map.md + the repo itself + ARCHITECTURE.md", | ||
| "relation": "Same graph. Substrate builds it from AST for code; framework generalizes the node type to {code,test,doc,config,diagram} so DOCS become first-class dependents \u2014 the key generalization that turns 'impact on code' into 'impact on all artifacts'." | ||
| }, | ||
| { | ||
| "concept": "Continual learning from outcomes", | ||
| "substrate": "Faculty: learning without touching theta (non-parametric always-on + parametric LoRA/EWC)", | ||
| "framework": "Reflexion loop made cross-session (I3/I4); DECISIONS.md as precedent DB; A4 mirrors durable lessons", | ||
| "forgekit": "Reflexion rule in CLAUDE.md; STATE gotchas; agents' memory: project", | ||
| "relation": "Same 'learn without retraining' stance. Both store verbal lessons externally and re-inject; substrate adds the parametric option, framework keeps it purely non-parametric (committed files)." | ||
| }, | ||
| { | ||
| "concept": "Rehydration (session start)", | ||
| "substrate": "closed-loop write-back/read-back band in the substrate architecture", | ||
| "framework": "Algorithm A5 CONTEXT-REHYDRATE; loader L; records git baseline for the gate", | ||
| "forgekit": "session-context.sh SessionStart hook; /catchup skill (deep variant)", | ||
| "relation": "The read side of the substrate's memory loop, made deterministic (inject, don't hope the agent reads)." | ||
| }, | ||
| { | ||
| "concept": "Independent verification / judge", | ||
| "substrate": "self-correction faculty; the honest-negative-result caution (models correct poorly alone)", | ||
| "framework": "LLM-as-Judge applied: reviewer agent (fresh context, explicit criteria, adversarial); self-consistency for critical changes (majority of N)", | ||
| "forgekit": "reviewer.md agent; DoD item 7", | ||
| "relation": "Substrate cited the finding that self-correction alone is weak; framework operationalizes the fix (an EXTERNAL judge), which is the same 'trust only an external check' principle as the gate." | ||
| }, | ||
| { | ||
| "concept": "The two-layer duality (THE central new insight)", | ||
| "substrate": "implicit: the substrate wraps a probabilistic core with deterministic external structure, but v2 never states it as a law", | ||
| "framework": "DESIGN LAW: instructions (Pi3) are PROBABILISTIC (raise p); interception (Pi2) is DETERMINISTIC (guarantee a floor c->1). P(silent miss) = (1-p)\u00b7prod_j(1-c_j). Since p<1 always, neither layer alone suffices.", | ||
| "forgekit": "the split itself: CLAUDE.md/rules/skills = soft layer; hooks (docs-guard, session-context, intent-router) = hard layer", | ||
| "relation": "THIS is what the kit gives the substrate theory: the reason the substrate must be TWO layers, stated as a theorem. The user's own discipline ('never trust AI output \u2014 it is calculated probability') is exactly (1-p)>0, which forces the deterministic layer." | ||
| }, | ||
| { | ||
| "concept": "The probabilistic failure model", | ||
| "substrate": "eval honesty: perfect accuracy shows separation not a benchmark; p<1", | ||
| "framework": "P(>=1 miss) = 1 - p^n over n tasks (0.9 -> 65% at 10, 96% at 30); layered: P(silent miss)=(1-p)\u00b7prod(1-c_j)", | ||
| "forgekit": "the lattice of gates: turn-level (hook) \u2282 commit-level (pre-commit) \u2282 PR-level (CI)", | ||
| "relation": "The math that makes 'it works sometimes then forgets' a geometric certainty rather than bad luck \u2014 and quantifies why each added deterministic gate multiplies down the residual." | ||
| }, | ||
| { | ||
| "concept": "Stewardship / governance boundary", | ||
| "substrate": "STEWARDSHIP/amana wrapper (33:72) around the whole architecture", | ||
| "framework": "amana in I3/I4 as no-fabrication + verified-currency; least privilege, reversibility, logged rationale, scope-boundedness", | ||
| "forgekit": "committed-files-only (auditable), block-at-most-once (no nagging), fail-open safety (T2), DOCS_GUARD_DISABLE auditable escape hatch", | ||
| "relation": "The ethical frame the substrate draws from the lens is realized as concrete safety properties in the framework (fail-open, reversibility) and kit (auditable hooks)." | ||
| } | ||
| ] | ||
| } |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This introduces
FRAMEWORK.mdas one of the three source bodies for the synthesis, but I checked the repository and there is noFRAMEWORK.mdor other non-research/formal-synthesissource for the named End-to-End Agent Reliability Framework. Readers cannot verify the crosswalk/theorem claims from the referenced document, so either add the file or replace this with the actual external/internal link.Useful? React with 👍 / 👎.