Why We're Building Claims Software in Lean

Every large claims program — a class-action settlement, a mass insurance payout, a compensation scheme — eventually comes down to software that decides who gets paid and how much. That software is usually written once, under deadline pressure, and trusted because it was "tested," not because anyone can show it is correct.

We think that is not good enough when the stakes are people's legal rights and their money. So we build our claims-calculation engines in Lean, a proof assistant that lets us state the rules of a settlement or policy precisely and then prove that the software implementing those rules matches the specification — for every claimant, not just the ones we happened to test.

This blog documents how that works in practice: how we turn legal and actuarial language into formal specifications, how we prove the resulting code correct, and what that buys claimants, administrators, and courts in terms of trust and auditability.

We are also using Verso, the same Lean-based tool used to write the Lean documentation itself, to build this site — so the code examples in our technical posts are always checked by Lean before they are published.