DEV Community: Hiroyuki Nakahata

Atom Is All You Need: Read a Codebase as an Atom Map, Not a Dependency Graph

Hiroyuki Nakahata — Sun, 31 May 2026 16:55:51 +0000

TL;DR

In the AI era, architecture analysis cannot stop at reading code as files, functions, imports, and dependency graphs.

We need to observe the smallest units that carry architectural meaning. I call those units Atoms.

By extracting Atoms from a codebase and reading the algebraic structure they generate, we can analyze architecture beyond ordinary dependency relationships.

The workflow looks like this:
codebase
  -> Atom observations
  -> ArchMap
  + LawPolicy
  -> ArchSig analysis packet
  -> architecture reading
This lets us see design pressure, semantic coupling, missing evidence, and review focus that ordinary linting, static analysis, and dependency graphs often miss.

We built a new tool for this workflow: ArchSig.

The repository is public and MIT licensed, so you can try it on your own codebases.

The key idea is simple:

Architecture analysis does not need a bigger natural-language summary.

It needs the right unit of observation.

Why We Need an Architecture Analyzer

AI agents can write code fast.

But writing code fast is not the same thing as evolving a system well.

For an AI agent, the codebase is the largest prompt.

If the existing codebase contains shortcuts, those shortcuts become examples.
If boundaries are vague, new code naturally lands in vague places.
If responsibilities are mixed, that mixing becomes part of the next implementation context.

Traditional tools often look at the current shape of code:

import graphs
dependency cycles
layer violations
lint rules
complexity metrics
test coverage
security rules

All of these matter.

But in AI-era architecture review, we often want to ask deeper questions.

Imagine a business backend where users select input data, run automated processing or generation, persist the result, receive events from external systems, run async jobs, call external providers, and save generated artifacts back into business state.

The important questions are not only:

Are the dependencies pointing in the right direction?

We also want to know:

Who is allowed to use which input for which operation?
Through which validation path does generated output become persisted state?
Where is an external provider failure recorded as durable state?
Do two workflows that produce the same artifact actually have the same effect order?
Do entrypoint-level permissions match the intended business scope?
Are privileged operations separated from ordinary workflow authority?

These are difficult to read from a dependency graph alone.

We need to read code not only as a collection of files and functions, but as a set of observations that carry architectural meaning.

That unit is the Atom.

Atom: The Smallest Unit of Architectural Meaning

An Atom is the smallest observation unit I want to use when reading architecture.

It is not necessarily a function, class, module, or file.

In practice, it is the thing you point at during review and say:

This is a boundary.

This is state.

This is an effect.

This is a contract.

This is where trust changes.

Examples of Atom families include:

component atom: an architectural unit exists
relation atom: two units or atoms are related
capability atom: a unit provides a specific capability
state atom: something is persisted or held as state
effect atom: an external call or side effect occurs
authority atom: someone is allowed to do something
trust relation atom: some output or provider is trusted up to a boundary
contract atom: inputs, outputs, preconditions, or failure behavior are promised
semantic atom: something has architectural meaning beyond its code location

The important point is that an Atom is not small in the syntactic sense.

It is small in the architectural sense.

For example, the observation:

Only an authorized actor may update this resource.

may cross multiple files.

The observation:

Generated output must pass through a service-level contract before persistence.

may cross a route, service, validation layer, job state, and repository.

Still, each observation is one meaningful unit in architecture review.

That is what an Atom records.

A Small Code Example

Even a tiny function can contain multiple Atoms.

def publish_artifact(actor, artifact_id, repository, gateway):
    artifact = repository.load_for_actor(actor.id, artifact_id)
    gateway.publish(artifact.payload)
    artifact.mark_published()
    repository.save(artifact)

If we only say "this is one function," we miss most of the architectural content.

Read as Atoms, we can observe at least:

component: repository and gateway are architectural units
relation: the handler flows into both the repository and the gateway
capability: the repository provides load/save, while the gateway provides publish
state: the artifact's published state is persisted
effect: gateway.publish changes external state
authority: the actor must be allowed to publish this artifact
trust_relation: the gateway response and failure behavior must be trusted only through a boundary
contract: publish success, save failure, and retry behavior need explicit promises
semantic: published is not only a flag; it means externally visible

These nine Atom schemas are the basic vocabulary for treating primitive architectural facts as generators of an architecture object.

ArchMap: Turning a Codebase into an Atom Map

An ArchMap is a map of these observations.

It is not a full copy of the codebase.
It is not an AST dump.
It is not only a dependency graph.

It is a source-grounded map of architectural observations.

source code
  observed as
Atom / Molecule / Semantic observations
  recorded as
ArchMap

If an Atom is one observation, a Molecule is a finite composition of Atoms that acts as one responsibility boundary.

For example, an ArchMap of a backend might contain Molecules such as:

authenticated request boundary
credential lifecycle
repository transaction boundary
interactive processing workflow
input-to-artifact pipeline
external integration ingress
job-managed generation surface
input-backed artifact boundary
edge policy and observability boundary
privileged governance boundary

The important point is not that the codebase has folders such as api, services, repositories, and models.

The important point is that architectural meaning sits on top of those folders:

authority
generation
external effect
durable state
artifact lifecycle
semantic contract

ArchMap records that meaning in a machine-readable form.

AAT: Reading Structure from an Atom Map

Once we have an ArchMap, we can ask a different kind of question:

Under which laws does this architecture object have pressure?

AAT, Algebraic Architecture Theory, reads software architecture as an algebraic structure generated from Atoms.

It studies architecture through objects, operations, laws, invariants, obstructions, and signature axes.

I will leave the detailed theory to Algebraic Architecture Theory.

For this article, the intuition is enough:

law: a design property we want to preserve
witness: observed evidence related to that property
obstruction: a structure that blocks the law
signature axis: the direction in which pressure appears
operation: a design operation such as split, move, protect, or refactor
path / homotopy: whether two change paths preserve the same structure
curvature / holonomy: when something looks locally natural but becomes inconsistent around a loop

In ordinary review, engineers often process these ideas in their heads:

This responsibility is mixed.

This external call should not be inside the transaction.

These two job statuses look the same, but the failure paths differ.

This generated output must be validated before it becomes domain state.

AAT tries to move this review vocabulary toward something we can compute.

The important step is to treat Atoms not as labels, but as primitive facts that generate architecture objects.

Once Atoms carry relation, state, effect, contract, and semantic axes, we can see things a dependency graph cannot show:

a locally natural change that changes effect order through another path
a split that moves complexity to another boundary
two workflows that look statically similar but differ under a semantic contract

These are non-trivial architecture readings.

They should not live only in a senior engineer's intuition.

They should be tied to a selected law universe and a selected set of witnesses.

That is the role of AAT.

ArchSig: Reading Structure from ArchMap + LawPolicy

ArchSig takes an ArchMap and a LawPolicy, then produces an AAT-style analysis packet.

ArchMap
  + LawPolicy
  -> ArchSig
  -> analysis packet

LawPolicy is the interpretation profile.

It selects the law universe, witness rules, signature axes, measurement policy, and coverage requirements for the analysis.

The same ArchMap can be read in different ways depending on what you care about:

authority boundaries
state/effect consistency
generated output mediation
domain cohesion
permission coverage
repair preconditions

ArchSig does not collapse all of this into one "good / bad" score.

It reports pressure and semantic coupling along different axes.

The output can include readings such as:

nonzero pressure by law axis
workflow risk
transfer bridge pressure
state/effect reconciliation pressure
operation squares
axis-wise monodromy defects
architectural holes
boundary holonomy
repair precondition blockers
review focus

This is not a code quality score.

It is a measurement surface for reading where design pressure and semantic coupling appear.

Case Study: Analyzing a Backend Repository

So far, the discussion has been conceptual.

Now let us look at the shape of one backend repository through ArchSig.

This repository has multiple users, authority boundaries, business data, external effects, async jobs, and generated outputs.

Users select input data and run analysis, generation, extraction, or transformation workflows.
External systems send events.
Async jobs call providers.
Results are persisted as business artifacts.

From the ArchMap, ArchSig could read structures like:

a backend split into API, service, repository, model, schema, and task layers
authority boundaries across users, organizations, and resources
a domain model where multiple artifacts derive from input data
generated output mediated by service contracts and job state
external provider effects paired with durable job state
privileged operations separated from ordinary workflows

This is already different from a dependency graph.

ArchSig reads the repository as a business backend with authority boundaries, generated outputs, external effects, and durable state.

The Design Pressure It Found

The strongest pressure appeared at the intersection of authority and generation.

The system is not merely saying:

An authenticated actor can run generation.

The real architectural question is:

Who can use which resource as input, and which generated output can become which domain state?

That is a central boundary.

Reviewing only authorization is not enough.
Reviewing only the generation job is not enough.
The two boundaries are bridged.

The next large pressure was state/effect reconciliation.

The repository has external providers, async jobs, event handlers, retries, roundtrips, and compensation paths.

In this kind of system, not everything can live inside one transaction.

The architecture needs durable intermediate state, external effect recovery, explicit failure finalization, and retryable paths.

ArchSig reads this through the relation between state atoms and effect atoms.

The third pressure was generated output mediation.

Generated output is useful, but it should not become domain state without mediation.

You need input construction, structured output, filtering, validation, job failure handling, and persistence gates.

In this repository, the mediation appeared across multiple workflows:

interactive workflows
analysis execution
content extraction
generated artifact creation

So the design question is not:

Does the system use generation?

The real question is:

Through which contract does generated output pass before it becomes domain state?

This is not just dependency analysis.

It is a reading of where authority, state, effect, contract, and semantic meaning overlap.

Same Destination, Different Path

One of the most interesting ArchSig readings is the monodromy defect.

The intuition is:

Two paths may appear to arrive at the same place.

But do they preserve the same structure?

In the repository, several workflows looked similar from the outside.

They produced artifacts or updated state.

But the order of provider calls, repository commits, job state transitions, and status finalization could differ.

A dependency graph may not show that.

Even if the static dependencies point in the same direction, the workflow path can change failure behavior.

Does the system create state before calling the provider?
Does it call the provider first?
Where is failure finalized?
Does retry use the same idempotency key?

ArchSig reads this kind of path difference as operation squares and axis-wise defects.

This is practical in review.

When someone says:

This follows the existing pattern.

ArchSig helps ask:

Does it really?

It may look like the same endpoint.
It may create the same kind of artifact.

But if the effect order differs, the operational behavior differs.

That difference often becomes incident cost or future refactoring cost.

Architectural Holes: Loops That Do Not Close

Another important result was the architectural hole.

ArchSig found holes around paths such as:

API -> service -> repository
async provider jobs
generated output -> domain state promotion
semantic contracts

This does not mean "there is a bug."

It means the evidence is not enough to say the architectural loop is closed.

For example, the path from generated output to domain state may involve:

input data
context construction
structured output
validation
job state
repository persistence

To say this loop is closed, source reading alone is not enough.

You may need test evidence, runtime traces, provider logs, and entrypoint-by-entrypoint permission audits.

ArchSig does not treat missing evidence as zero.

It preserves it as a hole.

That matters because one of the dangerous failure modes in architecture review is to read "unknown" as "fine."

ArchSig keeps the gap visible.

And the gap becomes a review proposal.

gap:
  - permission evidence is incomplete
  - runtime trace is missing
  - provider failure path is not covered

review proposal:
  - human reviewer: check authority boundary and failure handling
  - LLM reviewer: compare the generated output path with the declared contract
  - test reviewer: add evidence for retry and finalization behavior

