All posts
We built a prototype that verifies a code migration with a proof rather than a test suite. A coding agent rewrites the program in another language, a deterministic translator turns both the original and the rewrite into Lean, and a theorem prover proves the two compute the same result on every input. The translator handles a restricted subset of F# and Python and models their float
s as exact real numbers (ℝ
); it contains no language model, so the Lean is a faithful, inspectable rendering of each source.
This turns code migration into a proof obligation. Rather than hoping the rewrite behaves, you state, as a theorem, that it matches the original on every input, and let a machine settle it: Logos Agent proves the theorem, or finds a counterexample.
Our running example is iCPPI, a portfolio-insurance algorithm. We start from an F# implementation and a Python rewrite written by a coding agent, translate both into Lean with the deterministic translator, state the equivalence theorem, and prove it. The proof was produced by our automated proving system, which decomposes the goal into a blueprint of lemmas and discharges each in Lean; here it ran to some 22,000 machine-checked characters.
1. The problem: “we rewrote it, is it still the same program?” #
Migrations are routine and rarely comfortable. A model that lived in F# gets ported to Python so a data-science team can maintain it; a prototype gets reimplemented in a faster language; an older service is rebuilt on a new runtime. The question is always the same: is the new thing the same as the old thing?
The tools we normally reach for answer a weaker question than the one we're asking:
Tests sample the input space. A green suite says the two programs agree on the inputs you thought to check. The input that breaks the migration is, by definition, the one nobody wrote a test for.Diffing outputs on historical data has the same gap (only inputs that have actually occurred), and can't be run until the rewrite exists and is wired up.Manual code review doesn't scale to a nontrivial algorithm and yields conviction, not proof.
What we want to say is stronger: the new program returns the same answer as the old one for every possible input. That is not a test; it's a
theorem, a statement universally quantified over all inputs. To prove such a theorem you need both programs as mathematical objects in one logic, where “equal on all inputs” is a claim a machine can check. Producing those objects, reproducibly and in a form you can inspect against the source, is what our translator does.
A note on what “same” means here, made precise in §2: we compare the programs as functions over the real numbers, so “same” means same mathematical function, not identical floating-point bit patterns.
2. Why Lean, and why over the reals (ℝ)? #
Our target is Lean 4 with Mathlib, its large library of formalised mathematics. Lean is a proof assistant: you don't assert that two functions are equal, you prove it, and the kernel checks every step. Mathlib matters because a real program does real arithmetic (comparison, division, roots), and Mathlib already has the theory of the reals we need to reason about it.
The second decision is more consequential: we translate to the exact real numbers (ℝ), not to floating point.
- A literal
0.1
becomes theexactreal1/10
, not the nearest IEEE-754 double. No rounding in the model, and no floating-point non-associativity to complicate an equivalence proof. sqrt
,exp
,log
become the genuineReal.sqrt
,Real.exp
,Real.log
, with their real theorems available.
The trade-off, stated plainly: reasoning over ℝ proves algorithmic equivalence, that the two programs implement the same mathematical function, which for most migrations is exactly the question (did we faithfully re-implement the algorithm?). It does not prove bit-for-bit floating-point identity, and the two are genuinely different claims: proving sameness as a function over ℝ is one thing, while proving that two programs agree beneath the target's abstraction, in how they actually compute, is another and much harder.
That lower gap is not something floating point closes for you, even under one standard. IEEE 754 fixes the core operations (addition, multiplication, division and square root are correctly rounded and portable) but deliberately leaves transcendentals such as exp
and log
implementation-defined, so two standard-conforming maths libraries can return results that differ in the last bit for the same input (the “table-maker's dilemma”). Bit-for-bit identity is therefore not even well defined across platforms. Modelling over ℝ steps over that layer on purpose and asks the question a migration usually needs: do the two programs denote the same real-valued function? When the bits themselves are the object of interest, such as a checksum or a fixed-point ledger, you would target machine floats instead.
3. The running example: iCPPI #
iCPPI is a portfolio-insurance strategy: manage an account so it participates in the upside of a risky asset (equity) while never dropping below a protected floor. Each period you mark the account to market, update a high-water mark, compute the exposure the rules permit, and rebalance between equity and bonds, but only when the implied drift is large enough to justify a trade. Details matter, and an off-by-a-period slip is easy to make and hard to catch. Our transcription follows Algorithm 1 of the iCPPI specification.
In our migration story the original code is F#, in a functional style: a recursive loop
that folds over the price list, threading the account state (h, ns, nb, v, b)
through each period. (Excerpt; …
marks elided bindings such as em
, and helper functions rmin
/rmax
/rabs
are defined above it.)
The rewrite is Python, imperative: a for
loop over the price series with mutable state. (Excerpt; …
marks elided inception assignments to nS
, nB
, and the loop's B
, Em
, g
.)
The correspondence between the two is not obvious. They differ in paradigm (recursive fold vs. mutating loop) and in the shape of the computation. The F# loop
rolls the bond factor multiplicatively (b := b * rho
each period from an initial 1.0
), while the Python recomputes it as B = rho ** t
. Those happen to denote the same value, but you have to check that. This is the point: two honest, idiomatic implementations that a human must squint at to trust. Are they the same function? §5 makes that a theorem.
(To reduce notation friction: the same quantities wear different names across the three settings, so Python V0/S/H are F#/Lean v0/prices/h. They denote the initial value, the price series, and the high-water mark respectively.)
4. Deterministic translation, and what it does (and doesn't) buy #
4.1 The pipeline
Both front-ends share one shape. Source text is parsed into a language-neutral JSON AST; a small Lean reader turns that into typed Lean data; an emitter prints Lean, with float
s modelled as ℝ
:
The Python front-end reuses CPython's own ast.parse. The input is
literallyvalid Python (the same file runs under CPython), and we never reimplement Python's grammar; Python's parser is the source of truth. The emitter produces an imperative Lean model (
Id.run do
with let mut
/for
/if
).The F# front-end has no equivalent: F# ships no ubiquitous standalone AST exporter, so we wrote a small tokeniser and Pratt (precedence-climbing) parser for the supported subset. It emits a recursive Lean def
with a match
.
4.2 What the generated Lean looks like
The output is not opaque: it's readable Lean, indented, one definition per source definition. Here are the F# rmin
helper and the head of the loop
fold, exactly as emitted:
You can read it beside the F# and follow the correspondence line by line; this is the inspectability that backs the faithfulness argument. Types map directly: float → ℝ
, int → ℤ
, bool → Bool
, list t → List t
, tuples → ×
. Because F# uses the same operators for float
and int
, the F# translation is driven by the required type annotations: a float
becomes ℝ
, which fixes what every operator on it means. (The decide (…)
wrapper appears because the order on ℝ is noncomputable, so a comparison like a < b
is a Prop
; decide
, under open scoped Classical
, lands it back in Bool
.)
4.3 Two correctness backstops
We don't ask you to take the emitter on faith. Two independent checks stand behind each generated spec.
It type-checks against Mathlib. Building the spec runs it through Lean's elaborator against real Mathlib. A mangled translation, whether a wrong arity, a type mismatch, or a malformed term, won't compile. This rules out a large class of translation errors for free (it does not, of course, catch a translation that is well-typed but semantically wrong).
Proved sanity lemmas. For the helpers we go further and prove the generated Lean means what it should: the F# rmin
/rmax
/rabs
become Lean functions, and we prove they are min, max, and absolute value over ℝ:
This lemma is fully checked, with no sorry
. It's a machine-verified statement that the emitter's rendering of a comparison-and-branch denotes the intended function.
5. Migration by proof: the theorem, and how it was proved #
Here is the payoff.
After translation, both versions of iCPPI are Lean functions with the same signature:
That is six real parameters and a price list in, a (value, high-water-mark)
pair out. (Mechanical point: the F#-generated definitions live under namespace FSharp
, so both icppi
s coexist in one file without a name clash.)
The migration-correctness claim is one theorem. It refers to the actual generated specs, the top-level icppi
from the Python translation and `FSharp.icppi`
from the F# translation, not to a paraphrase:
Read the statement carefully. The variables are universally quantified: the equation holds for every combination of the six parameters and every price list, of any length and any values, including the empty list. No sampling, no representative dataset. It says the F# and the new Python compute the identical (value, high-water-mark)
pair on every input the algorithm could see.
How the proof was produced
We did not write this proof by hand. It was produced by our automated proving system, which attacks a goal by building a blueprint, a directed graph of lemmas that decomposes the theorem, then discharging each node in Lean. For icppi_agrees
the blueprint has three layers:
Leaf lemmas that the two implementations' primitives coincide over ℝ: the F#-generatedrmin
/rmax
/rabs
equal Lean'smin
/max
/abs
. Small, but they must hold for anything above them to.The inductive core, This is the hard part and the crux of the whole migration: it proves that Python'sloopAgrees
.imperativefor
-loop over the price series (a`forIn`
over a numeric range, indexing`S[t]`
at absolute positions, threading a six-field mutable state) computes the same thing, period for period, as F#'srecursiveloop
folding structurally over the tail of the list. Bridging “iterate over indices1 .. n-1
” against “recurse on the tail” is exactly the gap between the two paradigms, and it's discharged by induction on the list. The machine-checked proof term runs to some22,000 characters; no human wrote it.** The top theorem**, which assembles the pieces: the empty and single-element lists reduce directly (both sides return(v0, v0)
), and the general case appliesloopAgrees
with the inception state, rewriting through the leaf lemmas.
Every lemma is checked by Lean's kernel against Mathlib. The value of the blueprint structure is that the intimidating goal (“two whole programs are equal”) becomes a graph of individually-checkable obligations, and the automated prover works the graph until each is closed, using the same divide-and-conquer a human formaliser would, driven by the system rather than by hand.
6. Why this is more than a translator #
Zoom out and a general pattern appears.
The migration recipe. To move a program from language A to language B:
- Translate the original program (F#, here) → Lean spec A.
- Translate the rewrite (Python, here) → Lean spec B.
- Prove
A = B
in Lean. Or, when the rewrite isdeliberatelyallowed to differ, prove arefinementinstead: an implication relating the two under a stated relation, rather than plain equality. - Ship the rewrite carrying a machine-checked certificate.
You can prove properties, not just equivalence. Equivalence is one theorem; it isn't the only one worth having. iCPPI's purpose is a
capital-protection guarantee: the maturity value never falls below its floor β·H
N. That is a theorem about the same generated model, stated directly on
icppi
(and, since the two agree, on FSharp.icppi
too):(Here .2
is the final high-water mark HN and .1
the maturity value VN.) Migration correctness and domain correctness live in the same framework; both are just theorems about the generated Lean.
Cross-language by construction. We've shown Python and F#, but the back-end is specific to neither. Every front-end lowers to the same JSON AST and the same Lean emitter, so adding a source language means adding a parser to a neutral spine; the downstream equivalence machinery is unchanged.
The model is inspectable, and it doesn't drift. A deterministic, readable, type-checked Lean spec is regenerated from source and re-checked, so, unlike prose documentation, it cannot silently fall out of date with the code.