Formal verification, push-button

IOG has released open-source Lean 4 tooling that formally verifies Cardano smart contracts — and finds exploits on its own. Pointed at a public CTF contract, it produced a working double-satisfaction exploit unprompted, without being told what to look for. That is the kind of subtle, context-dependent bug that has historically needed an expert human auditor — charging tens of thousands of pounds — to catch.

The detail worth knowing: it verifies the compiled UPLC that actually runs on-chain, not the source it was compiled from. The compiler stops being a trusted link in the audit chain. You write the validator in Aiken, Plinth or Plutarch, state the properties you want to hold, and get back either a machine-checked proof or a ledger-valid counterexample that demonstrates the exploit.

It lifts the security floor for the whole chain, not just the contracts that could afford a heavyweight audit before. Cheaper, faster, more reliable verification means more serious things can ship on Cardano, with fewer expensive surprises along the way.

It’s the natural next step for a chain that has always done security the slow, peer-reviewed way. The work continues under the 2026 Cardano High Assurance proposal — foundational infrastructure, and worth backing.