In other words, ArchSig does not hide uncertainty.

It turns uncertainty into review focus.

Spectral Analysis: Where Pressure Comes Back

One of the most interesting parts of ArchSig is ArchitectureSpectrumReport.

Ordinary review often ends with a list of issues.

But in architecture, pressure does not always appear once and disappear.

An authority mismatch can show up in generated output persistence.
From there it can move into job state.
Then it can come back through retry behavior or provider failure handling.

Spectral analysis reads this recurrence.

curvature support
  -> transfer edge
  -> recurrent mode
  -> hotspot / witness cluster
  -> review focus

Again, the point is not a single score.

The interesting questions are:

Where does pressure concentrate?
Which obstructions recur?
Which witness clusters cross multiple law axes?
Which coverage gaps block a zero reading?
Which boundary should be reviewed before a repair candidate is trusted?

From a dependency graph, a workflow may look cleanly separated.

But spectral analysis may show remaining transfer between effect order, semantic contract, job state, and authority boundary.

That is not simply "there is a cycle."

It is a more structural reading:

Locally separate pressures return to the same support inside the architecture object.

ArchSig can surface that as a hotspot.

Repair Candidates Are Not Automatic Fixes

ArchSig can also produce repair candidates.

In this repository, many candidates were stopped by precondition blockers.

That is important.

Seeing pressure does not mean the system should immediately be split or rewritten.

If you cut one boundary, complexity may move somewhere else.
Fixing authority may increase runtime effect pressure.
Strengthening generated output mediation may change job state and retry paths.

ArchSig does not treat repair as an automatic safe edit.

It checks preconditions, witnesses, coverage, and transfer risk.

This is close to how experienced engineers review architecture:

This looks risky.

But before fixing it, we need this evidence.

That difference matters.

How This Differs from Existing Tools

So what exactly is different?

Existing tools are good at reading the current shape of code:

Does a dependency cycle exist?
Is there a layer violation?
Is test coverage missing?
Is a security rule violated?
Is complexity too high?

ArchSig is trying to read something else:

Where are responsibility boundaries composed?
On which law axis does pressure appear?
Do two paths with the same destination preserve the same effect order?
Where do generated output, external providers, authority, and durable state intersect?
Would a repair candidate move complexity to another boundary?
Which evidence is missing, and therefore should become review focus?

This is not a code quality metric.

It is an instrument for reading architectural state.

Another important point is that review can happen around the ArchMap artifact.

The source-grounded observation still has to be produced from real code.

But after that, sharing, reviewing, and comparing can happen around ArchMap and the analysis packet.

That matters for teams and companies that cannot freely share full codebases.

There is also an AI angle.

If you simply ask an LLM to review a large codebase, the full context will not fit.

Even if it does fit, it is hard to make the model consistently focus on:

the right boundary
the missing evidence
the relevant law axis
the path where effect order differs

ArchMap and ArchSig change the shape of the context.

Instead of handing the model all code and asking for a huge summary, you hand it Atoms, Molecules, law axes, holes, and review focus.

Then the model can reason around the architecture boundary that actually matters.

Atom Is All You Need

Trying to understand a large codebase all at once breaks down quickly.

There are too many files.
Too many functions.
Too many dependencies.
Too many external providers.
Too much code added by fast AI agents.

So start with Atoms.

component
relation
capability
state
effect
authority
trust_relation
contract
semantic

Observe them.
Record them as an ArchMap.
Choose a LawPolicy.
Run ArchSig.

This lets us read meaningful architecture boundaries without pretending we can understand the entire codebase at once.

What AI-era architecture analysis needs is not a larger natural-language summary.

It needs the right unit of observation.

Atom is all you need.

The Review Experience This Enables

Future review could look like this.

First, generate an ArchMap delta from a codebase or pull request.

Then run ArchSig using the team's selected LawPolicy.

The reviewer no longer has to read the entire diff as a flat pile of changes.

They can focus on the boundaries that require design judgment.

This change touches:
  - authority boundary
  - generated output mediation
  - state/effect reconciliation
  - async provider job path

Measured pressure:
  - nonzero on permission coverage axis
  - positive path continuation defect on effect axis
  - architectural hole on output promotion path

Review focus:
  - entrypoint-level permission evidence
  - job finalization behavior
  - provider failure handling
  - persistence gate before domain promotion

AI agents can read the same packet.

They can implement with more than a request like:

Just add the feature.

They can receive architectural constraints:

Preserve this Atom.

Do not cross this boundary.

Do not increase pressure on this law axis.

Do not treat these paths as equivalent; their effect order differs.

That matters because AI agents are strongly shaped by context.

If you give them only the codebase, you also give them every existing shortcut.

If you give them the ArchMap and the ArchSig analysis packet, you also give them the architecture's structural pressure and semantic coupling.

Closing

ArchSig is not a tool for grading code.

It is an architecture analyzer for reading a codebase as an Atom map, then using AAT to surface design pressure, semantic coupling, holes, and repair preconditions.

It does not replace dependency graphs, lint, coverage, or security tools.

Those are still important.

But there are questions they do not answer:

Where do authority and generated output intersect?
Where does state/effect order diverge?
Are two paths that create the same artifact really the same architecture operation?
Would this repair candidate transfer complexity to another boundary?

Those are the questions ArchSig is built to make visible.

Start from Atoms.
Record them in ArchMap.
Read them through AAT.
Analyze them with ArchSig.

That is the architecture analysis shape I wanted to introduce.

What Comes Next: SFT and FieldSig

We are also working on the next layer of this research.

AAT makes software architecture locally algebraic.

ArchSig becomes an observation instrument for that local algebra: it takes Atom observations and law-relative structure from a codebase and turns them into an analysis packet.

Beyond that is SFT, Software Field Theory.

SFT is about software evolution.

It does not only ask about the current architecture state.

It asks how review, AI agents, CI, operational feedback, and organizational decisions change the space of possible future software states.

FieldSig is the next measurement surface.

It reads ArchSig analysis packets and workflow evidence in order to make software evolution more computable.

ArchSig is the entrance.

That said, ArchSig is still at v0.3.1.

I do not want it to be judged as a finished product yet.

I want people to try it on many different repositories and tell us what it reads well, what it misses, and where the model feels wrong.

Good reads and bad reads are both valuable for the research.

You can get the ArchSig release bundles here:

AlgebraicArchitectureTheoryV2 Releases

I Open-Sourced the AAT / SFT Research Repository

Hiroyuki Nakahata — Sun, 24 May 2026 05:13:39 +0000

I open-sourced the AAT / SFT research repository.

Repository:

https://github.com/iroha1203/AlgebraicArchitectureTheoryV2

This repository is for building theory and tools that treat software architecture not only as a blueprint or a list of best practices, but as something that keeps evolving through changes, reviews, CI, operations, and proposals from AI agents.

The larger goal is to make the evolution of software and computers something we can measure, compare, and reason about, instead of only looking back after the fact.

What This Research Is About

The repository is organized around three ideas.

AAT makes architecture locally algebraic.
ArchSig makes architecture observable.
SFT makes software evolution computable.

AAT stands for Algebraic Architecture Theory.

It treats software architecture as a local algebraic structure.

In more practical terms, it asks questions like these:

Did this design change preserve dependency direction?
Did it cross a layer boundary?
Does it still depend on abstractions instead of concrete details?
Did it make failures easier to spread?

ArchSig is a set of tools for extracting architecture signals from real codebases and pull requests.

It is not meant to produce one big "good / bad" score. Instead, it separates different kinds of risk: dependency cycles, boundary violations, abstraction leaks, unmeasured parts of the system, and other signals that should be read separately.

SFT stands for Software Field Theory.

It treats software evolution as a sequence of changes and tries to make that evolution computable.

PRDs, issues, pull requests, reviews, CI, organizations, and AI agents do not only affect the current change. They also shape what kind of change is likely to happen next.

For example, a vague PRD can invite an ad hoc implementation. A codebase with clear boundaries tends to make the next change easier to place cleanly. SFT develops concepts for reasoning about what futures become easier to reach after a change.

Why I Am Building This

AI can generate working code very quickly.

But whether a fast diff makes future changes easier, or instead adds more ad hoc implementation, is a different question.

The question is not only:

Do the tests pass?

I also want to ask:

Did this change preserve the design properties we care about?
If not, what code or dependency shows the problem?
Is the problem a dependency cycle, a boundary violation, or an abstraction leak?
Does this PRD, issue, or pull request make the next change easier to move in a good direction?
Can review and CI stop risky change patterns early?

The motivation behind this repository is to turn those questions into something we can formalize, observe, and eventually support with tools.

What Is In The Repository

The repository currently contains:

Lean formalization for AAT
Research notes for AAT and SFT
Rust implementation of the ArchSig tools
Open proof tasks and a Lean theorem index
A static website for reading AAT, SFT, and ArchSig

On the Lean side, I am building small theorem packages with explicit assumptions.

On the Rust tooling side, I am working toward reports that extract design signals from codebases and pull requests, then make them readable in review and CI.

On the website side, I am preparing public-facing research notes and manuals for AAT, SFT, and ArchSig.

This Is Still Research

This repository is a working research space, not a finished product.

I separate different kinds of claims:

what has been proved mathematically,
what has only been defined so far,
what I want to prove later,
and what should be checked against real development data.

For example, a theorem proved in Lean does not automatically predict the future of a real project.

There is a difference between a tool saying "this dependency was observed," Lean proving "this property follows under these assumptions," and empirical work saying "this trend seems to appear in real development data."

The repository keeps those claims separate.

Where To Start

The README is the best entry point.

https://github.com/iroha1203/AlgebraicArchitectureTheoryV2

If you want to go deeper, I recommend this order:

Research goal
AAT mathematical theory
AAT / SFT interface
Software Field Theory
Lean definitions and theorem index
ArchSig tooling documentation

Website

There is also a website for reading AAT, SFT, and ArchSig as connected research notes.

https://iroha1203.dev

If you want the big picture before reading code or proof details, the website is the easier place to start.

Closing

The short version is:

I want to treat software architecture and software evolution as things we can observe, diagnose, and compute.

I do not want design principles to remain slogans.

I want to ask what properties they preserve, what failures they reveal, and what futures they make easier to reach.

This repository is where I am building the theory, formalization, tools, and public notes for that direction.

Forecast Cone: A Grand Theorem for Computable Software Evolution

Hiroyuki Nakahata — Fri, 22 May 2026 17:50:41 +0000

TL;DR

This article starts from the ForecastCone in Software Field Theory (SFT), then reads modularity, technical debt, review, governance, and learning as parts of one research program.

The goal is simple to state:

Make it possible to see what futures a change opens, close dangerous futures early, and shape the development environment so good futures become easier to reach.

If this theorem-shaped program works, architecture, technical debt, review, governance, and AI coding safety can all be reread around the same object: the ForecastCone.

We are also formalizing this direction in Lean by breaking concepts such as ForecastCone and ConsequenceEnvelope into small records and theorem packages.

For the Bigger AAT / SFT Picture

I introduced the broader AAT / SFT framing here:

The Problem: Fast Code Is Not the Same as Healthy Evolution

For an AI agent, the codebase itself is the largest prompt.

If the existing code contains many shortcuts, the agent can easily learn those patterns.
If boundaries are vague, the agent will naturally add the next change in the vague place.
A good structure attracts good changes. A bad structure repeatedly makes bad shortcuts look natural.

PRDs, issues, review policies, and CI rules do not only decide "this change."
They shape what the next PR tends to look like, which modules feel natural to touch, which boundaries are easy to miss, and which shortcuts are likely to pass.

