aaronjmars/proven-tokens: Computer-checked math proofs for 15 Ethereum tokens

An open-source repository provides computer-checked mathematical proofs in Lean 4 verifying the correctness of the exact deployed bytecode for 15 top Ethereum tokens worth about $54 billion. The proofs cover every possible input, caller, and transaction order to validate core guarantees such as supply invariants and owner permissions. Although the verified bytecode ensures that key rules hold across multiple transactions or calls, the project notes named assumptions regarding hash functions and highlights specific owner powers. Open article →