Migrating Code by Proof: From F# to Python — Logos ResearchSkip to content

Research6th July 2026<br>Migrating Code by Proof: From F# to Python

All postsWe 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 floats as exact real numbers (ℝ); it contains no language model, so the Lean is a faithful, inspectable rendering of each source.<br>The end-to-end picture: both implementations become Lean, and a theorem prover certifies they are equal on every input. The coding agent iterates until the proof succeeds.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.<br>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.<br>1. The problem: “we rewrote it, is it still the same program?”<br>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?<br>The tools we normally reach for answer a weaker question than the one we're asking:<br>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.<br>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.<br>Manual code review doesn't scale to a nontrivial algorithm and yields conviction, not proof.<br>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.<br>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.<br>2. Why Lean, and why over the reals (ℝ)?<br>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.<br>The second decision is more consequential: we translate to the exact real numbers (ℝ) , not to floating point.<br>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.<br>sqrt, exp, log become the genuine Real.sqrt, Real.exp, Real.log, with their real theorems available.<br>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.<br>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...