In vibe coding, for example, an AI agent can quickly produce a plausible implementation from an underspecified PRD.

A PRD that only says "make coupons usable" may turn into a small if inside the checkout flow.
The first demo works.
But if that change leaves pricing policy, refunds, usage limits, and audit logs as vague boundaries, the next PR will often build on the same shortcut.

The problem is not that AI writes bad code.
The problem is that vague artifacts plus fast generation can open bad future paths very quickly.
A bad field can be amplified by AI into larger technical debt.

Traditional review, CI, and metrics often look at the current diff or at outcomes that already happened.
In the AI era, that is not enough.

The question is no longer only:

Does this PR pass right now?

The deeper question is:

What future does this PRD, this agent, this codebase, and this review rule open next?

SFT needs ForecastCone in order to ask that question.
It gives us an object for making software evolution computable, not as a mere sequence of changes, but as a space of reachable futures.

The Grand Theorem: A Fundamental Theorem of Software Evolution

Modularity
  = ForecastCone descent

Technical debt
  = descent obstruction

Review
  = minimal decision-preserving envelope

Governance
  = desired-cone-preserving obstruction cutting

Learning
  = closed-loop boundary-explicit fixed point

In this article, I will call this theorem-shaped picture the Fundamental Theorem of Software Evolution.

In everyday engineering language, it says something like this:

A good architecture boundary lets teams and AI agents work separately, then combine their changes safely later.

Technical debt is the ability to explain, with a concrete cause, why integration keeps breaking at the same place.

In review, we do not want every diff line or every possible future. We want the dangerous futures that matter for the decision.

Governance should not just add rules that stop development. It should close bad shortcuts and make good implementation paths easier to choose.

Learning means using actual PRs, incidents, and review outcomes to update the next forecast and the next rule.

In more mathematical language:

A good architecture boundary is not merely a static dependency cut. It is a boundary across which future evolution paths can be computed locally and glued into a global future under compatibility conditions.

Technical debt is an obstruction that appears when that gluing fails.

Review is not the act of seeing the entire ForecastCone. It is the act of seeing an envelope that preserves the distinctions needed for a decision.

Governance is a support transformation that removes bad futures while preserving desired futures.

Learning is a closed-loop update that moves a field estimate toward a boundary-explicit fixed point using PRs, incidents, reviews, and operational outcomes.

If such a theorem can be proved, the way we reason about software evolution changes.

Whether an architecture is good, where technical debt sits, what a reviewer needs to see, which governance rule is effective, and how the field model should be updated next can be studied over the same computational object.

That object is the ForecastCone.

ForecastCone: The Range of Reachable Futures

SFT reads the development environment as a field.

codebase
  + artifacts
  + practices
  + agents
  + governance
  + feedback
  -> reachable software futures

The range of futures reachable under that field is what SFT calls a ForecastCone.

A ForecastCone is not a prophecy.

SFT does not say:

This PRD will definitely produce this PR.

Instead, it asks:

Under this field model, operation support, policy, observation boundary, and horizon, which future paths are reachable?

Imagine an e-commerce service receives a PRD: "Add limited-time coupons."

That PRD does not open just one future.

One future adds a small branch to the checkout flow.
One future adds a discount policy to the pricing service.
One future introduces an independent coupon domain.
One future expands into campaign rules and audit logs.
One future adds a database column for now and leaves cleanup for later.

All of these are, in some sense, "coupon support."
But they open very different next futures.

The ForecastCone is the object that lets us look at that difference.
The same PRD can make different futures easy or hard to reach depending on the current codebase, module boundaries, past workarounds, review rules, CI, and AI agent behavior.

Modularity = ForecastCone Descent

Modularity
  = ForecastCone descent

The intuition is:

The global future of a software system can be computed by gluing compatible local futures.

Traditional modularity is often described in terms of APIs, dependency direction, and responsibility separation.
SOLID, Layered Architecture, Clean Architecture, and Design Patterns have often been used as ways to help humans understand responsibilities, localize change, and control dependencies.

SFT extends that line of thought by asking:

Do the futures glue?

If a boundary is truly modular, we should be able to reason about the future of Pricing and the future of Checkout locally, then glue them into one checkout future under the right compatibility conditions.

The boundary is not just a line. It is a place where future evolution should cross without breaking.

In practice, following SOLID and Layered Architecture already gets us a lot of the way toward this kind of modularity.

Technical Debt = Descent Obstruction

Technical debt
  = descent obstruction

The intuition is that technical debt can be read as a failure of futures to glue.

local tests pass.
local reviews pass.
the AI proposal looks reasonable.
then integration breaks.

SFT does not want to stop at "the design is bad."
It wants to record the failure as an obstruction.

DescentFailure:
  missing interface invariant

Witness:
  Pricing returns a discounted total,
  but Checkout treats it as a tax-included final charge.

Now technical debt is no longer just a feeling.

Each team-local change looks reasonable, but the whole system cannot combine them into a valid global future.
The reason is that the boundary rule that should have been preserved was never defined.

That is the role of the Descent Obstruction Theorem.

Review = Minimal Decision-Preserving Envelope

Review
  = minimal decision-preserving envelope

A ForecastCone can be large.
A reviewer cannot look at every future path.
But a diff alone is often too small.

Suppose an AI agent produces a PR like this:

if coupon_code.present?
  total = total - discount
end

The diff is small.
But the reviewer does not only care about these three lines.

Will this add an unobserved branch to the refund path?
Will usage limits collide with retry behavior?
Is the tax boundary between Pricing and Checkout still undefined?

What we need is not the whole ForecastCone, but the part needed for a review decision.
SFT calls this a ConsequenceEnvelope.

The goal for review tooling is not to show everything.
It is to show the future-relevant differences needed for the decision, no more and no less.

Governance = Desired-Cone-Preserving Obstruction Cutting

Governance
  = desired-cone-preserving obstruction cutting

When a risky future appears, the simplest response is to add another rule.

Anything coupon-related must be reviewed by a senior engineer.

That is a guardrail.
But it is often heavy, and it may not say what future it is actually closing.

The kind of governance SFT wants is more specific: close bad futures while preserving desired ones.

Introduce separate DiscountedTotal and FinalCharge types across the Pricing / Checkout boundary.
Make coupon usage updates idempotent.
Require coupon invariant checks when touching the refund path.
Guide AI agents away from ad hoc discount branches under checkout and toward policy objects.

We want to close the future where discount logic spreads across checkout.
We still want to preserve the future where coupon policy can evolve independently.

That difference is what the Governance Synthesis Theorem is about.
It is not just about adding guardrails. It is about shaping the field.

Learning = Closed-Loop Boundary-Explicit Fixed Point

Learning
  = closed-loop boundary-explicit fixed point

SFT is not a theory where we compute one ForecastCone and stop.

Predicted future paths are compared with actual PRs, incidents, review comments, CI failures, and runtime observations.
When the forecast is wrong, that is not just a failure.
It becomes evidence for updating the model.

Was the field estimate too coarse?
Was the observation boundary too narrow?
Did the policy model fail to represent actual review behavior?
Should the unknown remainder have been made explicit?

As this closed loop progresses, an SFT workbench becomes more than an analyzer.
It becomes a system for continuously calibrating the field model of software evolution.

Attractor Engineering and ArchSig

This grand theorem becomes practical only when it connects to AAT and ArchSig.

AAT gives us a local theory for reading what a change preserves and what it breaks.
ArchSig gives us a signature layer for observing preservation and breakage from repositories, PRs, reviews, CI, and incidents.
SFT uses those observations to compute reachable futures and connect them to governance and learning.

AAT
  -> local laws / invariants / obstruction witnesses

ArchSig
  -> observed signatures / measured axes / evidence boundaries

SFT
  -> ForecastCone / ConsequenceEnvelope / governance update

Attractor Engineering fits here as well.

A good architecture attracts good changes.
A bad architecture repeatedly makes the same shortcut look natural.

In SFT language, this means the shape of reachable futures changes.
Governance interventions close bad future paths, type boundaries make good local evolution more natural, and review rules make risky paths observable.

Attractor Engineering is the practice of shaping the ForecastCone.
ArchSig is a tool for observing that change.
SFT connects those observations back to the theorem family.

A Sketch of a Future Development Workflow

SFT is not trying to build a system that decides the future instead of developers.
It is trying to make a development environment where developers, AI agents, reviews, and CI can see the future opened by a change on the same map.

An ambiguous PRD arrives.
An AI agent quickly proposes an implementation.
At the same time, a workbench sketches the futures that change seems to open and shows only the differences needed for review.

PRD
  -> implementation candidates
  -> reachable future range
  -> review-relevant differences
  -> review / CI / governance
  -> observed outcome
  -> next forecast update

Before reading every line of the diff, the reviewer sees which futures look risky.
CI checks not only whether tests pass, but whether a risk we wanted to close is still present.
The AI agent prioritizes implementation candidates that open better futures instead of copying the nearest shortcut.

Actual PRs, incidents, and review comments then become evidence for the next forecast.

That is the development workflow SFT is aiming toward.

Impact on Computer Science and Software Engineering

Lehman raised a core question of software evolution: long-lived software keeps changing as it adapts to its environment, and that change tends to increase complexity.

SFT revisits that question in the age of AI-assisted development.

Software engineering has long developed design and architecture theory around human cognition.

That makes sense.
Software is complex, and if humans cannot read it, they cannot maintain it.
So we developed ideas such as separation of concerns, information hiding, cohesion, coupling, layering, Clean Architecture, and bounded contexts to make complexity manageable for people.

That axis remains important.

But once AI coding agents enter the loop, the bottleneck shifts.
When code can be produced faster, the question is no longer only:

Can humans understand the current structure?

The next question is:

What futures does this structure make reachable?

A good design is not only one that makes the current code easier to read.
It is also one that makes good futures easier to reach and bad futures harder to reach.

From this point of view, architecture expands from human comprehensibility to future reachability.

Can this boundary glue future paths locally?
Which direction does this PR make the next change more likely to take?
Does this metric preserve distinctions that matter for future evolution?
Does this review rule close bad futures while preserving good ones?
Which gluing failure does this technical debt represent?

These questions already exist in practice.
They are just scattered across experience, intuition, review comments, incident memory, and organizational culture.

SFT tries to move them toward computable theory.

If this direction works, software engineering moves from:

techniques for making complexity understandable to humans

toward:

a science for observing, computing, and governing software evolution

The central concepts begin to look different:

architecture
  -> shape of reachable futures

modularity
  -> descent of future paths

technical debt
  -> obstruction to future gluing

review
  -> minimal consequence envelope

metrics
  -> cone-conservative observations

governance
  -> support transformation

refactoring
  -> evolutionary invariance

AI coordination
  -> agentic confluence

lifecycle
  -> bifurcation of repair feasibility

Lean Formalization

We are also formalizing this research program in Lean.

The point is to keep SFT vocabulary from remaining only a metaphor.

Terms such as field, ForecastCone, ConsequenceEnvelope, and governance update are being broken into small objects that can become records, types, and theorem packages.
The big research picture gradually becomes something we can touch formally.

Current formalization work includes:

SoftwareFieldEstimate
OperationSupport / StepRelation
ForecastCone / ClockedForecastCone
ConsequenceEnvelope
FieldUpdate

For example, ForecastCone is treated as a supported path within a finite horizon.
ClockedForecastCone introduces a shared clock and idle / stutter steps for descent.
ConsequenceEnvelope treats review output as a projection from a cone family.

The final grand theorem is also being assembled from components: descent, obstruction, review, governance, calibration, and agentic confluence.
Under those explicit components, the Lean-side assembly has the shape:

