The Rising Sea of Software Engineering — Rebuilding the Discipline on Algebraic Geometry

AI now writes code faster than humans can review it. That is not a prediction; it is the daily experience of most engineering teams.

And here is the other daily experience: no matter how much you invest in tests and CI/CD, end-to-end failures still happen. Every unit test passes. Integration tests pass. CI is green. Production breaks anyway.

I have come to believe this is not a problem of test coverage or pipeline speed. It is a problem of software engineering itself not having caught up — and this article is the record of a climb that begins with that diagnosis: one summit reached (the SAGA theorem), the view seen from it, and the mountains still ahead.

For first-time readers, here is a map of the names that appear in this article:

I wrote about the SAGA Theorem in this article.

The SAGA Theorem: The Day Software Architecture Became Genuine Algebraic Geometry

One promise up front: this article contains three kinds of statements — things that are proved, things that are vision, and things that are unproven. I will keep them separate. Not claiming unproven things as results is the core discipline of this project, and this article follows it.

The foothills — E2E failures have a mathematical name

Start with the diagnosis.

What tests and CI guarantee is local correctness. A unit test verifies one cross-section of one module. Even an integration test only verifies a finite, chosen set of paths.

But E2E failures have a very specific shape: every part is correct, and the whole breaks anyway. Fragments that are locally consistent fail to fit together globally.

Mathematics — sheaf theory in particular — has a precise name for this situation: all local sections exist, but no global section does. And it has a tool that counts the obstructions to gluing: cohomology, starting with H^1.

The phenomenon we call "all tests green, production on fire" — the thing the industry has named integration hell and fought with folklore — turns out to have an exact mathematical name. The crucial point is that the obstruction does not live in any single part. It lives on the overlaps between parts: implicit interface assumptions, shared state, temporal ordering. None of these exist inside a single module. That is why 100% test coverage does not remove them. As long as what you measure is local, you cannot reach them — not in practice, but in principle.

Classical software engineering is built on an unstated composition principle: improve the quality of the parts, and the quality of the whole improves. The gluing problem says precisely that this composition is not automatic. The sum of the local is not the global.

Why AI-driven development makes this worse

It is no accident that AI-driven development is aggravating the problem.

AI is extraordinarily good at local generation, and each generated fragment is individually correct. The faster generation gets, the faster inconsistencies accumulate on the overlaps.

Here is the thing worth noticing: what human review was actually doing was never primarily "checking that the code is correct." It was mentally re-deriving the gluing — "does this change still fit the assumptions of that other module?" That invisible computation is what can no longer keep up.

There are, in principle, exactly two ways to close the gap:

1. Make the reviewer an AI too.

2. Make review a matter of decidable mathematics.

The first inherits an infinite regress — who watches the watchers? In a world where generated artifacts inspect generated artifacts, no agent's judgment carries more authority than any other agent's. I chose the second.

The Rising Sea — the method

Grothendieck approached hard problems in algebraic geometry not by cracking the shell with a hammer and chisel, but by raising the water level of abstraction until, one day, the shell was simply open. In his own words: la mer qui monte — the rising sea.

The history of software engineering has been a history of hammers. E2E breaks? Write more tests. Integration breaks? Make CI faster. Boundaries break? Add contract tests. Each tool is individually correct, and the problem persists — not because the tools are bad, but because the problem is stated at too low a level of abstraction. We have been attacking a local-versus-global problem with local tools.

