formalswarm

FormalSwarm

Your agent says the change is safe. FormalSwarm makes it prove it.

Independent agents write theses in parallel, adversarial critics tear them down, and a seal runs real commands — then a deterministic rollup reads the verdict out of exit codes and case counts, never out of an agent's prose. Any repository, any language, any scale: from a 6-agent pilot to hundreds of agents. On DeepSeek Harness, Claude Code and ZCode from one and the same code.

---

The 60-second version

# from a checkout
FS="node ./core/bin/formalswarm.js"

# once the plugin is installed, resolve it from wherever the runtime put it:
#   Claude Code   FS="node $CLAUDE_PLUGIN_ROOT/core/bin/formalswarm.js"
#   ZCode         FS="node $ZCODE_PLUGIN_ROOT/core/bin/formalswarm.js"
#   any runtime   FS="node $(node -p "require('path').dirname(require.resolve('formalswarm/package.json'))")/core/bin/formalswarm.js"

$FS init                                   # profile this repository
$FS brief \
  --objective "Make cache eviction deterministic under concurrent writes" \
  --verdict-question "Does the cache evict deterministically under concurrent writes?" \
  --context src/cache.py,src/locks.py,tests/test_cache.py \
  --seal "python3 -m pytest -q tests/test_cache.py" \
  --seal "python3 -m pytest -q -k concurrency"
# -> brief.json, with the prompts and the repository profile already embedded

Then run it. You get one file, /outcome.json:

{
  "global_verdict": {
    "outcome": "REVISE",
    "reason": "at least one seal check fails (exit_code != 0) or a verifier declares REVISE",
    "warnings": ["2 objection(s) were filed by a critic outside its assigned partition ..."]
  },
  "objection_count": { "total": 9, "accepted": 8, "rejected": 1, "unanswered": 0, "orphan": 0 },
  "verdict_review": [
    { "verifier": "seal-1", "declared": "REVISE", "effective": "REVISE", "coherence": "ok",
      "notes": [] },
    { "verifier": "seal-2", "declared": "CONFIRM", "effective": "CONFIRM", "coherence": "ok" }
  ],
  "seal_verdicts": [ { "checks": [ { "command": "python3 -m pytest -q -k concurrency",
                                     "outcome": "failed", "exit_code": 1, "cases": 6 } ] } ]
}

Anyone can recompute that verdict. Nobody has to trust a paragraph.

---

Verify it yourself in 30 seconds

Zero agent calls, no API key, no network:

node core/validate-all.js   # -> ALL SUITES GREEN — 114 checks (body 48, driver 24, profile 23, generic 19)
node tests/smoke-e2e.js     # builds real throwaway projects, spawns the seal commands, asserts real exit codes

Both must exit 0. The first is the whole offline gate: every rollup branch, driver identity, profiler fixture and genericity guard, counted one by one — 114 lines of proof, about four seconds. The second needs python (or python3) on PATH for its fixture toolchain.

A verdict this repository computed about itself

FormalSwarm's first published debate ran on FormalSwarm itself: 5 theses, 5 critics, 5 seal verifiers, 6 real commands, 15 agent calls. The rollup returned REVISE — read straight from outcome.json:

{
  "global_verdict": {
    "outcome": "REVISE",
    "reason": "at least one seal check fails (exit_code != 0) or a verifier declares REVISE",
    "warnings": ["phase ANTITHESIS: 1 fallen agent(s)"]
  },
  "objection_count": { "total": 11, "accepted": 0, "rejected": 0, "unanswered": 0, "to_answer": 11, "orphan": 0 }
}

What the 15 agents actually measured:

• Every assigned seal check was green with counted cases: the offline gate (node core/validate-all.js, exit_code: 0, cases: 110), the end-to-end smoke (node tests/smoke-e2e.js, exit_code: 0, cases: 6, a green fixture reaching CONFIRM and a broken one REVISE quoting the real exit code), and the driver and genericity suites. The installed plugin copy passed the same gate in place.
• All five verifiers independently reproduced the one blocking objection with their own discriminating commands (exit_code: 1): the docs claimed any refused spawn makes the verdict INCONCLUSIVE, while the code enforces that only for a whole silent group and for the seal — a partial fall elsewhere was a warning, and the suite even pinned the contradicting behavior green.
• One critic fell for a reason the protocol is proud of: its answer missed required schema fields, save refused it, and the run recorded a fallen agent instead of reading a malformed answer.

