Who sits down to read an 88-page paper about the specific architecture behind DeepSeek Harness? We did.
"A Programming Paradigm for Spatiotemporal Composability" is the paper behind the Cordis-based plugin architecture that dsh is built on.
It is 88 pages ( here is the PDF ) answering one very specific question: how do you compose software that changes while it is running? The paper answers with a calculus and five proved theorems. Reading it, evidence included, can get a little tedious.
Three authors sign it: Yifan Shi, listed with a double affiliation, Peking University and DeepSeek-AI; Wei Zhang, of Peking University; and Tianyi Cui, of DeepSeek-AI.
It is a programming languages paper written from inside an AI lab.
So we have put together a reading guide: what problem sits underneath, what Cordis is, who signs it, what the theorems prove and which part is already running in real code.
The problem: changing a running system without breaking anything
Picture a system that is running and to which you want to add a new capability without stopping it. A new vision tool for a model or a harness, say.
That capability may depend on a database, on a model or on another service, and later you may want to retire it, swap it, replace a dependency or reload the component.
The hard part comes after the code is added or removed: guaranteeing what happens to everything that code had registered, which dependencies are still available and what state the system is left in when the change finishes.
In many systems, a good share of that responsibility falls on infrastructure code and developer conventions. What Cordis proposes is moving it into the semantics of the runtime itself, with explicit rules for dynamic changes and properties that can be formally proved.
What Cordis is and what it has to do with DeepSeek Harness
When DeepSeek released DeepSeek Harness on 13 August 2026, alongside V4-Pro, almost all the attention went to the agent.
We were far more interested in the harness. Because underneath sits something less flashy and more interesting: Cordis, the plugin framework the whole thing is assembled on.
DeepSeek Harness has no protected core in the traditional sense. The agent's capabilities, meaning the models, the tools, the sessions, the permissions and the interface itself, are structured as plugins that register into a shared context.
Cordis sets the rules by which those plugins load, unload and coexist while the system keeps running.
But Cordis did not start with the harness. It is an earlier project, with years of production behind it and a repository of its own , that DeepSeek Harness takes on as a dependency. The paper at hand is the formalization of rules Cordis had already been applying in code.
How that microkernel works inside, with its services, its typed events and its shared context, is covered in our section on Cordis .
The core idea in Cordis: two dimensions of dynamic change
The paper splits the dynamic composition problem into two orthogonal dimensions: time and space. The word "spatiotemporal" is the most important part of the title, and half the paper goes into it.
Time: revertible effects
The first dimension is time, and the tool is revertible effects.
Everything a plugin does on load, such as registering a command, hooking into an event or opening a connection, is an effect on the shared context.
In this model every effect carries its own inverse, which the runtime keeps track of. When the plugin unloads, the system runs those inverses and reverts its effects: there should be no orphan listener, no open connection and no ghost command left behind.
The important idea is that undoing stops depending on a cleanup function written by hand and becomes part of the rules of the model.
The revertible effects section covers it in more detail.
Space: reactive coeffects
The second dimension is space, and that is where reactive coeffects come in.
If an effect is what your plugin does to the system, a coeffect is what your plugin needs from the system: a database, a model or a service it depends on.
In Cordis those needs are declared, and the runtime uses the declaration to manage the lifecycle: it does not activate the plugin until what was declared is served, and it reacts when dependencies change, deactivating or reconfiguring the component when appropriate. A dependency stops being a line in an import and becomes something the system watches at runtime.
The reactive coeffects section walks through the full activation and deactivation cycle.
The central move in the paper is unifying both sides into a single kind of context, so that effects and coeffects are tracked by the same machinery. On that base it defines what a component is and builds a calculus of dynamic composition: the formal rules of a system where the pieces come and go without stopping the whole.
The five theorems in the Cordis paper, explained
Metatheory is the most tedious part to review and turn into something readable. But the paper brings five proved results about the calculus. Here is what each one says.
| Theorem | In plain language | What property it buys |
|---|---|---|
| Preservation | No valid step, be it load, unload or reload, leaves the system in a malformed state | After every move, the system still satisfies its own rules |
| Temporal composability | Reverting a component's effects returns the system to the state it would be in had that component never acted, even if others kept working in between | Undoing is exact |
| Spatial composability | Nobody activates without its dependencies served, and nobody has a dependency pulled from under it while in use | A provider only withdraws once its dependents have deactivated |
| Progress | As long as the dependency graph has no cycles, every pending transition eventually completes | The system does not get stuck halfway through a change |
| Confluence | Under the theorem's conditions, different orders of changes lead to the same stable state | The final result does not depend on the dynamic history |
Confluence is the one that rules. A system that has spent hours loading and unloading pieces converges to the same state you would have got by assembling in one go, in dependency order, whichever components ended up active.
The theorems section develops the formal statements, with their conditions and their notation.
What the theorems do not say
This part matters as much as the results themselves. A theorem proved about a formal model is a claim about that model, under its conditions.
There are conditions here, and the paper states them. Confluence, for instance, is proved assuming the dependency graph has no cycles and that the steps involved are independent of each other. Almost everything else sits outside the model: that each plugin's code does what it promises, that the real runtime implementation is faithful to the calculus, that the network and the disk behave the way we expect. The case study itself acknowledges an important limitation: the evidence comes from a single ecosystem in a single language and is observational.
From paper to production: Koishi and the harness's 49 packages
What makes *A Programming Paradigm for Spatiotemporal Composability* unusual next to many language papers is the direction of travel: the code had been in production for years by the time the formalization arrived.
Every construct in the calculus has its counterpart in the Cordis API. The effect that carries its inverse in the paper is what a plugin registers on load, the coeffect is the list of dependencies it declares, and the transitions of the calculus correspond to the lifecycle the runtime actually runs. The DeepSeek Harness piece walks that correspondence symbol by symbol , with the real API next to each definition.
The paper's case study is Koishi, an open source chatbot framework built on Cordis that has accumulated more than 4,000 community plugins in four years. It does not prove the model is correct across every possible system, but it does show its abstractions being used in a real ecosystem with independent contributors.
DeepSeek Harness is the other proof of life. At commit 47f9438, which we use as the reference for this analysis, the repository was organised into 49 packages, all of them plugins on that same core.
What changes if you have AI agents in production
If you have agents in production, their capability list rarely stays still: a new tool this month, a model coming in, an integration being retired. Today, many of those changes end up meaning a redeploy or bespoke logic for touching a live system without leaving pending resources or broken dependencies.
What the paper contributes is a formal basis for those changes: on a runtime that implements this model, you can add and remove capabilities from an agent in production without the system ending up in a state nobody can explain. Hot changes converge to the same state as a clean install, and no operation is left hanging halfway.
The paper formalizes the composition scaffolding, but not the intelligence of each agent or the correctness of each plugin. You can change an agent's capabilities while it runs, with a defined semantics for how they enter, what they depend on, what they undo on the way out and what state they converge to. That is the most interesting thing about Cordis.
If you want the full tour, from starting DeepSeek Harness up to the mathematical formalization, our dedicated microsite develops it across 24 sections.