computably governed
  or
typed boundary failure

This formalization makes SFT a research program where we can track what is a theorem, what belongs to modeling, and what remains on the tooling or empirical side.

Closing

ForecastCone is not a tool for predicting the future.

It is a way to make reachable software futures computable under explicit modeling boundaries, operation support, policies, observation boundaries, and horizons.

SFT's bet is that we can rebuild central software engineering concepts from there.

Architecture is not only the shape of present code.
It is the shape of reachable futures.

Architecture is not only the shape of the code we have now.

It is also the shape of the futures that codebase makes reachable.

Gotanda Style: Do AI Agents Really Need Meetings?

Hiroyuki Nakahata — Mon, 11 May 2026 14:28:47 +0000

TL;DR

Once you start running multiple AI coding agents, coordination eventually becomes its own bottleneck.

For long-running maintenance workflows, the cost of conversations, context, and tokens starts to add up.

We call the pattern Gotanda Style: agents do not talk to each other directly. Instead, they leave small structured signals in a shared environment. Other agents read those signals later.

This is a lighter introduction to a workflow we use on a roughly 200,000-line Python repository: Sentry alerts become shared signals, recurring patterns become GitHub issues, and coding agents turn the right ones into small, reviewable PRs.

Are we making AI agents attend too many meetings?

If you are building with AI coding agents, you will probably hit the coordination problem sooner or later.

When people design a multi-agent system, the first idea is often: "let the agents talk to each other."

A Planner discusses the plan. A Researcher investigates. A Coder implements. A Reviewer comments. A Supervisor keeps the whole thing on track.

That feels natural. It also works pretty well for small tasks.

But when you try to run a large system for a long time, a different problem appears.

More agents create more conversations. More conversations create more context. More context creates more token usage.

Eventually, the agents can spend too much of their budget reading each other's messages instead of solving the actual problem.

It starts to look a little like a human organization where work slows down because every decision turns into a meeting.

So we started with a simple question:

AI agents don't need meetings.

Or more precisely: not every kind of coordination needs to be a conversation.

Leave structured traces instead of chatting

In the pattern we are trying, agents do not talk to each other directly.

Instead, each agent writes down what it observed as a small signal in a shared environment.

Another agent can read that signal later.

Agents do not talk to each other.
They leave traces in a shared environment.
Other agents read those traces later.

This kind of coordination is called stigmergy.

The word sounds academic, but the idea is simple: coordinate through the environment.

We call the shared signals "pheromones" internally. The name is a little weird, but the implementation is just a structured record:

(scope, location, worker, strength, half_life, metadata)

For example, if a production error happens in a file, a Sentry worker might leave a signal like this:

{
  "scope": "file",
  "location": "app/services/invoices.py",
  "worker": "sentry-worker",
  "strength": 2.0,
  "half_life_days": 14,
  "metadata": {
    "category": "runtime_error",
    "environment": "production"
  }
}

This is not a long chat log.

It is small, structured, and easy to aggregate later.

The actual maintenance flow

In a simplified form, the workflow looks like this:

Sentry worker   ----+
Datadog worker  ----+-->  Pheromone field  -->  Refactor worker  -->  GitHub Issue  -->  Code worker  -->  Pull Request
Quality worker  ----+

Each worker looks at the codebase or production system from a different angle.

The Sentry worker watches production errors. The Datadog worker watches performance regressions. The Quality worker looks for test gaps and weakening module boundaries.

But they do not immediately create a pile of issues.

First, they leave signals in the shared environment.

If several workers point to the same location, that location becomes a hotspot.

If a weak signal happens only once, it fades over time.

If something was previously reviewed and marked "not worth fixing right now," the system can leave a negative signal for that candidate too.

The Refactor worker reads those signals and decides what should become an issue, what should go to a human, and what is safe enough for automated implementation.

Only issues at the right size and clarity are passed to the Code worker and turned into pull requests.

The nice part is that coordination cost moves from conversation to state updates.

When we add a new worker, we mainly define what kind of signal it writes.

A Security worker can write security signals. A Performance worker can write performance signals.

The Integrator can read all of them as part of the same shared environment.

That means production errors, slow endpoints, test gaps, and design drift do not all need to become all-hands agent meetings.

The small trick: zero does not always mean nothing

If you only add signals together, you can accidentally hide useful information.

Imagine one file has these two signals:

sentry-worker: +2.0
refactor-worker: -2.0

The simple sum is zero.

But that is not the same as a file with no signals at all.

It means something more interesting: "production is complaining about this area, but we also have a previous decision saying not to chase it right now."

That is a different situation from silence.

So the system should not only ask, "what is the final score?"

It should also ask:

How much positive signal is here?
How much negative signal is here?
Are different workers disagreeing?
Is this a quiet area, or a contested one?

That small distinction changes the behavior of the whole maintenance loop.

A quiet area can be ignored for now.

A strongly positive area might become an implementation issue.

A strongly negative area might stay suppressed.

But a contested area probably needs a human to look at the tradeoff.

That is the kind of detail that makes this feel less like "agents throwing tasks into a queue" and more like a maintenance system with memory.

The faster AI writes code, the more maintenance matters

AI coding agents are making it faster to write code.

But if code is written twice as fast, the maintenance load grows too.

More code reaches production. More changes need monitoring, debugging, testing, and refactoring.

It is like doubling the speed of a car. Speed is great, but only if the tires, brakes, suspension, and safety systems can keep up.

So in AI-driven development, "write code faster" is not enough.

This is not just a thought experiment for us.

We are using this pattern to maintain a Python repository with roughly 200,000 lines of code.

The loop from Sentry alert to pheromone deposit to GitHub issue to improvement pull request is already running.

That does not mean we try to automate everything.

Humans still step in when a fix needs architectural judgment, the cause is unclear, the blast radius is large, or an automated pull request needs review.

As we give AI agents more work, I do not think the human role disappears. It moves toward higher-level judgment and boundary design.

As a practice of attractor engineering

Zoom out a bit, and the whole codebase becomes part of the prompt for AI.

If the codebase has good structure, AI is more likely to follow that structure.

If the codebase has bad structure, AI is also more likely to treat that as the natural pattern.

That is why we care about preventing AI-generated changes from pushing the codebase toward worse future changes.

In that sense, this pattern is also a practice of attractor engineering.

I wrote more about that idea here:

Hiroyuki Nakahata

May 9

Attractor Engineering: Seeing Software Development as Field Dynamics

#softwareengineering #architecture #ai #computerscience

24 min read

Before the codebase drifts toward a bad attractor, we observe it, leave signals, and correct the trajectory through issues and pull requests.

This is not just about making AI coding agents go faster.

It is about keeping the codebase itself in a better shape for the next AI-generated change.

When stigmergic multi-agent coordination works, and when it does not

This pattern is not always better than conversational multi-agent design.

Direct agent conversation can be the right tool when:

The task is small
There are only a few agents
The context is short-lived
The goal is exploration or brainstorming
It is faster to reach agreement in the moment

Leaving traces in a shared environment tends to work better when:

The workflow runs for a long time
Signals arrive asynchronously
Multiple tools observe the same codebase
You want weak signals to accumulate over time
You want to add agents without increasing communication traffic too much

So this is not a universal architecture.

It is a coordination pattern for long-running maintenance work.

Wrap-up

In AI multi-agent systems, conversation feels like the natural coordination model.

But in long-running maintenance workflows, conversation itself can become the cost.

Does AI agent coordination really need to be a conversation?

As one experiment around that question, we call this pattern Gotanda Style.

I wrote a deeper version on Hashnode covering the design background, pheromone handling, and the production workflow from Sentry alerts to issues and pull requests:

https://blog.iroha1203.dev/ai-agents-don-t-need-meetings-gotanda-style-for-stigmergic-software-maintenance

How are you coordinating AI agents today? Are they talking to each other, or are they coordinating through shared memory, queues, databases, event logs, or some other environment?

When Lean Proved My Durability Definition Too Easily

Hiroyuki Nakahata — Sun, 10 May 2026 12:34:42 +0000

TL;DR

I tried to formalize a small ACID-like model in Lean 4.

Consistency became invariant preservation.
Isolation became a deliberately strong commutation law.
Durability exposed that my model had no persistence boundary.

The result was not a proof that databases are correct.
It was a reminder that every design claim depends on what the model can actually see.

The suspicious part was not that Lean failed to prove durability.

The suspicious part was that Lean proved it with almost no assumptions.

ACID is familiar enough that it is easy to stop thinking about it.

Atomicity. Consistency. Isolation. Durability.

In ordinary database terms, the rough meanings are:

Atomicity
  A transaction is all-or-nothing. It commits as a unit or has no effect.

Consistency
  A transaction takes the database from one valid state to another valid state.

Isolation
  Concurrent transactions behave as if they were controlled by some serial order.

Durability
  Once a transaction commits, its effect survives failures and recovery.

Most engineers learn these words through examples: bank transfers, constraints, concurrent transactions, crashes, logs, commits, and recovery.

But I wanted to ask a slightly different question:

What kind of structure is ACID preserving?

So I tried to write a small ACID-like model in Lean 4.

The result was not a proof that real databases are correct.

That is the part worth sharing.

A Minimal Model

Start with the smallest model that still has something architectural in it.

There is a state space S. There are transactions. Each transaction acts on the state. There is also an invariant, a predicate that says which states are valid.

This is not a formalization of real database ACID.

It is a deliberately lossy projection: keep the state-transformer shape, and drop many operational details.

In simplified Lean-shaped notation, the model looks like this:

abbrev Endo (S : Type u) := S -> S

structure Model (S : Type u) where
  Txn   : Type v
  apply : Txn -> Endo S
  inv   : S -> Prop

This is intentionally abstract.

S might be a relational database state. It might be an event-sourced aggregate. It might be a key-value store, an in-memory domain model, or a deliberately simplified toy system.

The point is not to model every detail of a database. The point is to ask what can already be said if we only know this:

transaction = operation on state
invariant   = property we want valid states to preserve

This small model already gives a useful reading of some ACID-shaped claims.

Histories Are Composition

Transactions rarely appear alone. They appear in histories.

A history is a list of transactions. Replaying a history means composing the corresponding state transformations.

def Model.replay (M : Model S) : List M.Txn -> Endo S
  | []      => id
  | t :: hs => fun s => M.replay hs (M.apply t s)

The empty history is the identity function. A non-empty history applies the first transaction, then replays the rest.

The important lemma is that replaying appended histories corresponds to composing their replays:

theorem replay_append
    (h1 h2 : List M.Txn) :
    M.replay (h1 ++ h2) = fun s => M.replay h2 (M.replay h1 s)

In plain English:

append histories
  corresponds to
compose state transformations

This is already algebraic. The list of transactions has a monoid structure under append. State endomorphisms have a monoid structure under composition. Replay connects the two.

In less mathematical terms, replay is the bridge between a log and the effect that log has on the system.

This is the first useful reframing:

a transaction log is not just a list;
it is a way to build larger state transformations from smaller ones.

Consistency as Invariant Preservation

For this model, the part of ACID consistency we keep is invariant preservation: a transaction should take a valid state to another valid state.

def PreservesInvariant (M : Model S) : Prop :=
  forall t : M.Txn, forall s : S,
    M.inv s -> M.inv (M.apply t s)

This is invariant preservation. The set of valid states is closed under every transaction.

valid state
  -- transaction -->
valid state

Once written this way, a small theorem becomes immediate:

