A new era of smart contract verification on Cardano
A July 16, 2025, blog post by Romain Soulat details a new Input | Output tool for automated formal verification of Cardano smart contracts. Leveraging the Lean4 proof system and SMT solvers, it automatically checks that contracts behave as intended without requiring developers to write manual proofs. This innovation aims to make high-assurance development faster, cheaper, and more accessible, allowing for continuous verification within CI/CD pipelines.
