Software that is verified before it is built.
A specification is a theorem. An implementation is its proof. MLambda builds the stack that makes that literal — Turing, an architecture platform where LLM agents turn a plain-language description into a formal model, check it, and generate the system that follows; Aleph, a pure language in which whole classes of defects cannot be written; and a runtime, a database and a UI framework built the same way.
Why it matters
Most software is built first, tested afterwards, and trusted on faith. Generating it faster does not change that.
-
The problem
Defects are found where they are most expensive — in production — because nothing in the process could rule them out earlier. AI code generation raises the volume of code without raising the guarantee on any line of it.
-
The wedge
Verification before construction. Requirements become a formal model; the model is checked for safety, liveness and consistency; the implementation is derived from it and its tests are obligations the model already implies. Agents do the work. Proofs decide.
-
Why now
Language models can finally produce the content — requirements, models, code — at the pace a business needs. What they cannot produce is the guarantee. MLambda supplies the part that is missing: the mathematics that admits or refuses what the model proposes.
A verifiable model
Every MLambda system is checked along four axes before it exists, and built in a language that keeps it that way.
-
Consistency
Proved, not promised
Specifications in Z; models checked in TLA+ for safety, liveness and temporal properties before a line of code. MLambda.Data's consistency model is a checked specification. Aggregates are derived from invariants, so the boundaries that must hold are the boundaries that exist.
-
Security
Refusal is part of the model
Who may act, on what, under which guard, and what is emitted when the guard fails — declared in the domain, not patched in later. Actors isolate state by construction; cluster nodes speak over mTLS; the data gateway authenticates with JWT and routes by role.
-
Performance
Measured against the target
An actor runtime with reactive messaging; a log-structured storage engine with Bloom-filtered reads; Aleph compiled to native code via LLVM with a direct FFI and SIMD. Every generated system carries benchmarks — throughput, latency, allocation — and design estimates are compared with what verification measures.
-
Memory and mutation
Defects with nowhere to occur
Aleph is pure and immutable by default: no shared mutable state to race on, no null, no unchecked failure — errors are typed values, cases are matched exhaustively, effects are explicit. Coordination is software-transactional memory and channels, not locks. The bugs mutable languages spend their lifetimes chasing are not expressible.
Software as mathematics
Aleph has a pure functional core — Hindley–Milner inference, algebraic data types, traits — and it is used as one: MLambda's rendering of Category Theory for Programmers is written in Aleph, each chapter a runnable program whose laws are verified by property tests. The same discipline runs through the stack. A system's invariants are stated as a theorem; the model checker is the referee; the implementation is admitted only as a proof. That is what MLambda means by treating software as engineering: not a metaphor, a method.
- 11Genesis packages on NuGet
- 4public documentation sites
- TLA+checked consistency model
- 17pipeline agents, one per stage
- 2019building since
A system that understands architecture — and builds from it
The idea is older than the company. Years before MLambda existed, its founder was an enterprise architect applying TOGAF by hand — business, application, data, technology — and watching the same thing happen on every project: the architecture was right, and the software still drifted from it, because nothing connected the two except people and time.
The mission became a single sentence: build a system that understands architecture the way TOGAF describes it, expresses each domain as a domain-specific language, and runs it on an actor framework built for reactive domain-driven design — so that the model is not documentation about the software, but the thing the software is generated and verified from.
That is what Turing is. A set of rational tools: domain-specific languages that call on language models to gather and validate requirements, then hand them to symbolic artificial intelligence — an inference engine, a proof kernel, a model checker — to derive the logic, the views, the tests and the verification. The LLM gathers; the symbolic layer decides. Genesis is the workbench the languages are built in; MLambda.Actors is the runtime the domains run on; Aleph is the language chosen so the generated system stays correct after it exists.
This is the application I dreamed of building for many years. I am building it now.
— Roy Gonzalez, founder
- TOGAFthe architecture cycle Genesis runs — vision, business, data, application, technology, governance
- Domain-specific languagesGuimel for the domain, Samek for the specification, Aleph for the program
- Actor frameworkMLambda.Actors — the runtime for reactive domain-driven design
- LLMgathers and validates requirements in controlled language
- Symbolic AIShin inference, a proof kernel and TLA+ derive logic, views, tests and verification
The stack
Products
Two tiers, stated on every page: Open · MIT on NuGet with public documentation, and Commercial · early access with public documentation and source by arrangement.
-
Commercial · early access
MLambda Turing
The architecture platform. Describe a system in plain language; get back one that was verified before it was built.
-
Open · MIT
Genesis
A compiler workbench for building languages — and for verifying what they describe before it exists.
-
Commercial · early access
Aleph
A functional language that reaches the machine directly — C, assembly, LLVM and WebAssembly through a native FFI.
-
Open · MIT
MLambda.Actors
A reactive actor runtime for .NET with supervision, clustering, gossip membership and mTLS.
-
Commercial · early access
MLambda.Data
A distributed database in which every component is an actor — and the consistency model is a checked TLA+ specification.
-
Commercial · early access
MLambda.UI
A reactive MVVM framework that never calls a render method — one view, painted by ImGui, Blazor or Avalonia.
-
Commercial · early access
MLambda.OS
A Minix 3-inspired microkernel for x86-64, specified before it is implemented.
-
Research
Hilbert
A neuro-symbolic transformer that reasons across five systems of logic and learns from each input without retraining.
Built for
Teams for whom a defect is not an inconvenience.
- Financial services and tradingOrder flow, positions and settlement, where latency and fault tolerance are architectural constraints — the founder's background is a mission-critical US trading platform.
- Logistics and supply chainIntegration-heavy systems with many parties and no tolerance for lost messages; the founder's years on DHL's logistics core.
- Regulated and safety-critical softwareAnywhere an auditor asks for evidence. A checked specification and derived tests are the evidence.
- Teams adopting AI code generationKeep the speed; add the guarantee. Turing puts a model checker between the language model and your codebase.
What's next
Direction, not dates. Genesis and Turing's backlog is public — every gap has an epic and an issue.
- TuringExecute the generated end-to-end suites; deepen static analysis; a catalogue of business agents; deployment-verification depth; hardening of the web surface; a second emission target.
- AlephNetworking through the FFI, TLS, a tracing garbage collector, and let-polymorphism for top-level functions.
- GenesisGears promoted to a top-level module; Thinker's deferred capabilities.
Method
Every system here is specified in Z, model-checked in TLA+, and only then implemented — by people or by agents — with the tests derived from the model rather than invented afterwards. How MLambda builds software →
Work with MLambda
- Demonstration — see Turing run on a domain you describe.
- Consulting — architecture and delivery with the MLambda stack.
- Commercial licence and support — for the commercial-tier products and supported use of the open ones.
- Early access — private builds and repositories for teams evaluating the commercial tier.