theorem preservesInvariant_comp
    (hC : PreservesInvariant M)
    (t1 t2 : M.Txn)
    (s : S)
    (hs : M.inv s) :
    M.inv (M.apply t2 (M.apply t1 s))

If t1 preserves the invariant and t2 preserves the invariant, then their composition preserves the invariant.

The same idea extends from two transactions to any history:

theorem preservesInvariant_replay
    (hC : PreservesInvariant M) :
    forall h : List M.Txn, forall s : S,
      M.inv s -> M.inv (M.replay h s)

This is the cleanest part of the story. In this projection, consistency becomes:

the invariant survives every selected operation.

That sentence is also the bridge to software architecture, but we will come back to that at the end.

An Algebraic Shadow of Atomicity

Atomicity is trickier.

In this model, I cannot express all-or-nothing execution.

There is no partial execution, no abort, no crash, and no visibility boundary.

The closest algebraic property I can write is closure under sequencing:

def ClosedUnderSequence (M : Model S) : Prop :=
  forall t1 t2 : M.Txn,
    exists t3 : M.Txn,
      M.apply t3 = fun s => M.apply t2 (M.apply t1 s)

This says that if two selected operations are executed in sequence, their combined effect can be represented as one selected operation.

transaction followed by transaction
  can be treated as
one transaction

That is not database atomicity. It is only an atomicity-shaped shadow.

So this definition needs a boundary:

This is algebraic atomicity as closure of selected operations.
It is not a full crash/failure semantics for transactions.

This boundary prevents a small theorem from being advertised as a larger theorem.

Isolation as Commutation, Also With a Warning

Isolation is also subtle.

A common intuition is that concurrent transactions should behave as if they had run one at a time. In database terms, serializability asks whether a concurrent execution is equivalent to some serial order.

Commutation asks for something stronger: the two serial orders are indistinguishable at the level of final state.

def CommutesOnValidStates (M : Model S) : Prop :=
  forall t1 t2 : M.Txn, forall s : S,
    M.inv s ->
      M.apply t2 (M.apply t1 s)
        =
      M.apply t1 (M.apply t2 s)

This says that on valid states, swapping the order of two selected operations does not change the result.

t1 then t2
  =
t2 then t1

This is mathematically clean, but it is stronger than serializability. It removes order from the observable final state rather than merely finding some serial order.

So this definition also needs a boundary:

This definition captures a strong commutation-style isolation property.
It is not a taxonomy of real-world isolation levels.

The formal model is valuable because it makes the approximation visible. Without it, it is easy to slide from "this resembles isolation" to "this is isolation."

Lean does not let that slide happen quietly.

Durability Exposed a Missing Boundary

Durability was the most interesting part.

My first attempt was to define durability as monotonicity of history. If one history is a prefix of another, then the longer history should replay as the shorter history followed by some suffix.

In pseudocode:

def WrongDurabilityAttempt (M : Model S) : Prop :=
  forall h1 h2 : List M.Txn,
    Prefix h1 h2 ->
      exists k : List M.Txn,
        M.replay h2 = fun s => M.replay k (M.replay h1 s)

This sounds plausible.

If h1 is already committed and h2 extends it, then h2 should contain h1 as a stable prefix. The past should not be rewritten.

But then something happened:

the theorem was provable with no real assumptions.

That was the moment the model started to teach me something.

Why?

Because if h1 is a prefix of h2, then by definition there is some suffix k such that:

h2 = h1 ++ k

And replay_append already gives:

replay (h1 ++ k) = replay k . replay h1

So the attempted durability theorem follows almost for free.

At first, that feels like success: the theorem was proved, the code type-checked, and the definition seemed to behave.

But that was the warning.

This was the bug: I had not defined durability.

I had defined a replay decomposition property of append-only histories.

If a property that should depend on storage, crashes, and recovery can be proved from list concatenation alone, then the property is not talking about storage, crashes, or recovery.

Durability is not just "the log has a prefix." It is a recovery guarantee under an explicit failure model.

Committed effects should survive the crashes and recoveries the system promises to handle.

A pure state-transition model does not contain storage.

It does not contain crashes.

It does not contain a recovery function.

So it cannot express the full property.

To talk about durability seriously, the model needs another layer:

volatile state
persistent state
write
crash
recover

Only after adding that layer can we ask for a non-trivial law such as:

recover after write preserves the committed effect

This was the most valuable lesson from the exercise.

Lean did not merely help prove a theorem. It helped detect that a proposed definition was too weak to express the intended claim.

In other words:

Lean did not reject the definition.
It accepted it so easily that the definition became suspicious.

What Lean Actually Gave Me

The result was not:

ACID has been proved correct.

That would be far too strong.

What Lean gave me was a way to notice when a claim had silently moved outside its model.

Within a pure state-transition model:

Consistency-shaped claims can be read as invariant preservation.
The atomicity-shaped fragment becomes closure under sequencing.
The isolation-shaped fragment becomes commutation on valid states.
Durability cannot be expressed without persistence, recovery, and a fault model.

For software engineering, this discipline matters more than the notation.

Many architecture discussions fail because claims move between levels without being noticed.

For example:

"We use Event Sourcing"
  quietly becomes
"we can always replay and recover correctly."

"We use Clean Architecture"
  quietly becomes
"dependencies cannot violate our boundary."

"We have tests"
  quietly becomes
"the behavior is preserved."

Each of those moves may be valid under additional assumptions. But the assumptions need to be stated.

From ACID to Architecture

The ACID example suggests a more general way to read software design.

A design rule is not just a slogan.

It is a claim that some operation should preserve some invariant.

In ACID, the operations were transactions. One invariant was database consistency.

In software architecture, the same pattern appears in a less obvious form.

ApplicationService -> SqlPaymentRepository

Suppose the intended architecture says that application code should depend on a payment port, not on the SQL implementation directly.

Then the issue is not simply that the design "looks bad."

There is an invariant:

application logic depends on declared abstractions,
not on infrastructure details directly

There is an operation:

a feature addition or refactoring introduced a new dependency edge

And there is a witness:

the concrete edge ApplicationService -> SqlPaymentRepository

That is the same shape as the ACID model:

operation acts on a structure
invariant is expected to survive
failure should have a concrete witness

Here, the "state" is not a database state. It is a dependency graph.

The operation is not a transaction. It is a code change that adds or removes edges.

The invariant is not a database constraint. It is an architectural rule about allowed dependencies.

The witness is not a bad row. It is a forbidden edge.

I use the name Algebraic Architecture Theory (AAT) for this broader lens, but the name matters less than the discipline: state the operation, the invariant, the witness, and the boundary.

The important word is not "algebra" for its own sake. The important word is invariant.

When we say a design is good, we should be able to ask:

Which invariant is being preserved?
By which operation?
Under which observation boundary?
If it fails, what is the witness?

The same question can be asked for dependency direction, abstraction boundaries, substitutability, replay laws, compensation laws, and failure locality.

When an invariant fails, we should not merely say "the design is bad." We should identify the concrete witness: a forbidden dependency edge, a cycle, an abstraction leak, an observation mismatch, or a failed compensation case.

Different invariants can fail in different ways, and each failure should have a witness.

The lesson from ACID carries over:

do not ask whether the architecture is "good" in general;
ask which invariants are preserved, which witnesses remain,
and which axes were not measured.

Conclusion

ACID was not the destination.

It was a small, familiar example showing that software design can be read as invariant preservation under operations, with explicit witnesses when preservation fails.

Lean did not turn a simplified model into a real database.

It did something more useful.

It showed that a definition can be wrong not because Lean rejects it, but because Lean accepts it for the wrong reason.

In that sense, formalization is not only a tool for proving.

It is a tool for discovering what your words were secretly assuming.

That is the habit I want to bring from formal methods into everyday architecture work.

Not every design discussion needs a proof assistant.

But every serious design claim benefits from the same discipline:

name the operation;
name the invariant;
name the witness;
name the boundary.

The working Lean repository for this line of thought is here:

https://github.com/iroha1203/AlgebraicArchitectureTheoryV2

AI does not only generate code faster. It changes the distribution of future changes. This post introduces Attractor Engineering: designing where software changes tend to converge.

Hiroyuki Nakahata — Sat, 09 May 2026 11:33:16 +0000

Hiroyuki Nakahata

May 9

Attractor Engineering: Seeing Software Development as Field Dynamics

#softwareengineering #architecture #ai #computerscience

24 min read

Attractor Engineering: Seeing Software Development as Field Dynamics

Hiroyuki Nakahata — Sat, 09 May 2026 11:25:16 +0000

TL;DR

A codebase can be read as a field that attracts future changes, and a pull request can be read as a force applied to that field.

A good field makes good changes easier to make. A bad field repeatedly makes bad shortcuts look natural. In an era where AI can produce PRs quickly, this attraction becomes stronger.

I call the practice of designing where future changes are pulled Attractor Engineering.

CI/CD, tests, reviews, and harnesses can be read as dissipative systems: they remove unwanted force and shape the trajectory.

ArchSig, or Architecture Signature, is a tool for observing that trajectory along multiple axes.

The first half of this article is written for practitioners: it explains the intuition in terms of codebases, PRs, review, CI, and AI-assisted development. The second half is more mathematical: it connects the same intuition to AAT, Architecture Signature, Lean formalization, and finite counterexamples.

The First Discovery

The starting point was a simple thought experiment.

What if we look at software architecture not only as a set of directories, design rules, or conventions, but as an algebraic structure?

From that point of view, everyday changes such as feature additions, refactorings, splits, migrations, repairs, protections, deletions, and integrations become operations acting on the structure we call architecture.

current codebase
  + feature addition
  + refactoring
  + review fix
  + migration
  + repair
  -> next codebase

If we take one more step, we can ask: if these operations are not applied once, but repeated dozens or hundreds of times, can the whole development process be read as a kind of dynamics?

Each individual PR is small.

But after enough PRs, the codebase gradually moves in some direction.

When a good structure already exists, the next change tends to fit into a good place.

When a bad structure exists, a locally natural change tends to take the same bad shortcut again.

Can we treat "where changes tend to go" as something we design?

I decided to call this way of thinking Attractor Engineering.

A Codebase Is a Field, and a PR Is a Force

The central interpretation is this:

codebase = a field that attracts changes
PR       = a force applied to that field
ArchSig  = an observer for the movement

A codebase is not a neutral space that passively receives future changes.

Existing names, types, responsibility boundaries, tests, directory structure, previous implementation examples, and review culture all shape which next change feels natural.

A PR is a force applied to that field. Each one may be small, but repeated PRs create a trajectory of change.

current codebase
  -> a PR is applied
  -> an architectural change is observed
  -> a trajectory of change emerges
  -> this becomes the next codebase

The important point is that a PR changes the codebase, and the changed codebase then changes what the next PR is likely to look like.

People and Systems Create the Field

This field is not created only by engineers.

Product managers, product owners, engineers, reviewers, AI agents, CI, tests, design documents, coding standards, and existing examples all participate in it.

Everyone and everything involved in development affects which changes become likely next.

Participant / mechanism	Effect on the field
Product manager	Decides which values and demands are repeatedly injected into the system.
Product owner	Shapes PRs through requirement granularity, priorities, and acceptance criteria.
Engineer / architect	Creates paths for change through boundaries, abstractions, standard patterns, and reference implementations.
Reviewer	Pushes back bad force and redirects it toward better directions.
CI / tests / types	Rejects, weakens, and narrows inappropriate force.
AI agent	Reads the existing field and quickly proposes changes.

The way requirements are sliced, prioritized, scheduled, and accepted changes how later PRs are produced. Even people who do not write code apply indirect force to the field of the codebase.

