Towards Multi-language Program Verification for AI
Raúl Raja CTO at Predictable Machines
David Mazarro Founding Engineer at Predictable Machines
2026
Instructions
Both of us on stage; Raúl opens.
Say
Hi, we are Raúl and David, from Predictable Machines. Today we have five stops: why tests are not enough, how types already verify your code, what dependent types add, how to verify many languages at once, and what AI changes.
Testing shows the presence of bugs, but never their absence
How many test cases would it take?
Sometimes, testing could rule out bugs if you test all possible inputs, but:
Function
Possible inputs
Test all inputs?
and(Bool, Bool): Bool
2 \times 2 = 4
yes
multiply(Int32, Int32): Int32
2^{32} \times 2^{32} \approx 1.8 \times 10^{19}
impractical
toUpper(String): String
\infty
impossible
A sea of inputs
unit tests check individual inputs some buggy input a property covers some behavior but some bugs can still go unnoticed a complete specification covers all behavior
For any given program, you have a sea of possible inputs and expected behaviors
Instructions
No steps. Let the picture sink in; the next slide starts testing it.
Say
Take any program. Every dot here is a possible input, and for each one there is a behavior we expect. That is a sea of inputs and behaviors.
Testing doesn't cover all behavior
unit tests check individual inputs some buggy input a property covers some behavior but some bugs can still go unnoticed a complete specification covers all behavior
Instructions
Four steps: the tests, a bug, a property that covers it, a bug outside the property. Name each one as it appears.
Say
Each dot is an input. Our tests check a handful of them, and they all pass. But here is a bug, in an input nobody tested. A property covers some behavior, a whole region of inputs at once, so it catches this bug. But here is another one, outside that region, and the property says nothing about it.
What is formal verification?
“Formal verification prove correctness formal specification
Correctness : a program is correct if it behaves as expected
Prove : use mathematical techniquesthese are the famous formal methods! to guarantee this correctness
…
so what about formal specification ?
Instructions
Go through the three underlined terms.
Say
Three words carry the definition. Correct: it does what we expect. Prove: mathematics, not sampling. And the one that hides all the difficulty, the formal specification, which is the next slide.
What is a specification?
A specification is a description of a program's behavior.
class Account {
// ...
withdraw(amount: number) {
this.balance -= amount;
this.history.push({
withdrawn: amount,
balanceAfter: this.balance,
});
if (amount >= 1000) {
this.flaggedForReview = true;
sendEmail(this.owner, "Large withdrawal");
}
db.accounts.save(this);
}
}
“If amount does not exceed acc.balance, acc.withdraw(amount) subtracts amount from the balance , records the withdrawal in acc.history and saves the account . If amount is 1000 or more, it sets acc.flaggedForReview and emails the account holder. The balance never goes negative. ”
Instructions
Five steps. Each highlights some lines and the clause of the specification they implement; the last one highlights the whole method.
Say
Let's read the code and the sentence together: subtracting, recording, flagging and emailing, saving. Each clause maps to some lines. But “the balance never goes negative” is not about any single line: it is an invariant of the whole method, and it is what tests are worst at. Keep this account in mind, we use it all the way through.
Formal specifications through Hoare logic
Hoare logic (C. A. R. Hoare, 1969) is a logical framework useful for describing what a program does from what must hold before and after it runs.
\{\,P\,\}precondition Cprogram \{\,Q\,\}postcondition
If the precondition P holds before running the program C, the postcondition Q holds after.
Instructions
Skip the inference rules.
Say
Hoare logic is a way to reason about programs, and all we need from it is this triple: a precondition, a command and a postcondition. If the precondition holds before running the command, the postcondition holds after.
Popping a stack
For a stack s, s.pop() throws an exception when s is empty.
\hoare{\texttt{s.size()} = n,\ n > 0}{\texttt{s.pop()}}{\texttt{s.size()} = n - 1}
n is the size before the call.
Instructions
Read the triple left to right, and stop on n > 0: that is what rules out the exception.
Say
A small one first. pop throws on an empty stack. The precondition says the stack has n elements and n is more than zero, so the throw never runs. The postcondition says one element is gone, and n lets it talk about the size before the call. Verification tools treat a possible exception as a failure, so proving this triple also proves this call cannot throw.
Function contracts
class Account {
// ...
withdraw(amount: number) {
this.balance -= amount;
this.history.push({
withdrawn: amount,
balanceAfter: this.balance,
});
if (amount >= 1000) {
this.flaggedForReview = true;
sendEmail(this.owner, "Large withdrawal");
}
db.accounts.save(this);
}
}
Partial withdraw contract
“If amount does not exceed acc.balance [...] the balance never goes negative.”
\begin{gathered} \{\,\texttt{amount} ≤ \texttt{acc.balance}\,\} \\ \texttt{acc.withdraw(amount)} \\ \{\,\texttt{acc.balance} ≥ 0\,\} \end{gathered}
Instructions
The same method as on the specification slide, now with a triple about it.
Say
Back to our account. If the amount does not exceed the balance, then after withdrawing, the balance is not negative. A triple like this is a contract. Design by contract in Eiffel, JML for Java, Dafny: same idea.
Verification tools
Instructions
This diagram comes back later; take a moment on it.
Say
Two languages go in: one for the program, one for the specification. The verification tool reasons about both and tells us whether the program matches. If it does not, we fix the program.
Formal verification covers all behavior
unit tests check individual inputs some buggy input a property covers some behavior but some bugs can still go unnoticed a complete specification covers all behavior
Instructions
The inputs from the testing slide again, with one step: the complete specification.
Say
Back to our inputs. A complete specification covers all behavior, every input, and the verification tool checks it, so neither bug can hide, not even the one the property missed.
How this translates to functional programming
Types and values
Bool
true
false
String
"λ"
"Málaga"
""
Int
…
−1000
−2
−1
0
1
2
3
42
1000
…
3 : Int
{ balance : Int // balance ≥ 0 }
balances that never go negative
Instructions
One view, no steps: 3 : Int first, then the balance subtype.
Say
Types are sets of values, and writing 3 : Int is a claim the compiler checks. A type can also say something about the value: not just an integer, but an integer that is at least zero. Those are our balances, and they come back later as a return type.
Logic as types: the Curry-Howard correspondence
Logic
Type (in Lean)
As a program
P \wedge Q
P × Q
a pair
P \vee Q
P ⊕ Q
one or the other
P \to Q
P → Q
a function
\top
Unit
always constructible
\bot
Empty
impossible to construct
\neg P
P → Empty
no way to build a P
proof of P
p : P
a program of type P
Instructions
Read the last row slowly: it is the punchline.
Say
Propositions are types and proofs are programs. A function from P to Q is a proof that P implies Q. So writing a well-typed program is proving a theorem. Notice that “for all” and “there exists” are missing; we come back to them.
So the type system of your statically typed language is indeed a formal verification tool !
But it is missing something…
const acc = new Account(100);
acc.withdraw(30); // balance: 70
acc.withdraw(60); // balance: 10
acc.withdraw(50);
acc.balance ≥ 0 is violated: the balance is −40
Instructions
Point at the last call.
Say
The compiler is happy, the bank is not. Every call is well-typed, but after withdrawing 30 and 60 the balance is 10, and withdrawing 50 more leaves it at minus 40. The property we care about depends on the value of the argument, and that is exactly what dependent types can talk about.
Introduction to dependent types
Dependent types
inductive Vec ( α : Type ) : Nat → Type where
| nil : Vec α 0
| cons : α → Vec α n → Vec α ( n + 1 )
def Vec.head : Vec α ( n + 1 ) → α
| .cons x _ => x
The empty case is impossible, and Lean proves it for us.
Instructions
One view, no steps: point at the type, the constructors, then head.
Say
The classic example. The length of the vector is part of its type, and each constructor says what it does to it. head only accepts a vector of length n plus one, so there is no empty case to handle: no Option, no exception. Lean proves that case impossible for us.
Types are specifications
def Account.withdraw ( acc : Account ) ( amount : Nat )
( h : amount ≤ acc . balance ) :
{ new : Account // new . balance ≥ 0 } :=
let newBalance := acc . balance - amount
let tx : Transaction :=
{ withdrawn := amount , balanceAfter := newBalance }
let new : Account :=
{ balance := newBalance
history := tx :: acc . history
lowBalanceAlert := newBalance < 50 }
⟨ new , by acc : Account amount : Nat h : ↑ amount ≤ acc . balance newBalance : Int := acc . balance - ↑ amount tx : Transaction := { withdrawn := amount , balanceAfter := newBalance } new : Account := { balance := newBalance , history := tx :: acc . history , lowBalanceAlert := decide ( newBalance < 50 ) } ⊢ new . balance ≥ 0 show newBalance ≥ 0 acc : Account amount : Nat h : ↑ amount ≤ acc . balance newBalance : Int := acc . balance - ↑ amount tx : Transaction := { withdrawn := amount , balanceAfter := newBalance } new : Account := { balance := newBalance , history := tx :: acc . history , lowBalanceAlert := decide ( newBalance < 50 ) } ⊢ newBalance ≥ 0 ; omega All goals completed! 🐙 ⟩
The precondition is an argument; the postcondition is the result's type.
Instructions
Three steps: precondition, postcondition, proof.
Say
The Hoare triple from before, now in one signature. The precondition is an argument, so you cannot even call withdraw without a proof that the amount fits. The postcondition is the result type, and omega proves the arithmetic.
Contracts as theorems
def withdraw ( acc : Account ) ( amount : Nat ) : Account :=
let newBalance := acc . balance - amount
let tx : Transaction :=
{ withdrawn := amount , balanceAfter := newBalance }
{ balance := newBalance
history := tx :: acc . history
lowBalanceAlert := newBalance < 50 }
theorem withdraw_nonneg ( acc : Account ) ( amount : Nat )
( h : amount ≤ acc . balance ) :
( withdraw acc amount ) . balance ≥ 0 := by acc : Account amount : Nat h : ↑ amount ≤ acc . balance ⊢ ( withdraw acc amount ) . balance ≥ 0
grind [ withdraw ] All goals completed! 🐙
The function is plain code; its contract is a separate theorem.
Instructions
Four steps: the function, the precondition, the postcondition, the proof.
Say
Or we keep the function as plain code and state its contract as a separate theorem, proved once by grind. This style scales to code we did not write: we cannot change a Java signature, but we can state a theorem about its translation.
Hoare triples in Lean
def withdraw ( amount : Nat ) : StateM Account Unit := do
let acc ← get
let newBalance := acc . balance - amount
let tx : Transaction :=
{ withdrawn := amount , balanceAfter := newBalance }
let new : Account :=
{ balance := newBalance
history := tx :: acc . history
lowBalanceAlert := newBalance < 50 }
set new
Instructions
Four steps on the theorem: precondition, command, postcondition, tactics.
Say
We can also write Hoare triples directly, over the same do-notation you would write anyway. vcgen turns the triple into verification conditions, and grind discharges them.
Logic as types: the Curry-Howard correspondence
Logic
Type (in Lean)
As a program
P \wedge Q
P × Q
a pair
P \vee Q
P ⊕ Q
one or the other
P \to Q
P → Q
a function
\top
Unit
always constructible
\bot
Empty
impossible to construct
\neg P
P → Empty
no way to build a P
proof of P
p : P
a program of type P
\forall x : A,\ P(x)
∀ x : A, P x
the result type depends on the argument
\exists x : A,\ P(x)
∃ x : A, P x
a value, paired with evidence about it
Instructions
Point at the two tinted rows.
Say
These are the two rows we were missing. “For all” is a dependent function, like Vec.head. “There exists” is a dependent pair: a value with evidence about it, like the subtype withdraw returned. With these two, the type system can state the specifications from the start of the talk.
Hoare triples and dependent types
\{\texttt{amount} ≤ \texttt{acc.balance}\}\ \texttt{acc.withdraw(amount)}\ \{\texttt{acc.balance} ≥ 0\}
def withdraw ( acc : Account ) ( amount : Nat )
( h : amount ≤ acc . balance ) :
{ new : Account // new . balance ≥ 0 }
def withdraw ( acc : Account ) ( amount : Nat ) :
Account
theorem withdraw_nonneg ( acc : Account ) ( amount : Nat )
( h : amount ≤ acc . balance ) :
( withdraw acc amount ) . balance ≥ 0 acc : Account amount : Nat h : ↑ amount ≤ acc . balance ⊢ ( withdraw acc amount ) . balance ≥ 0 All goals completed! 🐙
Instructions
One view, no steps: point at the precondition, the command and the postcondition in each of the three.
Say
The same contract, three ways. As a Hoare triple. As a dependent type, where the precondition is a hypothesis the caller has to provide and the postcondition is the return type. And as a theorem about a plain function, with the contract outside it.
The type checker as the verification tool
def append : List α n → List α m → List α ( m + n )
| .nil , ys => ys
| .cons x xs , ys => .cons x ( append xs ys )
Instructions
Compare it with the “Verification tools” diagram.
Say
Remember the verification tools diagram? Here the specification and the program live in one language, and the verification tool is the type checker: if the program does not match its type, it does not compile.
A language with a dependent type system like Lean gives us a super powerful formal verification tool “for free”
Instructions
Read the slide, wait for the laugh, then say the rest.
Say
And by “for free” we mean Leo, Sebastian and everyone else at the Lean FRO putting in the hard work.
Not only Lean
Lean is the hot thing in this field, but there are others:
Instructions
Hand over to Raúl at the end.
Say
Lean is the hot thing in this field, but not the only one: Agda, Idris and Rocq have been doing this for years. Raúl will tell you why we picked Lean.
“Solving” formal verification for different programming languages
One verification tool per language?
Java Kotlin TypeScript C# JavaScript Null safety Bounds & overflow Contracts A tool for each language 5 × 3 = 15 integrations A tool for a common language, and translate to it
5 + 3 = 8 integrations Verification tool, e.g. Lean Intermediate representation functions · branches · calls · effects · types High-level languages many constructs, many semantics Lower level a common semantic ground One verifier for every language above IR Java Kotlin TypeScript C# JavaScript Null safety Bounds & overflow Contracts
Instructions
Three steps: one tool per language, then one common language, then the morph into layers.
Say
Option one: a verification tool per language, so every analysis times every language. Five languages and three analyses is fifteen integrations. Option two: translate every language into one common language and build each analysis once: eight. That common language is an intermediate representation: lower level than the languages above it, a common semantic ground, with one verifier below it.
Why Lean
An expressive programming language and type system in the same package : huge flexibility to try different approaches to these problems
Ready-to-use building blocks , such as vcgen
Extensibility : teams can mold and shape its capabilities to their needs
def withdrawAll ( amounts : List Nat ) :
StateM Account Unit := do
for a in amounts do
withdraw a
theorem withdrawAll_spec ( amounts : List Nat ) :
⦃ fun ( acc : Account ) => amounts . sum ≤ acc . balance ⦄
withdrawAll amounts
⦃ fun _ acc => acc . balance ≥ 0 ⦄ := by amounts : List Nat ⊢ ⦃ fun acc => ↑ amounts . sum ≤ acc . balance ⦄ withdrawAll amounts ⦃ fun x acc => acc . balance ≥ 0 ⦄
vcgen [ withdrawAll , withdraw ] invariants
· fun _ rest _ acc => rest . sum ≤ acc . balance
with finish All goals completed! 🐙
Instructions
Go through the three points; for the second, point at the proof.
Say
Three reasons. Lean is a real programming language and a logic in one package, so we can try very different approaches to the same problem. It comes with building blocks: here vcgen proves that withdrawing a whole list of amounts never makes the balance negative, as long as they add up to no more than it, from a one-line loop invariant: the amounts still to withdraw fit in the balance. And it is extensible: teams can mold it to their needs.
Our current approach for Predictable Code
Source
Compiler front end
Common IR
Engines
Verdicts
Java
Kotlin
TypeScript
C#
Spoon on Eclipse JDT
K2 compiler plugin
tsc
Roslyn
Predictable
IL
IL deciders
structural facts
Lean + SMT
to discharge proof obligations
Witness
runs a test in the source language
verified
violated
with a counterexample
as a runnable test
We are still figuring out what works best for us and our partners
Instructions
Walk the columns from left to right.
Say
We do not write parsers: each language is read by its own compiler, so names and types resolve the way the language resolves them. Everything meets in one intermediate language. Three engines work on it: deciders for structural facts, Lean with SMT for proof obligations, and a witness that runs tests. Every requirement ends up verified or violated. And we are still figuring out what works best.
Typical challenges, and where AI changes the picture
With AI: faster development, but less reliable outputs
time
code
written
checked
AI assistants
written
checked
the gap
A more pressing need to tackle formal verification challenges
Instructions
Say it is a sketch, not data. Two steps: the curves after AI assistants, then the gap with the line under it.
Say
This is a sketch, not data. AI makes writing code much faster, but review is done by people, and people do not scale with tokens. The gap between code written and code checked keeps growing, and that is what we want verification to close.
Formal verification is still incredibly hard, even with AI
Requirement
“The balance never
goes negative.”
LLM
autoformalization
Formal specification
∀ a, a.balance ≥ 0
Lean
the kernel checks the proof
checked by the kernel
nothing checks that the specification says what we meant
Autoformalization does not solve much if you want to be hands-off: results cannot be trusted blindly.
Instructions
One view, no steps: first what the kernel checks, then what nothing checks.
Say
Even with AI, formal verification is hard. The kernel checks that the proof matches the specification. But nothing checks that the specification says what we meant, and a proof of the wrong theorem is still a proof. So autoformalization does not solve much if you want to be hands-off.
Where it gets better: maintenance
Maintenance of projects is way easier now.
PROOFS
The code changes
A proof breaks
AI proposes a fix
The kernel
re-checks it
a wrong fix does not check
LANGUAGE INTEGRATIONS
A language changes
Its integration breaks
AI updates it
The tests
re-check it
a wrong update fails the tests
Instructions
Proofs first, then language integrations.
Say
Where AI does help a lot is maintenance. When the code changes and a proof breaks, repairing it is a task models are good at, and a wrong repair simply does not check. The same goes for one integration per language: when a language changes, AI updates its integration, and the tests catch a wrong update.
Towards formal semantics
Formal semantics at the different layers of the pipeline allow for provably correct translations between software representations.
Source program
translate
IR
translate
Lean
semantics
semantics
semantics
⟦ source ⟧
⟦ IR ⟧
⟦ Lean ⟧
≈
≈
proved equivalent
proved equivalent
Instructions
One step: the semantics of each layer and their equivalences.
Say
Today every translation in a pipeline like ours is trusted code. If each layer has a formal semantics, each translation can be proved to preserve it, and those proofs compose from the source program down to Lean.
Semantics Done Quick
Semantics Done Quick, a project by Oath Technologies FRO:
We want to build semantic models fast, with AI doing most of the work, and trust the results in high-stakes settings.
“A desugaring function maps surface programs into core programs.”
“We validate against the reference implementation by randomised differential testing on a fuzzed corpus of programs.”
“Human expert attention is reserved for the hard design judgements where AI is unreliable.”
Instructions
Credit Mike Dodds and Oath.
Say
Writing formal semantics used to take expert teams years. Semantics Done Quick proposes letting AI agents write them in Lean, and earning trust by testing them against each language's real implementation.
Granularity of specifications vs. verifiability
generality
verifiability
index in bounds
no null dereference
balance ≥ 0
withdrawals are recorded in order
large withdrawals are flagged
“the bank is fair”
?
what we want
Instructions
The axes first; then the curve with the green points, the orange points, the red point, and the empty corner.
Say
Specific properties, like an index in bounds, are easy to verify but say little. The more general a requirement, like “the bank is fair”, the less verifiable it is as stated. What we want, general and verifiable, is the empty corner.
There is no reliable, hands-off approach to turn natural language requirements into formally verifiable requirements
Automation
Verifiability
fully hands-off
not possible
At Predictable Machines, we are navigating this spectrum to find practical verification solutions for our partners
Automation
Verifiability
fully hands-off
not possible
Takeaways
Takeaway to be written
Takeaway to be written
Takeaway to be written
Raúl Raja CTO at Predictable Machines
David Mazarro Founding Engineer at Predictable Machines
2026
