The LLM never answers. Only proofs do.
Why the only way to let language models build software you can trust is to put a symbolic layer in charge of what they say.
Large language models are extraordinary at one thing and poor at another, and most of the industry is trying to get the second thing out of the first. They are extraordinary at acquiring content: reading a requirement, proposing a model, drafting a function, critiquing a design, at a pace and breadth no team can match. They are poor at guaranteeing any of it. A model's confidence is a property of its output distribution, not of the world. Ask it whether a schema is consistent and it will answer fluently either way.
Software is the domain where that gap costs the most, because software is the one artefact we already know how to reason about exactly. We have had the mathematics for fifty years: type systems, formal specification, model checking, proof. What we have never had is a way to produce the raw material — the requirements, the models, the candidate code — fast enough to be worth proving. Now we do. Which means the question is no longer whether an LLM can write software. It is who gets to decide that what it wrote is true.
Two kinds of intelligence, one rule
Neuro-symbolic AI is often described as a hybrid, as if the point were to blend two techniques. At MLambda it is a division of labour with a single, non-negotiable rule: the neural layer acquires, the symbolic layer decides, and the neural layer never answers.
Inside Turing, our architecture platform, that rule is a component called Thinker. Language models — pluggable, with retrieval — read what a person wrote about their business and propose: here is a persona, here is a command, here is what must never happen twice. Nothing they say is believed. Each proposal passes through a deterministic grammar that formalises it into a controlled language, and a verification gate that admits it only if it is well-formed against the ontology. What is admitted enters a knowledge base; what is not is returned with the reason.
From there, only symbolic machinery runs. Shin, a stratified forward-chaining engine, proves over the admitted knowledge. A proof kernel re-checks every proof it produces — the prover is not trusted either. When a requirement implies something the person never said, the engine derives it and names it as an obligation; it does not ask the LLM to guess. And a symbolic reinforcement learner adjusts what the system believes over time — not by nudging weights but by revising rules whose consequences were refuted.
The output is not an answer. It is a proof, or a refusal with a witness.
Refusal is a result
This is the part that takes people a moment. In a conventional AI pipeline a refusal is a failure mode — the thing you prompt around. Here it is the product working. When Turing's model checker walks every reachable state of a specification and finds the one that violates an invariant, it does not soften the finding or propose a workaround. It sends the counterexample back to the requirements. Nothing goes forward to code. The specification is corrected, the proof is re-run, and only when every safety, liveness and temporal property holds does anything get generated.
That ordering — prove, then build — is the whole difference between a system that is tested and one that is verified. Tests are cases somebody remembered. A model checker does not remember; it enumerates.
What it means for the people who build software
Domain-driven design and distributed architecture are the two things an LLM cannot do on its own. Both require holding a whole system's invariants in mind and deciding what is true across them — exactly the faculty a language model lacks and a symbolic layer has. Turing does not replace the architect. It puts the architect's method — TOGAF's cycle for what exists, Gilb's quantified requirements for what must hold, reactive domain-driven design for what to build — inside the loop, where the LLM cannot skip it.
Describe a system in plain language. Agents gather and validate the requirements. Symbolic AI derives the domain model, the views, the tests and the verification. Only then is the system generated, on an actor runtime, with its tests as obligations the model already implied. The language model gathers. The proofs decide.
That is what we mean by treating software as engineering: a specification is a theorem, an implementation is its proof, and nothing is admitted on faith — least of all by a machine that is very good at sounding sure.
MLambda builds Turing, the Genesis workbench, the Aleph language, the MLambda.Actors runtime and MLambda.Data. See Turing run, read the method, or request a demonstration.