This becomes especially important in AI-assisted development. Vague requirements can quickly become vague PRs. If boundaries and non-goals are clear, an AI system is more likely to produce useful changes within those boundaries.

What Changes in AI-Assisted Development

The essence of AI-assisted development is not simply that code can be written faster.

The more important change is that the distribution of selected change operations changes.

An AI system reads existing code, neighboring files, names, types, tests, previous implementation examples, READMEs, and design documents, and then generates the next proposed change.

In other words, the whole codebase becomes input context for the AI.

the codebase becomes input context for AI
  -> AI proposes a change
  -> the proposal becomes a PR
  -> review / CI / merge process handles it
  -> the codebase is updated
  -> the next input context changes

If a good reference implementation is nearby, the AI is likely to imitate it.

If a bad shortcut already exists, the AI is also likely to treat it as a natural option.

In this sense, AI rapidly reproduces the local style already present in the field. That is why, in the AI era, what matters is not only the capability of an individual AI agent. The design of the field in which the AI participates matters just as much.

What Is an Attractor?

When a codebase contains a huge common module, an overly convenient helper, or an ambiguous service, changes tend to be pulled there.

Conversely, when good responsibility boundaries and clear implementation examples exist, the next change tends to follow them.

This destination toward which changes are pulled is what I call an attractor. When something moves repeatedly, it often tends to approach certain places or states.

The surrounding region from which things are likely to fall into that attractor is what I call a basin.

Technical debt can be read as a bad basin.

Once a codebase falls into it, locally natural changes keep adding to the same place, and the cost of refactoring out of it grows higher and higher.

The important point is that attractors can be good or bad.

A good attractor pulls in good changes.

A bad attractor makes bad shortcuts get selected again and again.

What Is Attractor Engineering?

Attractor Engineering is the idea that we should deliberately design these attractors.

Its target is not just the codebase.

It includes the whole development organization: product managers, product owners, engineers, reviewers, AI agents, CI/CD, tests, design documents, and coding standards.

The goal is not only to block bad changes from the outside. The goal is to create a field where good changes are naturally easier to select.

Part of Attractor Engineering	What it shapes	Examples
Create the field	Which changes feel natural to propose.	Requirements, priorities, design boundaries, types, APIs, examples, templates.
Dissipate bad force	Which proposed changes are rejected, weakened, or redirected.	Harnesses, CI, tests, reviews, PR granularity.
Observe the trajectory	How architectural movement becomes visible over time.	ArchSig, architecture features, drift reports.

Attractor Engineering is an integrated design theory for the era of AI-assisted development. It treats the entire development organization as part of the system.

Harness Engineering as a Dissipative System

We cannot simply take changes produced by AI and put them directly into the codebase.

Harnesses, CI, tests, type checking, static analysis, and review divide proposed changes into "accept", "fix and check again", and "do not merge".

In Attractor Engineering, this behavior can be read as dissipation.

Dissipation is the mechanism that removes unwanted components of the force entering the field.

If dissipation is too weak, the fast change force produced by AI enters the codebase directly. If it is too strong, nothing moves. A good harness weakens the force that increases debt while preserving the force that moves the product forward.

In this view, CI/CD is not merely a checklist. It is more like brakes, rails, signals, and safety equipment that convert fast PR generation into safe productivity.

What matters in AI-assisted development is not only making the engine stronger.

It is also preparing the field and the dissipative system that can receive a stronger engine.

What ArchSig Observes

To design the field, we need to observe what is happening.

That is the role of ArchSig.

ArchSig is short for Architecture Signature.

In my repository, I use it to mean an observation framework for reading changes in a codebase or PR along multiple axes. Dependencies, boundaries, abstractions, runtime exposure, semantic drift, and test observability are not collapsed into a single score. They are treated as multiple features.

ArchSig is an observer for seeing which direction a PR moves the architecture.

For example, we may observe axes like these:

Axis	What we want to observe
Static dependencies	Dependency direction and violations of forbidden dependencies.
Boundary rules	Connections that cross boundaries or bypass rules.
Abstraction leakage	Concrete dependencies that jump over abstractions.
Semantic drift	Whether responsibilities or meanings have shifted away from what was intended.
Test observability	Whether the change can be observed through tests.
Per-PR change	How each axis moves in a single PR.

The important point is that we do not compress good and bad into one score.

What we want to know is which axes got worse, which axes improved, and what kind of force each change applies.

PR
  -> observe change with ArchSig
  -> observe the trajectory of change
  -> see whether it is moving toward a good or bad region

ArchSig becomes an observer for the AI PR era.

Are AI-generated changes moving toward good attractors?

Are they falling into a pool of technical debt?

Is the harness dissipating enough bad force?

ArchSig gives us shared language for discussing those questions.

PRs Become More Important, Not Less

When AI reduces the cost of generating code, it may look as if PRs become less important.

From a dynamical systems viewpoint, the opposite is true.

A PR is not just a work unit.

A PR has the following roles:

It cuts continuous change into observable units.
It lets us separate the directions in which a change acts.
It embeds the dissipative process of review, CI, and approval.
It creates a boundary for rollback and reversibility.
It creates a unit for decision-making and discussion.

What AI lowers is mainly the cost of producing a PR.

But the value of PRs as units of observation, decomposition, dissipation, reversibility, and decision-making increases. In the AI era, PRs do not become unnecessary. They become more important as units for observing and controlling architectural movement.

Future Development Organizations

In future development organizations, the central problem will not be only how fast we can write code. It will be how to design a field that can safely receive that speed.

A fast train cannot run safely just because it has a powerful motor.

It needs rails, brakes, signals, safety equipment, and operations control.

Software development is similar. AI is a powerful motor, but by itself it can create semantic drift, responsibility drift, degradation of design properties we wanted to preserve, merge confusion, and flow toward technical debt.

What we need is a field with properties like these:

Small and observable PRs.
Fast feedback.
Reliable CI.
A useful type system.
Architecture tests.
Carefully selected reference implementations.
Isolation of legacy code.
Clear demands, requirements, and design boundaries.
Human-designed boundaries for value and acceptance criteria.

The safest AI coding environment is not the one with the strongest external harness. It is the one where good changes are natural, easy to imitate, observable, and less likely to fall into bad shortcuts.

Summary So Far

The success or failure of AI-assisted development is not determined only by how fast AI can write code.

The direction of the next PR changes depending on the field created by the codebase, requirements, design boundaries, reference implementations, review, CI/CD, and ArchSig.

A good field attracts good changes. A bad field repeatedly makes bad changes look natural. That is why architecture design in the AI era becomes the design of where future changes are attracted.

So far, this has been Attractor Engineering in practical engineering language. In the second half, I translate the same intuition into the language of AAT, Algebraic Architecture Theory, and dynamical systems.

From Here, in Mathematical Language

The rest of this article uses more mathematical formulation. If you only want the practical view first, it is fine to skip to the conclusion.

Around AI development, there are many heuristics: "this prompt worked", "this workflow made us faster", and so on. These heuristics are valuable. But by themselves, they make it hard to separate why something worked, how far it generalizes, and under what conditions it breaks.

So I decompose the flow: a change is selected, becomes a PR, passes review / CI, is merged, and then the updated codebase changes the distribution of future changes. By separating state, operation, observation, invariant, obstruction witness, and proof obligation, we can turn heuristics into something easier to test.

A Short Introduction to AAT

The background theory for this discussion is AAT, or Algebraic Architecture Theory. Here I introduce only the minimal vocabulary needed for the rest of the article.

The Lean snippets below are excerpts from implemented APIs, adjusted for readability. Namespaces, imports, and some proof bodies are omitted.

AAT treats software development not merely as a sequence of code changes, but as a theory of architectural extension, decomposition, repair, and composition.

Its central proposition does not appear in Lean as one large equation. It appears as packages that combine operations and proof obligations.

structure OperationProofObligation (State : Type u) (Witness : Type v) where
  kind : ArchitectureOperationKind
  obligation : ProofObligation State Witness
  precondition : Prop
  nonConclusion : Prop

Operations are first classified as an operation catalog on the Lean side.

inductive ArchitectureOperationKind where
  | compose
  | refine
  | abstract
  | replace
  | split
  | merge
  | isolate
  | protect
  | migrate
  | reverse
  | contract
  | repair
  | synthesize
  deriving DecidableEq, Repr

The important point is that names such as split or repair prove nothing by themselves. An operation kind is a classification for theorem packages. Claims about preservation, improvement, or repair must be stated separately as proof obligations.

From this viewpoint, a design review is not only the question "is this design good or bad?"

- Is the existing structure embedded after extension?
- Can the new feature be split out from the existing structure?
- Do interactions pass through declared interfaces?
- Which invariants are preserved, and which invariants were broken?
- If a split is not possible, which obstruction witness blocks it?

The smallest object in AAT is ArchitectureCore.

structure ArchitectureCore (C : Type u) (A : Type v)
    (StaticObs : Type w) (SemanticExpr : Type q)
    (SemanticObs : Type r) where
  flatness :
    ArchitectureFlatnessModel C A StaticObs SemanticExpr SemanticObs
  staticUniverse : ComponentUniverse flatness.static
  componentDecidableEq : DecidableEq C
  staticEdgeDecidable : DecidableRel flatness.static.edge
  runtimeEdgeDecidable : DecidableRel flatness.runtime.edge
  boundaryPolicyDecidable : DecidableRel flatness.boundaryAllowed
  abstractionPolicyDecidable : DecidableRel flatness.abstractionAllowed
  runtimeRole : C -> C -> RuntimeDependencyRole
  semanticRequiredDecidable :
    ∀ d : RequiredDiagram SemanticExpr,
      Decidable (flatness.requiredSemantic d)

Here it is important that ArchitectureCore is not the whole real-world codebase itself. It is a finite or bounded object extracted from code, specifications, reviews, and operational observations so that the theory can handle it.

Feature addition is read as an operation that extends an existing architecture into a larger one while preserving the existing architecture.

ExistingCore X
  -> ExtendedArchitecture X'
  -> FeatureView F

In a good feature extension, the existing core is preserved inside the extension, the feature view can be extracted in an explainable way, and interactions from the feature to the core pass through declared interfaces. Conversely, hidden dependencies, boundary policy violations, abstraction leakage, runtime exposure, and semantic mismatch are treated not as impressions, but as ObstructionWitness values.

To count, remove, preserve, or explicitly decline to conclude about these obstructions, AAT makes ProofObligation and Certificate explicit.

structure ProofObligation (State : Type u) (Witness : Type v) where
  formalUniverse : Prop
  requiredLaws : Prop
  invariantFamily : State -> Prop
  witnessUniverse : Witness -> Prop
  coverageAssumptions : Prop
  exactnessAssumptions : Prop
  operationPreconditions : Prop
  conclusion : Prop
  nonConclusions : Prop

An obligation is not discharged merely because it exists. It is discharged only when the visible assumptions imply the conclusion.

def AssumptionsHold (P : ProofObligation State Witness) : Prop :=
  P.formalUniverse ∧
  P.requiredLaws ∧
  P.coverageAssumptions ∧
  P.exactnessAssumptions ∧
  P.operationPreconditions

def Discharged (P : ProofObligation State Witness) : Prop :=
  AssumptionsHold P -> P.conclusion

The same is true for certificates. For example, in repair synthesis, if we say "there is no solution", solver failure alone is not enough. Only when a valid certificate exists do we use soundness to conclude that no satisfying architecture exists.