My research program, AAT, is that raising of the water. Stop handling the underwater rocks — code, modules — directly, and rise to the level of atoms (the theory's axiomatic primitives), sheaves, covers, and gluing. At that altitude, "tests pass but production breaks" stops being an enemy to fight and becomes an ordinary object with coordinates: a class in H^1.

This raising of the water has a practical by-product, too. Because atoms are abstracted away from code, neither the theory nor the measurement depends on any particular language, framework, or library. A Rust microservice fleet and a legacy Java monolith are, given their observations, subject to the same theorems and the same obstructions. There is no rebuilding the tool for every ecosystem, the way linters and architecture tests must be rebuilt — and the theory does not age as technology stacks turn over. Abstraction, in this sense, is also portability.

The problem does not disappear. But it stops being a mystery. What is no longer a mystery can be measured. What can be measured becomes a job for tooling.

Lifted to the right level of generality, a hard problem is not so much solved as rendered trivial. That is the point of the rising sea, and it is the method of this project.

One difference from Grothendieck's own sea: his settled into thousands of pages of prose (EGA/SGA), and later generations struggled to keep the water level up. My sea has its level guaranteed by Lean, a proof assistant. As long as the theorems are formally verified, the water does not recede. The central theorem of this sea is named the SAGA theorem — an homage to Serre's GAGA, the landmark work that established the correspondence between algebraic and analytic geometry. As GAGA bridged two geometries, SAGA is a comparison theorem bridging architecture semantics and algebraic geometry — plus the one layer neither had: machine verification.

And one thing that must not be forgotten: the rising sea was never abstraction as escape. Grothendieck always kept a concrete problem — the Weil conjectures — at the center, as the thing to be submerged. This project has the same shape. The concrete pain of E2E breakage is the shell at the center, the thing the water is meant to close over. The abstraction exists not to leave reality behind, but to trivialize it.

So much for the method. The method is a sea — raise the water, submerge the problem. But the journey of the research itself resembles a climb more than a tide: which peaks have been reached, what could be seen from the summit, which peak comes next. What follows is the record of that ascent.

The ascent — a summit called SAGA (proven)

This section respects claim boundaries strictly. The following already stand.

• The AAT canon — the mathematical text of AAT as pure mathematics, axiomatized on atoms, written with no apologies to tooling or formalization: the mathematics speaks only its own language.

• The SAGA theorem — a comparison theorem: the H^1 grown on the architecture-semantics side coincides with the genuine Čech H^1 on the site generated by atoms. Proved in Lean 4. The ascent took 352 cycles of an automated AI research loop — 347 of them spent stacking impossibility theorems, walls that said this vocabulary cannot reach the summit. In the last 5 cycles, a shift of vocabulary — an architectural law is not a predicate but an equation — broke the bedrock.

• The Lean tower — under the discipline of "formalize only what can be honestly stated," definitions, theorems, and examples are stacked without sorry.

• ArchSig — a measurement tool written in Rust. It takes an observation of the architecture (ArchMap), the laws to uphold (LawPolicy), and an evidence contract, and its H^1 obstruction detection is operational. One design principle matters above all: it speaks only what the given contract lets it speak, and stays silent about everything else. It never completes, guesses, or extends its inputs.

• SFT (Software Field Theory) — the dynamical side. If AAT is statics (the consistency of an architecture at a moment), SFT describes how change propagates through software over time — and it, too, has begun producing theorems.

• The development process itself is the experiment — this repository is developed by AI agents implementing at speed, adversarial reviews and a Lean gate judging consistency, and a human holding only the questions and the acceptance criteria. In other words: AAT and ArchSig are themselves being developed in exactly the style of development they are meant to protect. That self-applicability is, I think, the first evidence that the theory survives contact with real development.

The view from the summit, 1 — a quiet future

From here on, vision. Two views seen from the summit of SAGA.

The first:

An engineer starts the day. She finishes a change and says, "analyze it with ArchSig." A few obstructions are detected. She fixes the code. An E2E failure has been prevented before it ever existed.

What deserves attention in this scene is its quietness. No categories, no sheaves, no cohomology appear in it. The engineer says "analyze," receives one word — obstruction — fixes the code, and moves on. Behaviorally it is indistinguishable from running a linter.

Engineers should never need to learn algebraic geometry — that has been a founding principle of this project, and it is the blueprint of this scene. The closer the theory gets to completion, the less visible it becomes. When the sea has risen far enough, all you can see is the surface.

There is a deeper shift hidden in that scene. The sentence "an E2E failure was prevented" is a counterfactual. A failure that never happened cannot be observed. Today's software engineering has, in principle, no vocabulary for prevented failures — which is why tests can only prove their worth after the fact, and why the quality of an architecture hangs in the air until an incident lands.

Only when obstructions are grounded in theorems does "without this fix, the gluing would have failed" become not folklore but a consequence. That quiet scene is a world in which counterfactuals have become mathematics.

The view from the summit, 2 — a fixed point for a society of agents

There is a more extreme future.

The engineer only watches from outside. Multiple AI agents coordinate dynamically and build software at ferocious speed. Mid-stream, an ArchSig alert fires — ArchSig sits at the deployment gate. The agents read its output and correct the code.

In that future, the code, the tests, the reviews, and the fixes are all AI-generated. Everything stands on the same shifting ground — and the only thing that does not shift is a gate grounded in theorems. Its verdict is nobody's opinion; it is the consequence of formally verified theorems on a chosen contract. In the vortex of high-speed generation, there is exactly one rock that does not move. Only things with that property belong at a deployment gate. ArchSig stops being a human's tool and becomes the fixed point of a society of agents.

In that future, the principle of staying silent about what cannot be said stops being a luxury and becomes a safety device. A human reader will charitably interpret a vague warning; an agent reads output literally and acts literally. A checker that emits "this looks suspicious somehow" will make an agent loop diverge. The discipline of silence turns out to be the interface specification of the multi-agent era.

So where do the humans go? "Watching from outside" means, precisely, moving to the legislature. Who writes the LawPolicy? Who decides which vocabulary may be spoken, and what deserves to be called SAFE? The agents are the executive; the verified gate is the judiciary; humans write the law. You may give up the hands that write code — you have not given up deciding what must be protected. If anything, that becomes the purified human job.

A future in which engineers only watch is not a future in which humans have exited. It is a future in which humans have finished building the grounds for trust.

There is an economic tailwind too. Verification is orders of magnitude cheaper than generation. ArchSig is deterministic computation — effectively free next to LLM inference; a Lean proof, once established, is cheap to re-check. The scarcer compute becomes, the less affordable "LLMs reviewing LLMs" gets, and the more the economics favor cheap deterministic gates that kill bad generations early. It is the same story as type systems paying for themselves when memory was scarce: resource constraints always raise the value of catching mistakes before execution. In the age of ferocious generation, the most expensive thing is discovering a mistake after you generated it.

The way down — the next theorem is literally called descent (unproven)

Mountaineers say the summit is only halfway: a climb is complete only when you are safely down. The ascent of SAGA, too, leaves a way down. And by an almost too-perfect coincidence, the first theorem on that route is literally called the descent theorem.

So that aspiration is never dressed up as achievement, here is what remains unproven:

• The descent theorem (the citadel) — under what conditions does local correctness imply global correctness? This would give, for the first time, explicit validity conditions for the composition principle software engineering has always believed and never proved. The detection direction (a global repair exists ⇒ the obstruction vanishes) is accumulating; the true descent direction (the obstruction vanishes ⇒ a global repair exists) is still open.

• H^2 and above — there is not yet a language for higher obstruction structure. The derived extension is deliberately deferred.

• Fidelity of the observation layer — ArchSig's verdicts can never be more trustworthy than ArchMap's fidelity to the real code. This is the engineering weak point, not the mathematical one, and the defensive line — purifying observation, keeping raw values, excluding judgment from the observation layer — is being built ahead of need.

• Validation on real codebases — H^1 detection finding, on a real project, a gluing failure that humans had missed. The truth of the theory is one question; the value of the tool is decided here.

What changes when descent is proved? ArchSig can turn it into a checkable condition: "this architecture satisfies the hypotheses of descent, therefore passing local tests implies global consistency." And conversely, exactly where the hypotheses fail is where E2E testing should concentrate — the theory gets to point. The view from the summit reaches the valley of the real world only once this way down has been safely walked.

Speaking only what can be spoken

Finally, let me be explicit about what this tool does not say.

What ArchSig can say goes exactly this far: "this change is safe within the given vocabulary and laws." It does not say "this change is good design" — because it cannot. Between the two, there is a deliberately drawn line of silence.

I consider this a condition of trust, not a weakness. A tool that judges beyond what it can judge will, somewhere, inevitably lie. A tool that judges only what it can judge never lies within that range. In an era when AI wants to talk about everything, a tool that speaks only what it can speak is rare — and only such tools belong at a deployment gate.

This article was written under the same discipline: a proven section, a vision section, an unproven section — never mixed.

Closing

Software engineering has not failed to catch up. The necessary mathematics simply had not been imported yet. This research program is that import — and not smuggling, either: it clears customs through Lean.

The open problems are real: descent, higher obstructions, fidelity of the observation layer, validation on real codebases. None of them is light. But the difference between an unclimbable mountain and a climbable one was never the altitude. It is whether you can draw the route.

The water is rising. And a sea, once it starts rising, rises fast.

It can be done. And this is not an unclimbable mountain.

References

• Repository: AlgebraicArchitectureTheoryV2 (MIT license)

• Website: AAT/SFT Research Notes