Input Output Demonstrates Blaster for Cardano Smart Contract Verification

Cardano Community has published a presentation of Blaster, an automated verification tool designed to check whether Cardano smart contracts follow specified rules. Input Output engineers Romain Soulat and Jean-Frédéric Etienne demonstrate how the tool examines those properties and can produce a counterexample when it finds a violation. They also discuss ongoing work on proof reconstruction and ways to make results easier to inspect.

Defining What a Cardano Contract Must Do

Smart contracts set conditions for blockchain transactions and determine how applications handle assets. A developer might specify, for example, that only an authorized user can unlock funds held by a contract. Formal verification uses mathematical methods to check whether a system satisfies properties written in a specification. While a conventional test examines selected cases, formal verification aims to establish whether a stated property holds across the cases covered by the model.

Soulat, technical lead for Cardano High Assurance, explained that Blaster is intended to automate much of the proof work. Developers still need to define the behavior they want to check and provide the corresponding specification. When the tool finds a violation, it can produce a counterexample for inspection. Soulat described a transaction or sequence of transactions that could show someone other than the authorized user unlocking an output.

How Blaster Checks Contract Properties

Blaster uses Lean 4, a system for expressing mathematical statements and working with proofs, alongside an automated solver. It first simplifies the problem; if the property is not resolved during that phase, the remaining problem can be sent to the solver. To make the checks relevant to Cardano, the team has formalized parts of the environment in which contracts run, including script execution and transaction rules.

Etienne, a senior formal methods engineer, outlined three possible results: a property can be reported as valid, falsified, or undetermined. A counterexample associated with a falsified result can help developers identify a contract bug, a missing assumption, or an error in the specification. An undetermined result means the solver has not established whether the property holds. The scope of a check depends on the properties developers choose to express.

[NEWSBREAK]

Proof Reconstruction Is in Development

Developers can compile contracts written in languages such as Plinth, Aiken, or Plutarch into Untyped Plutus Core, the representation used to execute Cardano scripts. They can then import the compiled code into Lean 4 and specify the properties to be checked. Input Output previously released two open-source libraries that provide the Cardano-specific models for this process. In an earlier demonstration, the team used the pipeline on a practice contract from a security challenge, generating a transaction context that showed how the contract could be exploited.

Etienne explained that proof reconstruction is still in development. The aim is to let Lean independently check evidence supporting a valid result; the current tool does not yet produce a reconstructed Lean proof when the solver returns that result. Soulat also outlined plans for clearer counterexample views, allowing developers to inspect the transaction details behind a failed property.