structure NoSolutionCertificate
    {State : Type u} {Constraint : Type c} (Certificate : Type v)
    (C : SynthesisConstraintSystem State Constraint)
    (cert : Certificate) where
  valid : Prop
  sound : valid -> NoArchitectureSatisfies C
  coverageAssumptions : Prop
  exactnessAssumptions : Prop
  nonConclusions : Prop

theorem sound_of_valid
    (pkg : NoSolutionCertificate Certificate C cert)
    (hValid : ValidNoSolutionCertificate pkg) :
    NoArchitectureSatisfies C

nonConclusions is not decoration. Even if a static split is proved, runtime flatness or semantic flatness does not automatically follow. Even if no obstruction is found in one observation universe, that does not imply there is no obstruction in every universe. Making this boundary explicit is necessary if we want to treat the theory as testable rather than as a collection of engineering anecdotes.

ArchitectureSignature is also not intended to collapse architecture quality into a single score. It is a multi-axis diagnosis for reading multiple invariant and obstruction families axis by axis.

structure ArchitectureSignatureV1 where
  core : ArchitectureSignatureV1Core
  weightedSccRisk : Option Nat
  projectionSoundnessViolation : Option Nat
  lspViolationCount : Option Nat
  nilpotencyIndex : Option Nat
  runtimePropagation : Option Nat
  relationComplexity : Option Nat
  empiricalChangeCost : Option Nat
  deriving DecidableEq, Repr

Some axes are Option Nat because an unmeasured value must not be treated as zero. none does not mean "no problem". It means "not measured in this universe / extractor / bridge".

theorem not_axisAvailableAndZero_of_axisValue_none
    {sig : ArchitectureSignatureV1} {axis : ArchitectureSignatureV1Axis}
    (hNone : axisValue sig axis = none) :
    ¬ axisAvailableAndZero sig axis

From this perspective, a signature is not a convenient bag of metrics. It is a multi-axis invariant relative to a law universe. For selected required law axes, there are also bridge theorems connecting lawfulness and zero signature axes.

theorem architectureLawful_iff_requiredSignatureAxesZero
    {C : Type u} {A : Type v} {Obs : Type w}
    (X : ArchitectureLawModel C A Obs)
    [DecidableEq C] [DecidableEq A] [DecidableEq Obs]
    [DecidableRel X.G.edge] [DecidableRel X.GA.edge]
    [DecidableRel X.boundaryAllowed]
    [DecidableRel X.abstractionAllowed] :
    ArchitectureLawful X ↔
      RequiredSignatureAxesZero (ArchitectureLawModel.signatureOf X)

AAT does not treat every claim at the same level. It separates definitions, proved theorem packages, bounded bridge theorems, tooling-side evidence, and empirical hypotheses. It also records which universe, observation, coverage, and exactness assumptions each claim is relative to.

The dynamics part below follows the same discipline. The important point is that AAT is not using mathematical vocabulary for atmosphere. It is trying to make the assumptions, conclusions, and non-conclusions part of the type-level structure.

So far, AAT gives us vocabulary for a single architectural state and operations acting on it.

But in AI-assisted development, the central issue is not only a single operation. Requirements, existing code, review, CI, and AI agents change which operation is likely to be selected next, and this selection is repeated many times.

So we need to view AAT operations not only as one-time proof targets, but also as transformations repeatedly selected over time. This is where a chaos-game-like reading enters.

Formalizing Attractor Dynamics

From here, I use AAT vocabulary to rewrite "field", "force", "dissipation", and "observation" in a more mathematical form.

This is not merely a metaphor that says "AI development is kind of like a chaos game". It is an attempt to place PR force, operation support, trajectory, and basin candidates on top of the AAT vocabulary of state, operation, invariant, obstruction, proof obligation, certificate, and signature.

At this stage, I should be careful: this is not a finished theorem of real-world software development. It is a way to organize phenomena that practitioners can feel, in a structure that may eventually support measurement and verification.

The minimal loop of the dynamics can be read as follows:

architecture field
  -> operation distribution
  -> accepted / rejected transitions
  -> signature trajectory
  -> updated architecture field

The position is that architecture quality is not only a property of a snapshot. It is also a property of the future operation distribution and the signature trajectory.

1. State, Operation, Observation

Let the architectural state be X_t.

Feature addition, repair, split, protection, migration, and refactoring are operations acting on that state.

X_{t+1} = op_t(X_t)

The operation op_t is not selected uniformly at random.

The current codebase, requirements, prompt, review policy, CI, design boundaries, and organizational judgment all change which operations are likely to be selected.

op_t ~ P(operation | X_t, control_t)

This probability expression is notation for the practical reading. The formal core of AAT is not a probability distribution. It is finite or bounded operation support, bounded scripts, accepted transition predicates, and explicit preservation assumptions.

In Lean, for example, operation support is represented not as a probability distribution, but as a finite list of candidate operations for each state.

structure FiniteOperationKernel
    (State : Type u) (OperationId : Type w) where
  support : State -> List OperationId
  coverageAssumptions : Prop
  weightSourceBoundary : Prop
  normalizationBoundary : Prop
  nonConclusions : Prop

Weights, normalization, and completeness of AI-generated proposals are not mixed into the theorem here. Boundaries such as weightSourceBoundary and normalizationBoundary record what is outside the formal claim, and the probabilistic reading remains outside that core.

Likewise, repeated operation sequences are first treated as bounded scripts.

structure BoundedOperationScript (OperationId : Type w) where
  operations : List OperationId
  operationFamily : OperationId -> Prop
  operationsInFamily :
    ∀ op, op ∈ operations -> operationFamily op
  coverageAssumptions : Prop
  nonConclusions : Prop

This boundary helps avoid confusing probabilistic interpretation with preservation claims over finite support.

Instead of observing the entire state directly, we map it into signature space through an observation function Obs.

sigma_t = Obs(X_t)

This sigma_t is the Architecture Signature.

It contains multi-axis observations such as dependency direction, boundaries, abstraction, runtime exposure, and semantic mismatch.

In Lean, even the observation itself is packaged. The package contains not only the observation function, but also coverage and non-conclusion boundaries.

structure SignatureObservation (State : Type u) (Sig : Type v) where
  observe : State -> Sig
  coverageAssumptions : Prop
  nonConclusions : Prop

When architectural evolution is mapped into observation space, we get a signature trajectory.

def SignatureTrajectory (O : SignatureObservation State Sig) :
    {X Y : State} -> ArchitectureEvolution State X Y -> List Sig
  | X, _, ArchitecturePath.nil _ => [O.observe X]
  | X, _, ArchitecturePath.cons _step rest =>
      O.observe X :: SignatureTrajectory O rest

A change moves the signature.

Delta_t = sigma_{t+1} - sigma_t

This Delta_t can be read as the force applied by the PR or operation.

However, not every axis admits simple subtraction. For numeric axes, we may read it as a signed delta. For other axes, we read it as a before / after comparison, the appearance of a witness, or a change in state classification.

2. PR Force Model

With this structure, a PR becomes more than a diff.

A PR can be read as a force applied to the codebase in the selected Architecture Signature space.

PRForce(PR) = sigma(after(PR)) - sigma(before(PR))

The word force here does not mean physical force. It means an observed change in signature, relative to which axes are observed and which differences are defined.

Delta sequences, like trajectories, are relative to finite paths in Lean.

def SignatureDeltaSequence
    (O : SignatureObservation State Sig) (D : SignatureDelta Sig Delta) :
    {X Y : State} -> ArchitectureEvolution State X Y -> List Delta
  | _, _, ArchitecturePath.nil _ => []
  | X, _, ArchitecturePath.cons (Y := Y) _step rest =>
      D.between (O.observe X) (O.observe Y) ::
        SignatureDeltaSequence O D rest

For selected additive deltas, the sum of step deltas agrees with the endpoint delta. This is proved as a theorem.

theorem netSignatureDelta_telescopes [Zero Delta] [Add Delta]
    (O : SignatureObservation State Sig) (D : SignatureDelta Sig Delta)
    (law : AdditiveSignatureDeltaLaw D) :
    {X Y : State} -> (plan : ArchitectureEvolution State X Y) ->
      NetSignatureDelta (SignatureDeltaSequence O D plan) =
        EndpointSignatureDelta O D plan

But this theorem is finite path calculus under the assumption that the selected delta satisfies an additive law. It does not claim that unobserved axes, incident risk, review quality, or actual PR outcomes can all be added this way.

The force has multiple components.

Force component	Meaning
Feature force	The force that moves product functionality forward.
Repair force	The force that repairs existing breakage.
Coupling force	The force that increases or decreases coupling.
Boundary force	The force that preserves or violates boundaries.
Type force	The force that adds type information or creates type holes.
Test force	The force that increases or decreases observability through tests.
Debt force	The force that pushes the system toward a bad basin.
Refactor force	The force that helps it escape a bad basin.

A good PR has not only feature force, but also stabilizing force.

v_PR = v_feature + v_stabilize

A risky PR moves the feature forward locally while quietly adding small debt force.

v_PR = v_feature + v_debt

In AI-generated PRs, the especially important case is one where tests pass and the specification is satisfied, but small v_debt, v_coupling, v_type_hole, or v_entropy accumulates repeatedly. It may be hard to see in a single PR. But as a trajectory, the system is moving toward a bad basin. I call this the Local Correctness Trap.

3. Three Classes of Force

The earlier discussion about product managers, product owners, review, and CI/CD becomes clearer if we separate force by observability.

Force can be divided into three classes.

Force class	Meaning	Main evidence
ObservedForce	Before / after signature delta of PRs that were actually merged.	PRs, ArchSig reports, drift ledger.
LatentForce	Invisible force by which requirements, design, prompts, and local code style shape which PRs are proposed.	Requirements, prompts, proposal logs, case studies.
DissipatedForce	Raw force that was rejected, corrected, or weakened by review / CI / types / policy.	CI failures, requested changes in review, rejected proposals.

This classification makes AI-assisted development more concrete.

If we look only at merged PRs, we see only ObservedForce.

But in an era where AI can generate many proposals, the force that was not merged also matters. Force removed by review, rejected by CI, or reshaped before merge matters.

To understand how well a dissipative system is working, we need DissipatedForce.

To understand what kind of PR distribution is created by upstream requirements or prompts, we need LatentForce.

In Lean, the separation between accepted and rejected changes appears as a damping / control schema.

structure DampingControlSchema (State : Type u) (Sig : Type v) where
  observation : SignatureObservation State Sig
  invariant : SafeRegion Sig
  accepted :
    {X Y : State} -> ArchitectureTransition State X Y -> Prop
  rejected :
    {X Y : State} -> ArchitectureTransition State X Y -> Prop
  acceptedPreservesInvariant :
    ∀ {X Y : State} (t : ArchitectureTransition State X Y),
      accepted t -> StepPreservesSafeRegion observation invariant t
  coverageAssumptions : Prop
  nonConclusions : Prop

What this proves is limited: transitions classified as accepted preserve the explicitly stated invariant. The existence of rejected changes does not prove that the whole future of the codebase is safe.

On top of this schema, it is proved that accepted finite evolutions create trajectories inside the selected invariant.

theorem acceptedEvolution_preserves_selectedInvariant
    (control : DampingControlSchema State Sig) :
    {X Y : State} -> (plan : ArchitectureEvolution State X Y) ->
      StateInSafeRegion control.observation control.invariant X ->
      control.AcceptedEvolution plan ->
        SignatureTrajectoryInSafeRegion
          control.invariant (SignatureTrajectory control.observation plan)

4. A Chaos-Game-Like Correspondence

This is where the chaos-game-like reading appears.

