Verification should only have to happen once.

The thing we keep throwing away

The manifesto makes one move: when writing code is free, the scarce work is proving it correct. Everything follows from that. But there is a second move hiding behind the first, and we have not made it yet.

If verification is the expensive part, then doing it twice is the waste.

Right now every agent starts from nothing. It generates a date parser; the compiler checks it; the tests run; it works — and then the next task, the next session, someone else’s agent generates a date parser again, and checks it again, and the verification that already happened counts for nothing. We have built a world where the cheap thing is reused without a second thought and the expensive thing is recomputed on every turn.

A proof is not a draft. It does not need to be redone because someone new walked into the room. Once a function has been shown to typecheck, to be total, to satisfy its stated properties, and to compile to a reproducible artifact, that result is established. It should be citable. It should be borrowable. It should only have to happen once.

A function that can be vouched for

Source code is a lossy compression of intent. We have always known this, which is why we surround it with the uncompressed version — tests, docs, assertions, review. A manifest is what a function becomes when you stop throwing the uncompressed version away.

It is a definition together with three things a source file does not carry. An identity: a content hash, so the same meaning has the same name everywhere it appears. An evidence bundle: a precise record of what has been checked about it — and, just as importantly, what has not. And a provenance: the signatures of who compiled it, who tested it, who reviewed it, who vouched.

A manifest is the semantic artifact, completed. Intent-first, explicit about effects, verifiable, reproducible, explainable — and now also addressable, and now also attestable. It is not a file you run. It is a result you cite.

Written once

Identity is the hinge, and it is not a hash of the source text. Two engineers who write the same function in different styles — different names, different spacing, an argument flipped and flipped back — have written the same function, and it should have the same name. So the address is computed over the elaborated meaning of the definition, after the compiler has stripped away everything that was only how it was typed and kept only what it does.

From that one decision, a great deal falls out. Names stop being identity and become labels — many labels can point at one meaning, and a rename is a note in the margin, not a change to the thing. Dependency conflicts that come from two packages fighting over the same name simply cease to exist, because nothing is identified by its name. And when two people, anywhere, independently arrive at the same definition, it is stored once, and their evidence and their signatures pool onto the same object. Convergence is the closest thing software has to a shared, checkable truth, and this is how you let it accumulate: one definition, written once, vouched for by everyone who has ever needed it.

We did not invent this idea. Unison did. We are bringing it to a language where a definition can carry a proof, and to a compiler that can turn it into something fast.

Meaning under a contract

There is a wrinkle, and it is the most arcanist.sh thing about the whole design. In BHC the same source does not have one meaning. Compiled under the numeric profile it is strict, fused, and unboxed; under server it is structured and observable; under edge it is stripped to almost nothing. Same text, different envelope, genuinely different artifact.

So a manifest is not named by its meaning alone. It is named by its meaning and its contract — the profile, the language edition, the dependency hashes it was elaborated against. The same definition under two profiles is two manifests, because it is two behaviors, and the commons is honest about that. This is the “semantic artifact” thesis taken literally: the unit of software is meaning under a stated contract, and that pair is its name.

The evidence travels with the artifact

The model does not need to be right; it needs to be checkable. A manifest is where “checkable” stops being a slogan and becomes data.

Every manifest states exactly what holds. That its types are consistent — always. That its patterns are exhaustive and it has no partial escape hatch — when that has been established. That it satisfies a property, with the property written down and the check attached. That a refinement was discharged to a solver. And it states, in the same breath and with the same precision, what is merely asserted and was never checked. A compiler built for this era refuses to stay quiet about what it cannot prove; a manifest writes that refusal down and carries it along.

This is why the unit is a manifest and not a “truth.” Nothing here promises that a function is right. It promises something narrower and far more useful: a verifiable account of what was checked, by whom, under what contract — enough for the next author, human or model, to decide whether the result is strong enough to build on.

Vouched, not trusted

Provenance is the part that makes a commons safe to draw from. A manifest carries signed attestations — this compiled reproducibly to this artifact, this passes this property suite, this was reviewed by this key, this is vouched for by this organization. The same kind of signature that already guards a toolchain snapshot, applied to a single definition.

The load-bearing attestation is reproducibility, because it is the one nobody has to be trusted for. Anyone can recompile the manifest and confirm they reach the same address and the same artifact — trust, but verify, mechanically, every time. On top of that objective floor sits human judgment: whose review you require, whose vouch you accept, which organizations you will and will not build on. You set the policy; the commons enforces it; the ledger of who attested to what is append-only and public, the way a transparency log is.

What the compiler becomes

Give the meaning engine a commons to draw from and its job grows. It no longer compiles a file. It resolves a closure of manifests — a chosen set of definitions and everything they depend on, each named by content, each carrying its evidence — checks that they cohere, and lowers them, under the profile you asked for, into a binary, a WebAssembly module, a GPU kernel. A compute artifact built out of a collection of small, specific, separately-vouched-for results.

And the artifact is itself a manifest. Addressed, reproducible, attestable. The output of the commons is more commons.

The job changes again

The manifesto ends by saying the unit of work becomes the obligation, not the function — closer to architecture than to authorship. The commons is where that lands. When verification is cumulative and shareable, an agent’s task stops being write this code and becomes assemble this from meaning that is already checked, and where nothing exists yet, write it, prove it, and leave it behind for the next one. Generation was always going to be cheap. The point was never to generate more. The point was to stop verifying the same thing forever.

We have a conviction, not a crystal ball. The hard parts are real — addressing a language with type classes, drawing the line around effects, deciding who is allowed to vouch. None of them are reasons not to start, and most of the machinery already exists in the compiler under another name. The commons is the direction, not yet the destination.

All beginning is Haskell. The rest is who else gets to build on what you proved.