Migrating Code by Proof: From F# to Python

A team built a prototype that verifies code migration from F# to Python using a proof in the Lean theorem prover, rather than relying on tests. The system translates both the original and rewritten code into Lean, then proves they compute the same result for every input, demonstrated on a portfolio-insurance algorithm called iCPPI. This approach turns migration into a formal proof obligation, ensuring algorithmic equivalence over real numbers.

All posts /news/ 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 the exact real 1/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 genuine Real.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 literally valid 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 -generated rmin / rmax / rabs equal Lean's min / 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's loopAgrees . imperative for -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 's recursive loop folding structurally over the tail of the list. Bridging “iterate over indices 1 .. 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 some 22,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 applies loopAgrees 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 is deliberately allowed to differ, prove a refinement instead: 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.