For agents
Most code being written now is not typed out by a person. Deed is
built on that being true, and deed mcp is the part of it
you can point a tool at: a Model Context Protocol server, so the
thing writing the code asks the compiler instead of remembering.
loading the compiler
What comes back that a type error does not
A compiler that only says yes or no tells an agent whether it has finished. Deed says which of the promises in the signature it settled, and which it could only arrange to check at runtime. That is a gradient, and something iterating on its own output can climb it.
……
proven means the checker discharged it at compile time.
tested means it produced a property and ran it. Neither
was asked for.
And when it cannot
The same refinement without the precondition that establishes it. The answer is not "no", it is which tier this landed in and the reason it did not land higher.
……Nothing narrowed this name is a sentence a model can act on. It says where to look, which is the caller's side, and it is the difference between a warning and a next step.
A repair, and the reason behind it
Models reach for export, because most languages have one.
Across
five recorded runs
this was the single most common thing said, forty-five times, in
every task. So the answer carries the edit that fixes it and the
reason the word does not exist:
……
machine-applicable is the compiler saying this one may
be applied without asking. Guesses are marked differently and are
never applied on their own, which is a distinction an agent can only
respect if it is told.
A test nobody wrote
The contract in a signature is not documentation. Ask the same server to run the tests of a module that contains none, and it runs the property the contract generates:
……A hundred cases, from a seed that is in the answer so the run can be repeated. In the recorded runs this happened three times to a model that had been told not to write tests.
Wiring it up
The server speaks MCP on stdin and stdout, so a client starts it the way it starts any other:
{
"mcpServers": {
"deed": { "command": "deed", "args": ["mcp"] }
}
}
There is nothing else to install; see
Install. Six tools:
deed_check, deed_test,
deed_run, deed_fmt, deed_fix
and deed_explain. The full walkthrough is
in the repository.
What it is not allowed to do
The server holds no capability. A program arrives as text and the answer leaves as text; it opens no file, resolves no path, and refuses to run a program whose signature reaches for a directory before running a single instruction. That is not a sandbox bolted on — it is the same rule the language is about, applied to itself.
The cost is written down rather than hidden: a server with no filesystem cannot be handed a module set, so a program that imports another module has to arrive with it.
Does it actually help?
Measured, not asserted. Six tasks, one model, five runs, against a control arm with the compiler taken away:
| Arm | Answered | Check | Pass their tests |
|---|---|---|---|
| prompt only | 6/6 | 0 | 0 |
with deed mcp |
6/6 | 5 or 6 | 5 |
Six confident answers either way, and not one of the prompt-only ones compiles. Deed is in nobody's training data, which is what makes the control arm worth having and what makes the number honest rather than impressive.
The record says what it does not establish, too: one model family, no comparison against a language without contracts, and a control arm recorded against an earlier build. Read it before quoting it.