Input Output Show Blaster wey fit verify Cardano smart contract

Cardano Community don publish presentation of Blaster, one automated verification tool wey dem design to check whether Cardano smart contracts dey follow specified rules. Input Output engineers Romain Soulat and Jean-Frédéric Etienne show how the tool dey examine those properties and fit produce counterexample if e find violation. Dem still discuss ongoing work on proof reconstruction and ways to make results easy to inspect.

Defining Wetin Cardano Contract Suppose Do

Smart contracts dey set conditions for blockchain transactions and dey determine how applications go handle assets. Developer fit specify, for example, say na only authorized user fit unlock funds wey contract hold. Formal verification dey use mathematical methods to check whether system satisfy properties wey dem write for specification. While normal test dey examine selected cases, formal verification dey aim to establish whether stated property hold across the cases wey model cover.

Soulat, technical lead for Cardano High Assurance, explain say Blaster dey automate plenty of the proof work. Developers still need define the behavior wey dem wan check and provide the correct specification. When the tool find violation, e fit produce counterexample make person inspect am. Soulat describe transaction or sequence of transactions wey fit show person wey no be authorized user dey unlock one output.

How Blaster Dey Check Contract Properties

Blaster dey use Lean 4, one system for expressing mathematical statements and working with proofs, together with automated solver. E first simplify the problem; if the property no resolve during that phase, the remaining problem fit go the solver. To make the checks relevant to Cardano, the team don formalize parts of the environment wey contracts dey run inside, including script execution and transaction rules.

Etienne, senior formal methods engineer, outline three possible results: property fit report as valid, falsified, or undetermined. Counterexample wey join falsified result fit help developers identify contract bug, missing assumption, or error for the specification. Undetermined result mean say the solver never establish whether the property hold. The scope of any check depend on the properties wey developers choose to express.

[NEWSBREAK]

Proof Reconstruction Dey Under Development

Developers fit compile contracts wey dem write for languages like Plinth, Aiken, or Plutarch into Untyped Plutus Core, the representation wey Cardano scripts dey use to execute. Dem fit then import the compiled code enter Lean 4 and specify the properties to check. Input Output don release two open-source libraries before wey provide the Cardano-specific models for this process. For earlier demonstration, the team use the pipeline for practice contract from one security challenge, generate transaction context wey show how the contract fit dey exploited.

Etienne explain say proof reconstruction still dey development. The aim na to allow Lean independently check evidence wey support valid result; the current tool never dey produce reconstructed Lean proof when the solver return that result. Soulat still outline plans for clearer counterexample views, to allow developers inspect the transaction details wey dey behind failed property.