WhyLog — a truth-maintenance system for the decisions you made with an AI
DevPost "About the project" submission. Markdown with LaTeX. Copy the body below the line.
Inspiration
Every tool in this space remembers what you decided. None of them remembers what had to be true for that decision to be right.
"SQLite, not Postgres" is not a fact. It is a belief held under assumptions:
$$\text{SQLite} \succ \text{Postgres} \;\mid\; {\text{single user},\ \text{no deploy infra},\ \text{no concurrent writers}}$$
The moment you add a second writer, the decision does not become disliked — it becomes false, and nothing in your repo, your ADR folder, or your agent's context window will tell you so. Your agent will keep happily building on it, because the decision still reads like a decision.
That asymmetry is the whole idea:
Contradiction detection fires when you contradict yourself. Premise invalidation fires when reality does.
The second one is the expensive failure, and it is the one no coding agent can catch on its own — it has no memory of the assumption, only of the conclusion.
We read the literature and found the pieces existed but had never been assembled for this workflow. Doyle's 1979 Truth Maintenance System and de Kleer's 1986 ATMS give the formal machinery. Zep/Graphiti gives bi-temporal knowledge graphs. Kantara (arXiv:2506.11005) mines rationale from kernel commits and finds 396 contradictory pairs. veritas-tms implements JTMS contraction. RecovAr recovers design rationales at 75% recall / 77% precision. ARGUS recovers alternatives at 15.4% precision with a 13:1 false-positive-to-false-negative ratio — which told us the hardest problem here is not finding things, it is not crying wolf.
And one number convinced us the payoff is real: across 15 feature requests in 10 open-source repos, agent-optimised ADRs cut wrong turns by ~90% (191 → 20), with 37% fewer tokens and 22% less time. Anthropic's own guidance warns that "if two rules contradict each other, the model may pick one arbitrarily."
Nobody was storing the given. So we built the thing that does.
What it does
Paste an AI-agent transcript — Cursor, Claude Code, Copilot, ChatGPT, messy or clean. WhyLog:
- Extracts decisions, their premises, and the alternatives you rejected — with verbatim character spans back into the raw transcript, never a paraphrase.
- Builds a premise lattice: decisions and premises are separate node types, so one premise shared by four decisions is one node with four edges. Invalidate it once, and all four are re-examined.
- Runs three gates. (a) structural — same variable, different canonical value, overlapping validity window. (b) semantic — near-duplicates whose rationales conflict. (c) premise — the one nobody else has: a decision goes UNSOUND because an assumption stopped holding, not because you changed your mind.
- Cascades with backtracking, ordered by entrenchment — retract the cheapest belief first, and refuse a newcomer that cannot outrank every incumbent it contradicts (Hansson screening).
- Answers "why" questions under an evidence contract: at most three searches, every citation must resolve within the run, and "insufficient evidence" is a first-class answer rather than an apology.
- Synthesises executable guards from each decision — the check that would falsify it — and exports a standalone runner plus a GitHub Actions workflow. The literature on ADR fitness functions is entirely manual authoring; nobody generates the check from the decision.
- Exports for agents, not just humans:
DECISIONS.md,CLAUDE.md,.cursorrules,AGENTS.md— scoped, imperative, verifiable, non-conflicting, under 200 lines.
No API key required for any of it. Extraction, invalidation, cascade, entrenchment, guards and export all run offline and deterministically through a local engine. The LLM path is a second implementation of one interface, not a dependency.
The formal core is a knowledge base $K = \langle D, P, J, L, N \rangle$ — decisions, premises, justifications, labels, nogoods — with Doyle's SL validity condition:
$$\text{valid}(j) \iff \bigwedge_{p \in \text{IN}(j)} L(p) = \textbf{IN} \;\wedge\; \bigwedge_{q \in \text{OUT}(j)} L(q) \neq \textbf{IN}$$
A non-empty OUT-list is what makes the system non-monotonic, and it is gate (c). That single clause is the difference between a decision log and a belief-revision system.
Entrenchment decides which belief to give up:
$$E(d) = 0.30\,a_{\text{source}} + 0.20\,c_{\text{impl}} + 0.20\,k_{\text{corrob}} + 0.15\,\sigma_{\text{conf}} + 0.15\,\rho_{\text{recency}}$$
capped by the weakest premise it rests on — $E_3(d) = \min_{p \in P(d)} E(p)$ — because a decision cannot be more secure than the assumption underneath it.
Retrieval fuses five index levels with Reciprocal Rank Fusion ($k=60$):
$$\text{score}(d) = \sum_{r \in \text{levels}} \frac{1}{k + \text{rank}_r(d)}$$
L1 dense statement embeddings · L2 index-time hypothetical questions (HyPE) · L3 BM25 sparse · L4 structural · L5 premise inverted index — then reranks against the original query only, at weights structural .35 / lexical .30 / dense .20 / premise .10 / recency .05. No vector database: cosine over Float32Array in localStorage.
How we built it
Append-only, bi-temporal, and paranoid about provenance.
Every mutation is append → fold → persist. Nothing is ever deleted (invariant I1); a correction is a new event, and the timeline can be replayed as-of any learned time. Each event carries two clocks — valid time (when it became true in the world) and learned time (when WhyLog found out) — because you paste a three-week-old transcript and a single-timestamp model orders that graph wrongly. Events are sealed into a SHA-256 hash chain; the CI exporter refuses to emit a runner from a broken chain.
Four invariants shaped every module:
- I1 — nothing is deleted
- I2 — premises are shared nodes, so the graph is bipartite, never decision→decision
- I3 — retrieval proposes, a classifier disposes
- I4 — the system proposes, the human disposes
We built DecisionMemEval, a 13-metric benchmark, before we tuned anything: 12 hand-labelled transcripts (5 clean, 4 messy, 3 adversarial), 50 ground-truth labels each resolved to a verifiable character span, 7 planted interventions, 8 questions of which 2 are deliberately unanswerable. Matching requires span overlap and variable agreement. Six of the thirteen metrics have no published comparator — premise extraction, L2 invalidation, cascade correctness, survivor preservation, MRR, modality precision. That is the new-territory claim, stated as a count rather than an adjective.
An ablation harness declares its thresholds before running: 11 toggles plus 2 parameter sweeps, each with a pre-committed expected damage.
And npm run readiness — one command that answers "are we done?" in three separate parts, because a single exit code cannot:
build-ready YES 8/8 hard gates
demo-ready YES 8 beats verified, 3 dry runs identical
benchmark-defensible NO 8 known gaps open, each with its closing condition
274 source files · ~80,000 lines · 172 tests · tsc at 0 errors under a fully strict config including exactOptionalPropertyTypes and noUncheckedIndexedAccess.
Challenges we ran into
The interesting ones were never type errors. They were code that compiled, ran, threw nothing, and produced nothing.
1. The graph had zero IN nodes. We instrumented the benchmark and found:
decisions 34 → IN 0, OUT 27, UNKNOWN 7
premises 98 → IN 0, OUT 21, UNKNOWN 77
The harness never emitted PremiseConfirmed. A premise is UNKNOWN until a human confirms it; a justification is valid only when every IN-list node is IN; so with every premise UNKNOWN, every decision was OUT. Half our metrics weren't low — they were structurally zero. The "26 unexplained retractions" in our false-positive metric were every decision in the corpus. Our own test helper had written the rule we broke: "fixtures that test gate (c) must start from a REVIEWED graph."
2. Eight of eleven ablation toggles were declared and never read. The first ablation returned exactly +0.000 for every switch on every metric. Fifteen configurations cannot produce bit-identical scores unless the switches do nothing. A declared switch is not an implemented one. We wired all eight at the module that owns the behaviour, and kept the not-wired verdict permanently — it is the check that catches the next one.
3. Our own audit had an inverted sign. delta = ablated − baseline, so removing a load-bearing component gives a negative delta — but confirmed tested delta >= threshold, which is the case where removing it made things better. A component that improved the system by being deleted would have been reported as confirmed. It never fired only because no delta reached either threshold.
4. A vacuous pass in our headline metric. With gate (c) finally wired, the ablation reported that removing premise invalidation improved L2 recall to 1.000. Not a finding: with no intervention planted, the watched decision was already OUT for unrelated reasons, and a standing breakage was being counted as a detection. A metric that can score perfectly when the mechanism was never switched on is not measuring the mechanism. We now require that an intervention actually happened, and report untestable when it didn't.
5. Gate (a) was crying wolf — and the fix was not a threshold. With a live graph the false-positive rate was 138.2 per 100 decisions, 43 of them contradiction records. Gate (a) fired freely on decisions with status proposed: two unreviewed machine guesses disagreeing, presented to the user as a conflict about their project. Requiring one accepted side took it to 11.8 per 100 with contradiction precision 1.000. That broke our demo's best beat — correctly, because a decision nobody accepted cannot be reversed — so approval became part of the harness's review step.
6. Refusal cannot be tuned into existence. We measured the two unanswerable questions against the six answerable ones. They retrieve at 0.348 and 0.346; two answerable ones retrieve at 0.348 and 0.350. The distributions overlap. No threshold separates them. We added a structural refusal instead (the question resolved to a variable and nothing retrieved occupies it) — and it doesn't fire either, because spurious nodes occupy all fifteen variables. Refusal, over-firing and weak retrieval are the same problem: extraction precision.
7. A linter that broke the build while the tests stayed green. biome check --write --unsafe took lint errors 53 → 9 and tsc 0 → 31 in the same run, by stripping every non-null assertion that noUncheckedIndexedAccess requires. All 172 tests passed throughout.
8. Our corpus is set in the future. Learned time is monotonic; the transcripts are dated into November while the build ran in October, so stamping events with nowISO() put them before the log's last event and the substrate rejected the batch.
Accomplishments that we're proud of
- False-positive rate 11.8 per 100 decisions with contradiction precision 1.000 — against ARGUS's published 15.4% alternative precision and 13:1 FP:FN ratio. This is the metric that decides whether anybody keeps the tool installed, and it is the one we most nearly shipped at 138.2.
- The demo's peak beat is real, not scripted. Beat 5: "Nothing contradicted me. I never said the word database. The world moved, and the log noticed." Nine justifications carry non-empty OUT-lists; twelve premise-gate records fire;
demo:verifyreports it VERIFIED across three identical dry runs. - A benchmark that reports its own failures.
untestableis a verdict.NOT WIREDis a verdict.vacuous passis a thing the audit now detects. Our ablation currently reports 0 confirmed / 0 falsified / 8 below floor / 5 untestable — and says in plain text that it therefore has not tested the architecture. npm run readiness, which refuses to collapse three different questions into one exit code.- Everything runs keyless and deterministically — same input, same graph, same byte-for-byte export.
- We found and fixed all of it ourselves, then wrote it down: 80+ deviation-log entries, and a
LIMITATIONS.mdwith ten named constraints and a gate-status table that says G6 NOT MET in as many words.
What we learned
Three blind spots, and only one tool per blind spot. A regex structure-checker cannot see a syntax error. Reading code cannot see a wrong contract — a real name with the wrong shape. And neither can see code that runs and silently produces nothing. Only a compiler catches the first two; only execution catches the third. Every one of our worst bugs was type-correct and threw no error.
A passing test suite does not imply a compiling project. Vitest strips types. We had 172 green tests over 8 type errors, and later 172 green tests over 31.
Honesty is a mechanism, not a mood. It only survived because we made it structural: thresholds declared before the run, n printed beside every value, untestable as a first-class verdict, and a report that prints "NOTHING WAS FALSIFIED" in capital letters when that is the result.
The hardest problem in rationale mining is restraint, not recall. ARGUS's 13:1 ratio predicted our experience exactly. Every improvement we made to the headline number came from making the system decline more often, never from making it look harder.
Don't claim novelty you don't have. Three sentences we wrote into our own docs and then refused to say: "nobody has built a decision log for AI coding" (several have), "we do semantic search over your decisions" (everyone does), "we detect contradictions" (Kantara does, over 396 pairs). What is actually new is the given.
What's next for WhyLog
npm run readiness lists eight open gaps with the condition that closes each — so this is a worklist, not a wish list:
- Extraction precision — the one root cause behind refusal, over-firing and weak retrieval. 28 of 34 decision nodes have no ground-truth label behind them, and values like
Use ohare being adopted. - Corpus to 30 transcripts, labelled by someone who isn't the author — the largest methodological weakness in the benchmark, and the reason three metrics are untestable.
- A fixture repository with seeded violations — guard precision currently has no denominator at all (n = 0), because a transcript corpus contains no repo state.
- A real-model pass — the LLM path is reachable, typed and never measured. Every number we report is keyless.
- Close gate (c) on the benchmark, not just on fixtures: a plant whose premise the extractor actually produces, chosen from ground truth without being chosen because the extractor finds it.
- Hypotheticals becoming nodes — 3 of 6 labelled declines still get promoted.
- One falsified hypothesis, which is what Phase 7.3 asks for and what G6 needs.
- A cross-encoder reranker — documented as unavailable rather than faked, worth roughly +27pp precision@1 in the literature.
The destination is unchanged: a log that tells you when something you decided stopped being true, before your agent builds another three features on top of it.
Memory tools stop you repeating yourself. WhyLog stops you building on a decision that stopped being true — which is the more expensive mistake, and the one your agent will never catch on its own.
Log in or sign up for Devpost to join the conversation.