Skip to main content

Blog > 2025 > October

Always secure and safer than ever, thanks to next-level smart contract verification on Cardano

Traditional smart contract verification checks high-level code and trusts the compiler. In this second blog post in the formal verification series, we explain how we can verify the actual compiled bytecode that runs on-chain, catching bugs that other approaches miss

14 October 2025 Romain Soulat 12 mins read

Always secure and safer than ever, thanks to next-level smart contract verification on Cardano

It is now possible to formally verify smart contracts at the exact level they execute on Cardano nodes – working directly with Untyped Plutus Core (UPLC) rather than reasoning over abstract models or surface loop. 

By directly targeting UPLC, contracts can be verified regardless of the source language, including Plinth, Aiken, Plutarch, or any future language that targets the…