smesh-devteam

LLMs propose · machines adjudicate · humans ratify

---

An orchestrator for an elite software team whose members are language models, built on the SMESH signal mesh.

It is not a prompt library. Three rules are enforced by the type system, so no amount of clever prompting routes around them:

1. No role holds two of the three powers. A role that could both author a claim and bless it cannot be constructed.
2. A ticket without a machine-checkable invariant cannot exist. The tool contract rejects a wish before it becomes a signal.
3. A ticket cannot be discharged without a gate report covering its own obligation. There is no other constructor for the discharged state.

Why the adjudicator is not a model

Verification only means something if the verifier is independent of the proposer. Two language models being independent is an assumption about their training corpora — and for a model shipped under a codename, not even that.

A language model and cargo mutants being independent is a fact about the tool.

So LLM adversaries file findings, and only deterministic gates block a merge:

fmt → clippy -D warnings → test → TLC → property → DST replay → mutants @ 0 survivors

Cheap rungs run first and short-circuit the rest. A rung that did not run is recorded as Skipped, never as a pass — because a report that is silent about a gate has not cleared it, and that distinction is the difference between a green badge and a checked invariant.

A ticket is a proof obligation

use devteam_kernel::{Gate, Ticket};

// Rejected: an invariant that restates the title discharges nothing.
Ticket::propose("Add a ring buffer", "add a ring buffer", Gate::Property, "Architect")
    .unwrap_err();

// Accepted: a property a machine can falsify, and the gate that falsifies it.
let ticket = Ticket::propose(
    "Bounded ring buffer",
    "len never exceeds capacity, and dequeue on empty returns None",
    Gate::Mutants,
    "Implementer",
)?;

Tickets live in a SMESH field as signals, so they decay. One that no independent role corroborates loses intensity and drops out of the backlog by itself. A proposer cannot corroborate their own ticket — not by repeating it and not by rewording it — which is what makes the count mean anything.

Two proposals converge when they name the same symbols under the same gate. Those symbols are read off the repository's own declarations, so no model decides whether two tickets mean the same thing; a ticket that names nothing concrete converges with nothing and says so.

The roster

Tier	Roles	Power
Intake	Registrar	Propose
Proposers	Architect, Modeler, Reliability, PropertyAuthor, SimulationAuthor, Implementer	Propose
Adversaries	Refuter, ContradictionSentinel, CompletenessCritic	Judge
Stewards	Curator (not an LLM), Human	Ratify

Proposers reason through practitioner lenses — Lamport for the model checker, NASA's Power of Ten for the reliability pass, TigerBeetle-style deterministic simulation for the sim author — but a lens is a prompt, and a prompt is not a guarantee. The guarantees are on the ladder.

Crates

Crate	Contents
devteam-kernel	The constitution: powers, capabilities, tickets, the gate ladder
devteam-gates	Pure command planning plus a thin process runner
devteam-mesh	Tickets as decaying signals, and the tool contract handed to the model

Build

cargo test --workspace
cargo clippy --workspace --all-targets -- -D warnings

# The top rung: zero survivors or it did not pass. Scope and timeout bounds are
# in .cargo/mutants.toml; keep --jobs low, the run is meant to share the machine.
cargo mutants --workspace --jobs 2 --no-shuffle

The TLA+ rung needs tla2tools.jar:

curl -sSfL -o ~/.local/lib/tla2tools.jar \
  https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
export TLA2TOOLS_JAR=~/.local/lib/tla2tools.jar

License

MIT OR Apache-2.0