You Can Draw a Google Docs Design in 10 Minutes. Can You Prove It?
Boxes and arrows on diagram are cheap. System that actually correctly built is expensive.
Most system-design answers stop once the architecture diagram looks plausible:
Client
↓
WebSocket Gateway
↓
Collaboration Service
↓
Database / Cache / Queue / Snapshot Store
That is enough to explain where data flows. It is not enough to explain why the system remains correct when requests are retried, owners fail over, stale processes keep running, snapshots replace history, clients reconnect, ACKs disappear, and engineers start “optimizing” the implementation six months later.
This repository is an experiment in Proof-Driven Development: make a small set of high-impact architectural guarantees explicit, decompose them into independently reviewable proof obligations, and preserve that correctness reasoning as the system evolves.
The goal is not to formally prove every line of application code. The goal is to turn correctness reasoning that senior engineers normally reconstruct from memory into a reusable engineering asset.
Real system-design reasoning often advances one counterexample at a time:
Use a leader.
→ What if the old leader keeps running after failover?
→ Add fencing.
Persist before ACK.
→ What if the ACK is lost and the client retries?
→ Preserve logical request identity.
Compact history into snapshots.
→ Can a retry after compaction still recover the same accepted result?
→ Preserve identity and provenance across lifecycle transitions.
This is useful reasoning. But it has no explicit stopping condition. A design discussion often ends because the reviewers can no longer think of another counterexample, not because the correctness argument has reached a state we can inspect, preserve, and maintain.
Most of that reasoning is ephemeral. It lives in working memory, whiteboards, design-review threads, and the experience of whoever happened to be in the room. Six months later, a performance optimization can invalidate one of those arguments without anyone realizing which responsibility the old implementation was carrying.
Proof-Driven Development asks whether system-design reasoning can have an explicit convergence process:
What are we trying to prove?
What remains open?
What assumptions does each claim depend on?
Can a bad execution still exist while every current claim remains true?
What implementation evidence supports the leaves?
What reasoning became stale after this design change?
The goal is not to make uncertainty disappear. It is to make the remaining uncertainty explicit, and to make each new challenge either discharge an existing obligation or expose a missing correctness responsibility that can be added to the model.
AI did not create this correctness problem. It changes its economics.
Agents can now make broad implementation changes at a throughput that human reviewers cannot match. The urgent problem is therefore not merely how to review more code. It is how to let AI change a system aggressively without silently breaking the small set of correctness responsibilities the architecture depends on.
If every change requires a senior engineer to reconstruct distributed invariants from scratch, AI-driven development does not scale safely. The higher-leverage alternative is to make those invariants persistent and machine-trackable:
senior / staff reasoning once
↓
explicit guarantee / proof obligation
↓
implementation surface / verification boundary
↓
AI changes the system
↓
affected obligations are invalidated and reverified
↓
unaffected reasoning is reused
Human judgment remains essential, but its role changes. Engineers decide what the system actually promises, which assumptions are acceptable, which failure models must be covered, and what evidence is strong enough to trust. Automation should preserve those decisions, detect when a change threatens them, and force the affected reasoning to be reopened instead of silently drifting away from the architecture's original guarantees.
Senior engineers find correctness bugs. Staff engineers try to make the entire class of bugs harder to reintroduce.
Suppose you open a fresh AI agent and ask only one question:
Prove
P = NP, or proveP != NP.
We cannot expect any agent in the foreseeable future to solve that correctly. The prompt is one sentence, but the reasoning space behind it is enormous.
Now ask:
What is
1 + 1?
It would be surprising for a sufficiently capable model to get that wrong.
The prompts are equally short. The essential difference is the size and ambiguity of the reasoning task.
Real distributed-system correctness lives somewhere between those extremes. For example:
Is this collaborative editor correct under retry, failover, reconnect, snapshotting, history compaction, and concurrent ownership changes?
That question is too large to trust as one monolithic LLM judgment. Even a very strong model has to reconstruct too many hidden assumptions, cover too many failure paths, and maintain too many state and semantic relationships in one context.
Formal methods attack this by defining semantics precisely enough for a proof system or model checker. They can provide much stronger guarantees, but the main cost is often not “running the proof.” It is defining the formal state space, transition system, abstraction boundaries, and their correspondence to the real implementation. For an ordinary production system, that modeling cost is usually too high to pay everywhere.
Proof-Driven Development explores a middle ground:
Do not ask one agent to reason about the whole system at once. Keep decomposing the correctness argument until each local proof obligation is narrow, explicit, adversarially checkable, and difficult for a strong verifier to misunderstand.
No local audit is assumed to be infallible. The bet is statistical and economic: when each obligation has precise semantics and a small context, independent strong auditors are much less likely to make the same reasoning mistake than when they are all asked to judge one giant architecture prompt.
The Harness exists to make that decomposition, context isolation, proof reuse, and revalidation systematic.
Traditional development often looks roughly like this:
requirements
→ system design
→ architecture spec
→ implementation
→ tests
→ code review
The correctness argument is usually implicit. It lives in design discussions, reviewer memory, old incidents, and assumptions that happened to survive implementation.
Proof-Driven Development makes that chain explicit:
workload + product requirements
↓
candidate architecture
↓
root correctness guarantees
↓
proof-obligation decomposition
↓
local proof boundaries / assumptions
↓
implementation
↓
executable evidence
A node in the correctness graph is a proposition, not a service, class, file, or box in an architecture diagram. An edge means logical proof dependency: if a lower-level proposition is no longer trusted, every guarantee that depends on it must be reconsidered.
That makes the correctness model resemble a build dependency graph:
semantic change
↓
affected proof obligation
↓
transitive invalidation
↓
re-establish only the affected guarantees
A compiler rebuilds artifacts after source dependencies change. The Harness tries to do something analogous for correctness reasoning.
The detailed Harness semantics and type system live in correctness/SPEC.md; the current machine-readable model lives in correctness/correctness.yaml.
This repository is an experiment, not a claim that the methodology already works universally.
The hard questions are economic and operational:
- Can correctness reasoning for a non-trivial distributed system converge into explicit, maintainable obligations instead of remaining an open-ended sequence of reviewer challenges?
- Can local proof obligations become precise enough that multiple independent AI auditors are sufficiently reliable on them?
- Can specification gaps and bad decompositions be discovered without repeatedly reopening the entire system context?
- Can implementation changes be mapped to affected proof obligations with sufficiently high recall?
- Can enough leaf obligations ultimately be discharged by mechanical evidence that the model reduces, rather than increases, human review cost?
- Can invalidation propagation remain local enough that AI can keep changing the system without forcing whole-system correctness reasoning after every meaningful modification?
If the answers are mostly no, Proof-Driven Development becomes specification bureaucracy.
If the answers are mostly yes, correctness reasoning can become a reusable and maintainable engineering asset instead of something that existed briefly in the previous reviewer’s head.
A collaborative editor is a useful case study because the product is intuitive while the correctness argument is not.
At the UI level, the requirement sounds simple:
Multiple users edit the same document and eventually see the same result.
But the architecture quickly depends on harder properties:
- an acknowledged edit must survive owner crash or failover;
- retrying one logical edit must not create a second canonical operation;
- accepted revisions must form one gap-free authoritative history;
- after ownership has moved, the stale owner must not continue appending;
- snapshot plus replay must reconstruct the same observable state as authoritative history;
- reconnect must neither omit nor double-apply accepted changes;
- lifecycle operations must not silently destroy the identity or provenance needed for retry and recovery.
These are not merely implementation details. They determine whether the architecture is actually the architecture we think it is.
Consider a simplified example.
Suppose documents.latest_revision is updated synchronously for every accepted edit. Someone notices that it has become a per-document hot row and proposes:
Let
accepted_changesbe the source of truth and updatelatest_revisionasynchronously.
At the database level, this sounds like an ordinary performance optimization.
But suppose the current correctness argument uses the revision frontier as part of the serialization contract:
append revision r may commit only if
pre.latest_revision == r - 1
and after commit
post.latest_revision == r
If latest_revision becomes eventually consistent, it can no longer carry that proof responsibility.
That does not automatically forbid the optimization. The engineer can replace it with an authoritative tail lookup, sequencer, lock, transactional append primitive, or some other mechanism that proves the same property.
The important distinction is:
Replacing an implementation is fine. Silently deleting the proof responsibility it carried is not.
Without an explicit correctness model, code review might stop at:
remove synchronous frontier update
→ reduce contention
→ looks good
With a proof graph:
frontier semantics changed
↓
serialization proof obligations affected
↓
dependent guarantees become stale
↓
replacement reasoning or evidence required
This is the practical value of the proof graph: the reviewer no longer has to reconstruct the whole architecture from memory before realizing that a seemingly local field carries a system-level invariant.
As the Harness evolved, one distinction became central: there are several different ways a correctness model can be wrong, and they require different assurance layers.
refinement
Is this proposition/decomposition well formed?
specification coverage
Did we forget an important proposition or relation entirely?
composition
Do these direct premises actually imply this target?
implementation evidence
Does the real system satisfy the leaf proposition?
The first, third, and fourth questions can become increasingly mechanical once the relevant property has been stated. The second is fundamentally more open-ended. A solver cannot prove that a missing variable, provenance relation, terminal outcome, or namespace coordinate should have existed if nobody represented it in the model.
The practical strategy is therefore to use semantic audits to discover missing correctness relations, then convert those discoveries into typed structure that future tooling can enforce. For example, provenance-sensitive state may declare a resource scope such as document; once that semantic choice is explicit, the Harness can mechanically reject a provenance contract that binds the value fields but forgets the document namespace. Likewise, an invariant can be forced to expose both its establishment boundary and the transitions that must preserve it.
This is the boundary the project is trying to push:
Human/LLM judgment discovers what relation matters. Typed contracts, validators, signatures, and mechanical evidence make it progressively harder to forget or silently break that relation again.
The initial decomposition is not assumed to be correct. It must be attacked continuously and adversarially.
A local verifier receives only the context required to judge the current proposition: the target, its direct premises or local proof boundary, relevant system semantics, and the failure model. Its first job is to construct a counterexample, not to produce a persuasive explanation.
That process can expose several different defects:
missing premise
wrong dependency
one claim bundles multiple independent obligations
missing lifecycle transition
incorrect provenance assumption
genuine ambiguity in the system semantics
Context isolation does not mean “a short prompt magically becomes a proof.” It means each verifier faces a narrower problem with less room to smuggle in unstated assumptions.
The Harness then surrounds the uncertain reasoning step with machinery that is as deterministic as practical:
clean-context local audit
↓
semantic judgment
↓
typed mutation
↓
validation
↓
signature-based invalidation propagation
↓
next local audit frontier
Lower-level propositions that have already been audited can be reused as opaque contracts instead of reopening the entire subtree every time a parent is examined. If the lower-level semantics change, recursive signatures automatically reopen the affected reasoning.
This is where the methodology tries to improve reliability without paying the full modeling cost of formal verification: keep human/LLM reasoning as local as possible, and make the control machinery around that reasoning as deterministic as possible.
A beautifully decomposed DAG is still only a specification artifact if its leaves are not connected to implementation evidence.
Different properties deserve different verification mechanisms. A leaf might ultimately be checked by:
schema / uniqueness constraint
transaction contract test
control-flow / static-dataflow analysis
state-machine / property-based test
concurrency test
fault injection
replay / differential test
runtime invariant
model checker
The engineering question is not “How do we formally prove everything?” It is:
For this particular proof obligation, what is the cheapest independent verifier that still provides enough assurance?
That distinction matters. A database uniqueness property should not require an LLM to reread the whole service. A crash-durability claim should not be considered proven merely because the code says it flushes. Evidence should observe the real property through an independent and economical boundary whenever possible.
Production systems contain enormous amounts of feature-specific behavior. Many bugs matter to users without belonging in an architectural correctness DAG.
Proof-Driven Development is aimed at properties that are repeatedly depended on over time and are easy for later changes to break accidentally:
idempotency
ordering
fencing
durability
atomic state transitions
state invariants
provenance bindings
snapshot / replay equivalence
recovery / migration safety
The useful boundary is not “important bug versus unimportant bug.” It is closer to:
Is this a stable, high-blast-radius correctness responsibility that many future changes must keep preserving?
If not, ordinary tests and code review may be cheaper.
Scope control is only half of the cost model. The other half is keeping invalidation local.
A proof system that reruns expensive whole-system reasoning for every one-line change is economically useless.
The target workflow must remain local:
implementation change
↓
map to affected implementation surfaces
↓
no relevant correctness obligation? ───→ ordinary review
↓
affected proof obligations
↓
local invalidation
↓
reasoning / evidence only where needed
Most code changes should never trigger deep correctness work.
Maintenance cost should scale with blast radius, not repository size or diff size.
That locality is one of the central hypotheses this project is testing. If every change eventually invalidates the entire graph, the methodology has failed operationally even if the model is theoretically correct.
This is not a claim that ordinary application code should all be formally proven, that tests or code review become unnecessary, or that LLM judgments are authoritative.
It is an attempt to connect several existing practices into a stronger chain:
system guarantee
→ proof responsibility
→ local reasoning boundary
→ implementation surface
→ independent evidence
→ change impact
→ targeted revalidation
Formal methods remain the right tool when the risk and economics justify them. Ordinary tests remain the right tool for most ordinary behavior. Proof-Driven Development explores the space in between.
The repository deliberately separates the target-system design from the Correctness Harness:
design/google-docs.md— the collaborative-editor architecture being analyzed;correctness/SPEC.md— the human-readable mental model for the Correctness Harness;correctness/SCHEMA.md— the canonical model field/type reference;correctness/correctness.yaml— the current machine-readable correctness model;correctness/correctness.py— validation, slicing, scheduling, semantic signatures, assurance state, and controlled mutation;HANDOVER.md— current operational snapshot, campaign state, and recommended continuation;AGENTS.md— repository operating rules for agents.
A ten-minute architecture diagram can show where requests go.
A serious system design must also explain what remains true when requests race, retries overlap, machines fail, ownership changes, snapshots replace history, and future engineers start optimizing the implementation.
The deeper problem is not merely finding a good design. It is knowing when the correctness argument has converged enough to trust, preserving the reasoning that got us there, and reopening exactly the right parts when the system changes.
The core insight of this project is that we do not need one human or AI to hold the entire proof in its head at once.
If we can keep decomposing the argument into small enough proof obligations, give each verifier exactly the context it needs, attack those obligations from multiple independent perspectives, connect the leaves to real implementation evidence, and deterministically reopen the right reasoning when semantics change, then trustworthy correctness reasoning may become much cheaper to maintain over time.
Do not ask one agent to prove the whole system correct. Build a proof system that keeps giving AI questions small enough that errors become hard to hide.