The fix (narrow the two doc sentences, harden the rollup against out-of-enum outcomes and non-integer counts, make the gate's temp directories per-process unique, and pin the real partial-fall semantics with new counted checks) took the gate from 110 to 114 green checks. The verdict was never edited: REVISE is what the code computed, and the corrections came after it.

---

The problem this exists for

A capable agent reviews a change and writes a confident, well-argued paragraph. It is often right — and it is still not evidence, because you cannot recompute it. Three failure modes show up constantly, and none of them is a stupid mistake:

Failure	What it looks like	Why nothing catches it
Empty green	The command exits 0 having tested nothing (unittest discover with no -s tests finds zero tests and still exits 0)	The exit code is genuinely zero; only a case count reveals it
Missing evidence	The reviewer silently skipped one of the things it was asked to check	Nothing compares what was asked against what was answered
Silence as agreement	One subagent crashed; the summary reads as if everything passed	A dead agent produces no objection, and no objection is read as consent

FormalSwarm exists to make those three states mechanically visible, and to make the verdict a computation rather than a judgement.

Why not just ask another agent to review it?

Because you would get a second confident paragraph. The difference is not the model — it is what counts as evidence:

	A reviewer (human or model)	FormalSwarm
Evidence that "it works"	prose	real exit codes and counted cases
Adversarial pressure	depends on the reviewer	partitioned critics, hunting hallucinations by contract
A check that tested nothing	invisible	cases: 0 → INCONCLUSIVE — empty green is a verdict, not a pass
A subagent that died	invisible, or worse	fallen_agents and warnings — silence is never a vote
The final answer	an opinion you re-read	outcome.json — a computation anyone can re-run

---

The idea, and where it comes from

In September 2026 OpenAI reported a mathematics run in which on the order of 10,000 agents exchanged millions of messages over 88 hours attacking the Navier–Stokes Millennium problem, with formal verification in Lean acting as a seal on whatever the swarm produced — reported at the time by WION.

The interesting part is not the number. It is the two-part shape:

1. Massive, independent, parallel exploration — many attempts, no shared context, no groupthink.
2. A machine-checked oracle that does not care how confident anyone sounds.

That shape does not need a Millennium problem. Your repository already owns the oracle: its test suite, its linters, its measurement scripts. The seal of a FormalSwarm debate is not Lean — it is your commands, with their real exit codes and their real case counts, and a rollup that fails closed.

What this is not. It is not a reproduction of that result; it is that pattern applied to ordinary software work. And no number of agents makes an unmeasurable claim measurable: FormalSwarm does not make agents smarter, it makes their output auditable, and it will happily tell you INCONCLUSIVE when the repository cannot decide the question.

---

How it works

 THESIS            ANTITHESIS           [SYNTHESIS]        SEAL
 n writers   ──▶   m critics      ──▶   only the      ──▶  k verifiers run the
 in parallel       each with a          attacked            checks for real:
 (isolated)        disjoint slice       writers answer      command, exit code,
                   of the theses        their objections    case count, output
                        │                                        │
                        └──────── deterministic rollup ──────────┘
                                       CONFIRM / REVISE / INCONCLUSIVE

Phase	Who	Must produce
THESIS	n_thesis writers, isolated subagents	a position, its findings with path:line evidence, its risks, and the measurement that would prove it
ANTITHESIS	n_critics, each handed a disjoint partition of the theses	objections with re-read evidence: hallucination, dead_control, dead_guard, logic_bug, bad_measurement, empty_green, safety, other
SYNTHESIS	only the writers actually attacked (rounds ≥ 2)	answers that copy the objection's evidence string verbatim, so the accept/reject count is deterministic
ANTITHESIS-2	n_critics on the revised state with a deterministic board (rounds = 3)	genuinely new objections; already-accepted ones are absorbed
SEAL	n_seals verifiers, each with a disjoint slice of your seal_plan	command, outcome, exit_code, cases, detail — and a per-check measurement limit

The orchestrator never votes. It opens the rounds, executes the subagents, and reads a verdict that the body computed.

---

Scale: 6 agents or 600

The default plan is a 2+2+2 pilot — six agent calls, the right size for a first run or a new kind of task. Scaling up is a flag, not a redesign:

# a wide exploration: 60 writers, 40 critics, 40 verifiers, one round
formalswarm brief ... --thesis 60 --critics 40 --seals 40 --max-calls 200

# the full cycle: thesis → antithesis → synthesis → antithesis-2 → synthesis-2 → seal
formalswarm brief ... --thesis 20 --critics 10 --seals 10 --rounds 3 --max-calls 120

Group sizes go from 1 to 500; there is no policy ceiling. The only ceiling is the one you declare:

Flag	Meaning
--thesis N / --critics N / --seals N	size of each group (defaults 2, 2, 2)
--max-calls N	the budget for the whole run (default 15) — the plan is refused before the first call if it would exceed it
--rounds 1|2|3	1 = thesis + antithesis + seal; 2 = + synthesis; 3 = + second antithesis and synthesis

Worst case = thesis + critics + seals + (rounds≥2 ? thesis : 0) + (rounds≥3 ? critics + thesis : 0). Real cost is usually lower: synthesis only runs for writers that were actually attacked, and idle critics are never spawned.

Two things keep a large run honest rather than merely large:

• The partition scales with the critics. Writers are dealt round-robin across the critics, so each critic reviews a slice instead of everything. brief warns you when a critic's slice is getting unreadable (raise --critics).
• The seal brief stays bounded. Every blocking objection always reaches the verifiers; long thesis texts and a crowded ledger are clipped with an explicit warning, and the full material is always in the scratch files and in outcome.json.

The runtime is the final arbiter of concurrency: DeepSeek Harness, Claude Code and ZCode each cap how many subagents run at once. A spawn the runtime refuses is recorded as a fallen agent and warned about — never a silent pass. The phase dies and the verdict becomes INCONCLUSIVE when no agent of the group answers, and any fallen seal verifier is INCONCLUSIVE on its own; elsewhere a partial fall is recorded and warned while the debate continues.

---

Why you can trust the verdict

The rollup is code in the body, identical on all three runtimes. It fails closed:

Situation	What a naive summary says	What FormalSwarm returns
outcome: "ok" but exit_code: -1 (never ran)	"green"	INCONCLUSIVE — a check not run is not a check passed
outcome: "ok" with cases: 0	"green"	INCONCLUSIVE — empty green
cases: -1 (the tool counts nothing)	"green"	INCONCLUSIVE — the green is unverifiable
The right number of checks under different commands	"green"	INCONCLUSIVE — coverage is matched by command identity, not counted
A check with an empty command	"green"	INCONCLUSIVE — a check that names no command cannot be reproduced
An empty thesis or revised_thesis	"a thesis"	the writer counts as fallen; the previous state stands
A verifier fell, or the seal is empty	"green"	INCONCLUSIVE — silence is not a vote
Whole antithesis phase failed to answer	"no objections, ship it"	INCONCLUSIVE — a dead phase is not a vote
Verifier claims CONFIRM its checks don't support	"confirmed"	corrected to REVISE/INCONCLUSIVE, recorded as coherence: corrected_by_the_body
Verifier declares REVISE with weak checks	"missing data"	REVISE kept — a testimony of failure is never softened
A check genuinely failed	"mostly fine"	REVISE, quoting the command and the exit code
A critic judged a thesis outside its partition	invisible	tagged out_of_partition, routed correctly, and warned
An objection with no evidence	a finding	tagged unsubstantiated and warned about — an objection without evidence is itself a hallucination

Plus: the budget is refused rather than exceeded; a result folder is cryptographically bound to the brief that produced it — and the binding fails closed, so an unreadable signature stops the run instead of letting one debate eat another's results; labels and phases are restricted to a safe alphabet, so no artefact can be written outside the result folder; and only the orchestrator session may touch production, and only on CONFIRM.

---

Works on any repository

FormalSwarm knows nothing about your language, framework or domain. It profiles the repository it is pointed at:

Stack	Marker	Test command it finds
Python	pyproject.toml, setup.py, requirements.txt, …	python3 -m pytest -q, else python3 -m unittest discover -s tests -v
Node	package.json	the test script through the detected package manager, else npx vitest run / npx jest / npx mocha
Rust / Go	Cargo.toml / go.mod	cargo test / go test ./...
Java	pom.xml / build.gradle	mvn -q test / ./gradlew test
Ruby / PHP	Gemfile / composer.json	bundle exec rspec / composer test
Anything else	Makefile with a test: target, or a bounded content probe	make test, or the stack inferred from the source files

The commands follow the platform the checks will actually run on: python3 on POSIX and python on Win