Method

How MLambda builds software

Specified in Z, checked in TLA+, and only then built — by people or by agents — with the tests derived from the model.

Most software is built first and tested afterwards, and the tests are whatever someone thought to write. Everything at MLambda inverts that. A system exists first as a formal specification; the specification is model-checked; the implementation follows from it; and the tests are obligations derived from the model, not guesses about it.

The pipeline

The BEAM pipeline Ten stages in two rows: research, conceptualise, formalise in Z, verify in TLA+, plan; then generate, test with BDD, benchmark, deploy, and measure — with evidence returning to the start. Researchdomain graph Conceptualiseactor topology FormaliseZ specification VerifyTLA+ · TLC Planfive artifact plans Generateactors · data · UI TestBDD from the model Benchmarkthroughput · latency DeployHelm · Kubernetes Measureevidence → gap list measurements return to research — the cycle repeats

Research decomposes a business domain into a knowledge graph of processes, events, data flows, decisions and human roles. Conceptualisation turns that into an actor topology with an explicit supervision hierarchy, human boundaries and interface surfaces. Formation refines colloquial requirements into a purified Z specification. Verification generates an executable TLA+ specification from it and runs the TLC model checker until every safety, liveness and temporal property holds — correction loops go back to Formation, not forward to code. Planning derives five artifact plans — mobile UI, web UI, API gateway, backend, infrastructure. Only then: generation, BDD tests derived from the model, benchmarks, deployment, and measurement whose evidence returns to the research gap list.

Four claims the method rests on

  • A missing requirement is an unfulfilled obligation — deduced from the knowledge base, not guessed by a model.
  • A waiver is a belief, and closes nothing until a scope statement a person wrote grounds it.
  • The aggregation is derivable: an invariant spanning two entities forces them into one aggregate, so the connected components of the invariant graph are the aggregates.
  • Design estimates, verification measures, and the difference between them is what the method learns.

The agentic layer

The pipeline is run by agents. In Turing, a society of agents — a roster, expert agents, code agents — is coordinated by Gears, a build engine that drives declared workflows and writes each agent's report. As a Claude Code plugin, MLambda.Actor.Agent runs the same method with 17 specialised agents, one per stage, from a business description to an actor system deployed on Kubernetes.

What keeps an LLM-driven pipeline honest is the reasoning layer, Thinker. Language models acquire content — through pluggable providers and retrieval — and a deterministic grammar formalises what they propose. A forward-chaining engine proves over the formalised knowledge, a proof kernel re-checks every proof, and a symbolic reinforcement learner improves what is believed over time. The LLM never answers; only proofs do. The method borrows TOGAF for what exists, Gilb's Planguage for what must hold, and reactive domain-driven design for what to build.

The full method is documented in the twelve-chapter method book on genesis.mlambda.net. For the reasoning behind the neuro-symbolic layer, read The LLM never answers. Only proofs do.