Sovereignty by Proof: A Defensive Strategy for European AI

Central idea — The race to the AI frontier is lost for Europe. The race to defence is not, and it is necessary whatever the outcome. The ground to take: models that prove mathematically that code holds, against any attacker, including a more powerful AI. That market is structuring itself right now, with hundreds of millions raised in the United States, and without a single visible European actor.

Why now#

The market for AI-driven formal verification moved in 2026 from research to nine-figure rounds. No European actor appears.

Actor	Round	Date	Lead	Approach
Pramaana Labs	$27M (seed)	June 2026	Khosla Ventures	LLM plus a Lean-style verification layer, by sector (tax, law, pharma, cyber)
Axiom	$200M (Series A, $1.6B valuation)	March 2026	Menlo Ventures	Models that produce proofs in Lean, a verified-data loop
Axiom	$64M (seed)	October 2025	—	same

The paradox: Pramaana cites Catala, an INRIA project that formalises the French tax code, as its precedent. The founding research is often French (Rocq, CompCert, Catala, the B method). The industrialisation happens elsewhere.

The window is open, but it is closing: the first to accumulate verified proofs take a lead that compounds.

The reasoning, step by step#

Each step is a distinct claim. If one does not hold, the rest falls: that is where to push.

1. Capability is ahead of use. For most lines of work, today's models are enough; adoption stalls on data, processes and accountability, not on power.
2. The frontier race is therefore justified by national security. The only domain where AI gives an immediate advantage is the digital one, and first of all cyber: no factory, a deployment in hours.
3. That race is lost for Europe. The investment gap with the United States and China is measured in orders of magnitude.
4. Security can be taken from either end. What the race is about is security, and security has two entrances: attack, which is the frontier, and defence. The same stake can be taken from the other end, and Europe has a real advantage there: the founding research in proof is often French (Rocq, CompCert, Catala, the B method).
5. Defence is necessary whoever wins. Even the leading power must protect its own systems. A defensive investment never becomes obsolete, unlike a model that is outdated in six months.
6. Formal proof is a defence that does not depend on the attacker's strength. A proved property holds against any AI, whatever its compute.
7. Proof lends itself to autonomous learning. A verifier decides automatically: the model generates, the verifier sorts, the successes become the next corpus. The scarcity of initial data is a brake, not a wall. This is the step the whole note rests on: if the capacity to prove simply follows general capacity, the lead cannot be taken.
8. It is at European scale. Start from an open code model and post-train it; the compute needed is counted in hundreds of thousands of euros, not billions (order of magnitude, to be confirmed).
9. Defence sells; attack does not. Selling attack means handing someone attack potential: export controls, liability, reputation, a customer base reduced to states. Defence sells to anyone, without an ethical dilemma, recurrently, and regulation creates the demand. A third country looking for a supplier with no allegiance to Washington or Beijing can buy certainty; it cannot buy an offensive weapon without consequences.

What proof covers, and what it does not#

Proof does not close every door. It closes the two most serious ones: remote code execution and privilege escalation.

Attack type	Covered by proof?	Answer
Memory bugs (about 70% of critical vulnerabilities at Microsoft and Chrome)	Yes	Rust, by construction
Hostile inputs, function contracts	Yes	Verified annotations
Cryptography, authentication, kernels, access control	Yes, if stated	Explicit specification
Stolen credential, phishing	Not the cause, yes the propagation	Proved compartmentalisation: the human error stays local
Hijacked business logic (a sequence of individually legitimate operations)	Partially	Depends on the quality of the specification
Compromised upstream dependency	No	Supply chain, out of scope
Denial of service	No	Network capacity; no AI needed to attack

Two structuring limits. Proof protects what is written or rewritten, not the billions of existing lines: on a new, critical system, most doors close; on the existing estate, you nibble. And it covers only the properties that are stated.

The stack: a pragmatic choice, not a dogma#

The invariant of the thesis is automatic verification. The tools will change.

Today the most realistic starting point for code is Rust plus Verus. Rust eliminates memory bugs by construction. Verus, open source, adds proofs written in Rust's own syntax, checked in seconds. Three assets for training: models already know Rust, the verification loop is fast, and published work has already prepared the ground (AutoVerus, KVerus).

Other paths exist and could win. Lean, chosen by Axiom and Pramaana, is more powerful and benefits from a large mathematical corpus. Rocq (formerly Coq) and the B method have proved themselves in industry (CompCert, seL4, line 14 of the Paris metro). Dafny, F*, Kani and Creusot hold intermediate positions.

The tool choice gets revised; the durable asset is the accumulated proofs and the method.

Where the moat is: the specification#

The model that writes the proofs will be commoditised fast. What will not be is the tool that lets an ordinary engineer express what they want to guarantee.

A formal specification does not require a mathematician's level. It is a sentence of the form: if the user does not own the record, the function never returns its content. The difficulty is exhaustiveness (covering the cases nobody thinks of), not theory. A model can precisely propose the forgotten cases.

The moat comes from the loop between the two pieces:

• the tooling captures real use and produces validated specifications and proofs;
• that data improves the model;
• the model improves the tool.

A model's size is caught up in six months. This loop accumulates. The developer's job shifts accordingly: they state guarantees rather than write loops, closer to the architect or the jurist.

What should be done#

For Mistral. Take this position before it closes: a proof model post-trained on an existing code model, and the specification tooling on top. It fits its positioning: specialised models, deployable on site, customers who cannot send their critical code to an American cloud (defence, energy, banking, health). Do not sell software: sell certainty.

For an entrepreneur. The service is reachable right now: make an existing critical codebase verifiable. The asset is the method, not the GPUs. The demand is created by regulation (NIS 2, the European Cyber Resilience Act).

Points to challenge#

This note is written by a non-specialist. The most fragile points:

• The cost of post-training: is the order of magnitude of a few hundred thousand euros realistic for a competitive model?
• The speed of commoditisation: will generalist models become good at proof without specialisation, making the lead useless?
• The choice of language: Verus, Lean, something else? Might the market converge on Lean, where the Americans already lead?
• The existing estate: can old code be made verifiable at a reasonable cost, or does it all have to be rewritten?
• Real demand: will customers pay for a formal guarantee, or will regulatory compliance be enough without proof?

Sources#

• Axiom raises $200M (SiliconANGLE, March 2026)
• Pramaana Labs raises $27M (TechCrunch, June 2026)
• Verus, official repository
• AutoVerus (ACM)
• KVerus (arXiv, May 2026)
• Catala (INRIA)