Cardano High Assurance
IOG has introduced Blaster, an automated formal verification engine for Lean 4 designed to provide mathematical security guarantees for Cardano smart contracts. Tested on complex protocols like Djed and USDCx, Blaster automatically checks for common vulnerabilities (such as double satisfaction) using a Common Vulnerability Library. IOG leads delivery of this work with six ecosystem partners that each own defined components, aiming to lower the barrier to high-assurance development and foster institutional trust and TVL growth for Cardano's Vision 2030.