The similarity is that we have multiple transformations, one of them is selected at each step, and a state trajectory is produced.

The difference is that, in software development, neither the set of transformations nor their likelihood is fixed. Requirements, review, CI, design boundaries, existing examples, and AI agent behavior all affect which operation is likely to be selected next.

So the goal is not to claim that software development literally is the classical chaos game. The goal is to use AAT vocabulary to handle the structure where multiple operations are repeatedly selected and the resulting trajectory tends to move toward certain regions.

The correspondence is:

Chaos-game side	AAT / development side
State `X_t`	Architecture state / codebase field.
Transformation `f_i`	Architecture operation / PR / patch.
Transformation selection	Operation selection by developer / AI / requirement / review.
Trajectory	Architecture Signature trajectory.
Attractor	Signature region where the system tends to stay.
Basin	Initial or surrounding states likely to fall into that attractor.
Control input	Prompt, review policy, CI, type checker, architecture rule.

As a formula:

X_{t+1} = f_{i_t}(X_t)
i_t ~ P(. | X_t, control_t)
Y_t = sigma(X_t)

The important point is not to assert probability or attractors as strong theorems too early.

What we should handle in practice is first an attractor candidate or basin candidate relative to a finite observation window, bounded horizon, selected signature axes, and selected operation support.

finite observed trajectory
  + selected signature region
  + bounded operation support
  -> attractor / basin candidate

This is not an escape into weak claims. It is a boundary that makes measurement and falsification possible.

5. Support Shaping

The mathematical core of Attractor Engineering is support shaping.

This is not just about "blocking bad PRs". It is about changing the set of operations that can naturally be selected next, and changing how likely they are to be selected.

In short, Attractor Engineering is a theory of designing the geometry of the operation distribution.

def Supports
    (kernel : FiniteOperationKernel State OperationId)
    (X : State) (op : OperationId) : Prop :=
  op ∈ kernel.support X

For the current architecture state X, the set of operations that can naturally be selected is called operation support.

Good design changes this support.

def SupportOperationsPreserveSafeRegion
    (kernel : FiniteOperationKernel State OperationId)
    (sem : OperationTransitionSemantics State OperationId)
    (O : SignatureObservation State Sig) (R : SafeRegion Sig) : Prop :=
  ∀ {X : State} (op : OperationId),
    kernel.Supports X op -> sem.OperationPreservesSafeRegion O R op

The strong form of support shaping says: operations that remain in support preserve the selected safe region. In practical terms, we reduce bad operations, increase good operations, make correct paths easier to choose, and make dangerous shortcuts less convenient.

This idea is packaged on the Attractor Engineering side as follows:

structure AttractorEngineeringSupportPackage
    (State : Type u) (Sig : Type v) (OperationId : Type w) where
  observation : SignatureObservation State Sig
  kernel : FiniteOperationKernel State OperationId
  semantics : OperationTransitionSemantics State OperationId
  targetRegion : SafeRegion Sig
  supportPreserves :
    kernel.SupportOperationsPreserveSafeRegion semantics observation targetRegion
  coverageAssumptions : Prop
  measurementBoundary : Prop
  nonConclusions : Prop

With this package, if a bounded script uses only operations from finite support, and the starting point is in the target region, then the observed trajectory remains in the target region. This is stated as a theorem.

theorem supportPackage_preserves_targetTrajectory
    (package : AttractorEngineeringSupportPackage State Sig OperationId)
    (script : BoundedOperationScript OperationId)
    {X Y : State} (plan : ArchitectureEvolution State X Y)
    (hStart :
      StateInSafeRegion package.observation package.targetRegion X)
    (hRealizes : script.RealizesEvolution package.semantics plan)
    (hSupport :
      package.kernel.ScriptUsesSupport script.operations plan) :
    SignatureTrajectoryInSafeRegion package.targetRegion
      (package.TargetTrajectory plan)

For example, good APIs, good examples, clear ownership, narrow modules, and domain states represented in types increase the local discoverability of good operations.

Conversely, a huge common module, implicit global context, ambiguous services, and overly convenient helpers increase the local convenience of bad operations.

From this viewpoint, refactoring is not only cleaning up the current structure. It is also a basin-reshaping operation that changes the future operation distribution.

In the measurement layer, one tooling-side metric candidate to watch here is SupportRiskMass.

SupportRiskMass(C) =
  sum over op in support(C) of weight(op) * risk(op, C)

Here again, it is important not to reduce risk to a simple 0 / 1.

In AAT terms, we should distinguish at least:

safe-preserving proved
safe-preserving measured
safe-preserving estimated
unsafe witness measured
unmeasured
unavailable
private
notComparable
outOfScope

Unmeasured must not be read as zero. This is a central principle in both ArchSig and AAT.

6. The Same Signature Does Not Imply the Same Future

An important point is that two states can have the same current Architecture Signature but different future operation distributions.

For example, two modules might show the same number of dependency violations, the same test coverage, and the same complexity. But one may have a good canonical example nearby, while the other may contain many bad shortcuts.

Even if the current observation values are the same, future PRs may be attracted in different directions.

Obs(X) = Obs(Y)
  does not imply
OperationSupport(X) = OperationSupport(Y)

This is why architecture quality should not be judged by snapshot metrics alone. The current value can be the same while the future force field is different. Attractor Engineering treats this future force field as a design object.

7. Accepted Preservation and Support Preservation Are Different

There is another important separation.

Suppose review and CI ensure that merged PRs preserve a safe region.

Even then, unsafe operations may still remain inside operation support.

This separation is not just a warning. It appears on the Lean side as a finite counterexample. Accepted-step invariant preservation can hold, and an accepted safe step can exist, while operations that do not preserve the safe region remain in support.

theorem acceptedPreservation_not_supportPreservation_counterexample :
    (∃ (t : ArchitectureTransition ExampleState safeState safeState),
      control.AcceptedStep t ∧
        StepPreservesSafeRegion control.observation control.invariant t) ∧
    (∀ {X Y : ExampleState} (t : ArchitectureTransition ExampleState X Y),
      control.AcceptedStep t ->
        StepPreservesSafeRegion control.observation control.invariant t) ∧
    (∃ X op,
      kernel.Supports X op ∧
        ¬ semantics.OperationPreservesSafeRegion control.observation
          control.invariant op)

This is the difference between guardrails and attractor engineering.

Strong guardrails may stop bad PRs.

But a field where bad PRs are produced in large numbers every time is still not a good field.

A good field is one where bad operations are less likely to appear in the first place, and good operations are natural, easy to imitate, observable, and low-friction.

8. PRs Are Non-Commutative

PRs are generally non-commutative.

PR_2 o PR_1 != PR_1 o PR_2

Of course, this only makes sense when both orders can be applied. Even then, the same two PRs can produce different final signatures depending on merge order.

This matters in an era where AI agents can generate multiple PRs in parallel.

Even when individual PRs are locally correct, their order can change boundaries, types, tests, and semantic alignment.

I call this merge order sensitivity.

MergeOrderSensitivity(a, b, X) =
  distance(
    sigma(b(a(X))),
    sigma(a(b(X)))
  )

This is not merely a merge conflict issue. It is the non-commutativity of operation algebra branching the signature trajectory. We will need this viewpoint when evaluating teams of AI agents as well.

9. Observe the Shape of the Trajectory

Architecture Signature should be read not only as a current value, but also as a trajectory.

Even if the endpoint is safe, the path may have passed through a bad region.

Even if net delta is zero, there may have been large churn inside the path.

endpoint safe
  does not imply path safe

net force zero
  does not imply no excursion

This is also proved in Lean as a small finite counterexample. In a trajectory such as 0 -> 2 -> 0, both endpoints are the same safe state. The endpoint delta and net delta can both appear to be zero, while the path passed through an unsafe region.

theorem netSignatureDelta_eq_zero :
    NetSignatureDelta (SignatureDeltaSequence observation signedNatDelta
      excursionPlan) = 0

theorem endpointSafe_and_zeroDelta_but_not_pathSafe :
    EndpointSignatureDelta observation signedNatDelta excursionPlan = 0 ∧
      StateInSafeRegion observation safeRegion 0 ∧
      StateInSafeRegion observation safeRegion 0 ∧
      ¬ SignatureTrajectoryInSafeRegion safeRegion
          (SignatureTrajectory observation excursionPlan)

Trajectories have shapes.

Trajectory type	Meaning
Stable Orbit	The system returns to a safe region after small changes.
Drift	The system slowly shifts toward a bad region.
Spiral Debt	It appears to return, but over the long run moves closer to a bad basin.
Sudden Phase Shift	A signature changes sharply after a particular PR.
Oscillation	Feature additions and refactorings alternate between good and bad.
Basin Capture	After some point, the system gets captured by a bad structure.

What ArchSig really wants to observe is this trajectory.

Not just the evaluation of one PR, but the resulting motion produced by a group of PRs.

10. Expanding Observation Can Suddenly Reveal Badness

With coarse observation, a codebase may look safe.

But if we add more observation axes, a hidden obstruction may suddenly appear as nonzero.

coarse observation:
  safe

refined observation:
  hidden obstruction appears

We can call this an observability expansion shock.

The important point is that this does not necessarily mean the architecture got worse. It may simply mean that an axis that used to be invisible has become visible.

That is why ArchSig must distinguish unmeasured from zero. When something that was not measured becomes visible, we must separate "the architecture got worse" from "the observation became better".

About the Lean Formalization

The structure above is not built only from metaphor. Some of the core vocabulary of AAT has been implemented as Lean definitions and theorems under Formal/Arch.

The repository is AlgebraicArchitectureTheoryV2. The proved API is summarized in the Lean definition and theorem index.

The vocabulary used in the second half of this article mainly corresponds to Formal/Arch/Evolution/SignatureDynamics.lean and Formal/Arch/Evolution/AttractorEngineering.lean.

The role of Lean formalization is not to give this theory an aura of correctness. Its role is to record, with boundaries, what can be said under which universe, observation, coverage, and exactness assumptions.

It is important that counterexamples live in the same place as proved theorems.

proved:
  accepted evolution preserves selected invariant
  bounded sampled support-preserving script stays in target region
  selected additive delta telescopes over finite path

proved counterexamples:
  endpoint safe + zero delta does not imply path safe
  accepted preservation does not imply support preservation
  unmeasured axis is not available-zero evidence

Conversely, the fact that something is proved in Lean does not mean that a real-world code extractor is complete, or that every runtime / semantic obstruction has already been observed. With this boundary, AAT can separate what is formally known, what depends on measurement, and what remains an empirical research question.

Conclusion

The discovery of Attractor Engineering changes how I see software architecture: from a static blueprint to a field that guides future changes.

If software architecture is read as an algebraic structure, feature additions and refactorings become operations.

When those operations are repeated, the architecture state draws a trajectory.

We can then ask where that trajectory tends to go, and where it tends to stay. This is where attractors and basins enter the picture.

Architecture design in the era of AI-assisted development can be described as creating a field where future changes gather in good places and can escape bad places.

Harness engineering becomes the engineering of receiving AI's change force, dissipating unwanted components, and guiding the system toward good attractors.

ArchSig is the tool for observing that trajectory.

The essence of AI-assisted development is not only producing PRs faster.

It is deciding where fast force should converge.

A codebase is a field.

A PR is a force.

CI/CD is a dissipative system.

Product managers, product owners, engineers, reviewers, and AI agents are participants in the field.

ArchSig is an observer of the trajectory.

With this framing, development in the AI era is no longer just automation. It becomes field design.

As a design theory for that purpose, Attractor Engineering may be a useful direction for both practice and research.