Rent the capability, own the control

When Mistral released Leanstral, a six-billion-parameter, Apache-licensed model that outperforms far larger and costlier systems on formal proof tasks, the obvious headline was cheaper coding at frontier quality with open weights. All true, and all beside the point. In a regulated enterprise the number that matters is not the price. It is that a perfect verifier changed what the model needed to be, and with it what kind of evidence the software can carry.

The economic flip #

Leanstral writes code in Lean 4, a proof assistant in which a program can carry a machine-checkable proof that it satisfies a specification. Lean accepts the proof or it does not; there is no discretion in the verdict. Once you have a checker that is sound, automatic, and cheap, correctness stops being something the generator must achieve and becomes something you can search for: generate many candidate proofs, discard the failures, keep a survivor. This is why a small model wins: it need not be right, only right once across several cheap attempts, because the verifier does the discriminating. This is a documented regularity rather than a quirk of Leanstral: the generation-verification asymmetry. Because checking a candidate proof is easier than producing one, repeated sampling against a sound verifier lets a small model match one many times its size.

The consequence is larger than any single model. The leverage in verifier-gated generation is the verifier, not the generator. The question stops being “which frontier model do we standardise on” and becomes “where can we build a verifier strong enough to gate what the model produces.” That is not a capability question. It is a control question: the one regulated engineering has always actually been asking.

Two predicates the machine owns, and a third it cannot #

A verifier-gated pipeline answers two questions mechanically. Does this implementation satisfy its specification? Leanstral writes the proof; Lean checks it. Does a proof exist at all? The search terminates or it does not. Both are now cheap, reproducible, and free of discretion. That is a real advance, because verification used to be the expensive, expert, unscalable step.

But there is a third question the machinery cannot reach: does the specification say what we actually meant? No verifier can evaluate that, and the reason is structural. Let the generator write the specification it is graded against and it will drift, reasonably and invisibly, toward specifications it can easily satisfy; the proof returns green and certifies nothing. The specification of intent must be authored outside the system that satisfies it, or the apparatus grades its own homework.

And a green proof is more dangerous than a silent gap, because it reads as assurance. To a risk committee or an auditor, “the proof checks” looks like “the software is correct.” It is not. It means the code conforms to a stated specification, and says nothing about the cases the specification forgot. So the third predicate (is this specification faithful to intent, and complete enough to trust?) cannot be discharged by a signature alone. It needs a review ritual and an explicit coverage statement standing beside every proof. Conformance is not correctness, and a control architecture that blurs the two manufactures assurance the organisation has not earned.

Control is a discipline, not a purchase #

Here the capability framing collapses and the control framing takes over. The tool industrialises the how: the proof, and much of the labour of rendering intent into formal syntax. The human keeps the what: which obligation matters, and whether the formal statement faithfully encodes it. Authoring intent is exploration and stays with people; proving conformance is industrialisation and leaves.

But it is not a one-time act, and this is where most versions of the argument quietly fail. Intent drifts (regulation is amended, a product pivots, an obligation is reinterpreted) while a proof-enforced corpus keeps certifying yesterday’s intent, green forever. Owning the third predicate therefore means owning a standing discipline: revalidating specifications against changing intent, and retiring the ones that no longer hold. Specifications and proofs are themselves code; they rot under refactoring and toolchain drift, and the scarce person who can read whether a formal statement still means what you meant is the one doing the maintenance, not the cheap model. The specification corpus is a maintained asset with a named owner and a lifecycle, or it is a wish. There is no “author once, enforce forever, at no cost.” There is funded, staffed upkeep, or there is decay.

The evidence you already owe #

State it that way and the regulated enterprise gets something better than a cheaper model. A named human attesting that specification S faithfully encodes obligation O is precisely the artefact that accountability regimes already demand and cannot currently obtain for AI-written code. Personal-accountability regimes of the Senior Managers type require a named individual answerable for a control; model-risk governance of the SR 11-7 kind requires effective challenge and ongoing validation; aviation’s DO-178C, through its formal-methods supplement, already recognises formal proof as a means of compliance. None of these is a new burden invented by the architecture. They are obligations the enterprise already carries, and the third predicate is where they can be discharged earlier, and made auditable by construction. The specification corpus becomes the versioned record of who attested intent-fidelity, against which obligation, and when.

One honesty is owed in the same breath: the generator is itself a model. A proof answers “does this code conform to this spec”; it does not validate the system that wrote the spec or the code. Under model-risk expectations, Leanstral is itself a model requiring validation. The architecture closes the code-correctness question and opens a model-risk question in the same move. A strategy that hides the second to sell the first is not one a supervisor will thank you for.

Two things to own #

Ownership of intent is one axis of control, and it is model-independent: you can own the third predicate on a closed, rented endpoint. The stack is the other axis, and it is where sovereignty earns its place on its own merits, not as a rider on the intent argument. A verifier you can inspect, self-host, and audit (whose determinism you can demonstrate and whose availability you do not rent) is exactly what operational-resilience and third-party ICT-risk expectations push toward. That is the case for backing open, sovereign tooling like Leanstral: Apache-licensed weights on your own hardware and an open checker mean the machinery that produces your evidence is itself inspectable and yours. Capability can be rented. Control, and the auditability that rides on it, has to be owned.

What to build around #

None of this is universal. Proof-carrying generation pays only where a formal specification is affordable and worth writing: cryptography, protocols, compilers, financial calculation kernels, safety-critical control, data transforms with hard contracts. And the skill to author a faithful invariant is scarce enough that this is an elite-core discipline, not a lifecycle-wide one. Applied everywhere it collapses; applied to the parts of the estate where an error is expensive enough to justify the specification, it compounds.

But the shape of the bet is now clear, and it is not the one on the press release. The frontier is not more code, faster. It is code that arrives carrying the accountable evidence a regulated enterprise already owes: gated by a verifier you can audit, specified by an intent you own and keep revalidating, running on a stack you control. The capability you can rent. The control, and the accountability that rides on it, you cannot outsource, to any model, at any price. Strategy for AI in the regulated software lifecycle comes down to a single instruction: build around owning it.