cardano-blaster v0.2.1

The native Lean CLI now exports Haskell counterexamples directly:

cardano-blaster check plutus.json assurance.json

For a falsified property with confirmed UPLC replay, the terminal shows the Haskell input values and the path to counterexamples/CounterexampleN.hs. The JSON report binds the generated file by SHA-256 and records the source inputs, call targets and argument indices.

The exporter supports primitive values, lists, pairs, options, Plutus Data, and the explicit V3 ScriptContext, TxInfo and ScriptInfo codecs. Exported contexts must match the replayed Data argument exactly. The generated Haskell program decodes with the real plutus-ledger-api instances and checks the exact Data round trip.

Source generation requires no Python or Haskell compiler. The report records compilation: not-run; compiling and running the generated module is an independent, optional check. Unknown types, incomplete values, unfinished replay and mismatched contexts are reported as unavailable without changing the SMT verdict.

Validation:

• Native Linux and macOS release CI passed all 44 true properties, both typed/replayed counterexamples and Haskell source export checks, with development tools blocked on PATH.
• Both example Haskell exports compiled and ran locally with GHC 9.6.7. A separate renderer fixture validated the three V3 codecs, Unicode escaping, bytes, empty lists and options against the real Plutus API.
• macOS builds use a supported macOS 15 runner and explicitly target macOS 14.

Download the Linux x86-64 or macOS ARM64 archive and its matching checksum file. Verify and extract it, keeping the extracted directory together:

shasum -a 256 -c cardano-blaster-PLATFORM.tar.gz.sha256
tar -xzf cardano-blaster-PLATFORM.tar.gz
cd cardano-blaster
bin/cardano-blaster check examples/auction-counterexample/plutus.json examples/auction-counterexample/assurance.json --refresh-environment

The deliberately false Auction claim exits with code 1. The archive includes the executable, Lean modules, Z3 and examples. Verification remains bounded SMT/CEK checking; it does not reconstruct Lean proofs or establish ledger acceptance or execution budgets.

Haskell export documentation · Release CI

cardano-blaster v0.1.0

Native Lean 4 CLI for checking a compiled Plutus blueprint and its assurance:

cardano-blaster check plutus.json assurance.json

Download the archive for Linux x86-64 (Ubuntu 24.04 / glibc 2.39+) or macOS ARM64 (macOS 14+), and its matching .sha256 file. Verify and extract it:

shasum -a 256 -c cardano-blaster-PLATFORM.tar.gz.sha256
tar -xzf cardano-blaster-PLATFORM.tar.gz
cd cardano-blaster
bin/cardano-blaster check examples/game/plutus.json examples/game/assurance.json --refresh-environment

Keep the extracted directory together. It includes the native executable, the compiled Lean modules, Z3 5.3.1, licenses and examples. Using it requires no Python, Lean/Lake installation, Git or C/C++ compiler. All three verification libraries are pinned to exact commits.

The release tests verify 44 properties across Game, parameters, recursive schemas and Auction, and confirm two typed counterexamples by replay against compiled UPLC. They also cover strict environment rechecking, input rejection, unsupported claims, runtime integrity and worker deadlines. Both platforms run from a relocated distribution with development tools blocked on PATH.

Verification uses Blaster's SMT results and the declared CEK execution bounds. This release does not reconstruct Lean proofs or establish ledger acceptance or CPU/memory budgets.

Usage and source builds · Exact runtime pins