Input Output (IOG) released two open-source libraries on May 12 that bring end-to-end automated formal verification to Cardano smart contracts for the first time. The tools allow developers to submit a compiled contract and receive either a machine-checked mathematical proof that a property holds or a concrete demonstration of exactly how it can be broken. The release targets Cardano's roughly 672 active ecosystem developers, approximately 276 of whom work full-time in the ecosystem, and carries particular weight for builders in Africa and South Asia, where expensive third-party security audits have historically been out of reach.

What Was Released

The two libraries, PlutusCoreBlaster and CardanoLedgerAPIBlaster, are both written in Lean 4, a proof assistant language used in academic and industrial mathematics. PlutusCoreBlaster is a machine-checked formalization of Plutus Core, including every built-in function and execution semantic, with verification targeting Untyped Plutus Core (UPLC), the specific form that Cardano actually executes on-chain. CardanoLedgerAPIBlaster formalizes the rules Cardano uses to validate transactions. Together they let a developer import a compiled contract into Lean 4, state the properties it should satisfy, and call Blaster to check them.

Critically, verification runs at the bytecode level. Cardano contracts are compiled from higher-level languages like Aiken, Plinth, or Plutarch down to UPLC before they go on-chain. Because Blaster works on that UPLC output, any language that compiles to UPLC is supported without the developer changing their toolchain. More than 75 percent of surveyed Cardano developers currently use Aiken, according to the Cardano Foundation's 2025 Developer Ecosystem Survey, meaning the majority of the ecosystem is immediately compatible.

Under the hood, Blaster pipes expressions through Z3 and CVC5, two widely used satisfiability modulo theories (SMT) solvers. It first tries to optimize the Lean expression aggressively, sometimes resolving a property to True with no solver interaction at all. If that fails, it translates the expression to SMT-LIB format and queries the solvers. In an October 2025 demonstration at the UPLC 2025 Conference at the University of Edinburgh, attended by Philip Wadler and other Plutus language designers, the team verified a mainnet production function exceeding 1,500 lines of UPLC against 14 formal requirements in roughly 10 seconds. The team has also run the full pipeline on a contract from a public security challenge, with Blaster automatically generating a script context that reproduced the exploit.

"For the first time, the full chain from a high-level smart contract source language to a machine-checked property is open to Cardano developers," said Romain Soulat, Technical Lead for Cardano High Assurance Product at IOG.

Why This Matters Beyond the Technology

Formal verification is not new to Cardano. IOG's research teams have maintained an Agda-based specification of Plutus Core for years. What is new is automation. The previous approach required deep specialist knowledge and could not generate counterexamples automatically. The current release is designed to minimize expert intervention by embedding Cardano-specific reasoning directly into the toolchain. Today's public release marks a milestone in a sustained development effort: the team announced a functional prototype in July 2025, held the first public demonstration at the UPLC 2025 Conference in October 2025, and ran an early access program for developers in February 2026 before the general release.

That shift has real financial implications. Security audits from established blockchain audit firms typically cost between $20,000 and $100,000 or more, depending on contract complexity. For developers in Africa or South Asia building applications for local markets, that cost alone can make security assurance impractical. Automated formal verification at the tool level changes that calculus. Lean 4's growing presence in South Asian academic computer science programs, including technical workshops held in Bangalore that have introduced the proof assistant to a new generation of engineers, means the tool's foundations are already familiar to many developers in the region.

The stakes in some of these markets go beyond token losses. Cardano already underpins 80,000 land rights records in Mozambique through Landano, a national carbon credit registry in Tanzania through Thallo, and agricultural provenance tracking for export markets in Nigeria through ZenGate. A smart contract bug in a land registry carries consequences that are harder to reverse than a DeFi exploit.

The release also lands during a concentrated push to expand the African developer base. A $30 million Africa-focused grant program announced in March 2026 drew 180 project submissions from 14 countries in its first week. Developers entering the ecosystem through that program can use formal verification from the start, rather than retrofitting security guarantees later.

Cardano's DeFi ecosystem held between $380 million and $552 million in total value locked (TVL) as of early 2026, placing it around 27th among all blockchains by that metric. With approximately 110,000 daily active addresses and more than 1.3 million ADA staking participants, the scale of value at risk makes accessible, automated security tooling not a luxury but a practical necessity.

What Comes Next

The High Assurance project is funded through Cardano's on-chain treasury via the Intersect governance framework, which means DReps (Delegated Representatives), the on-chain voting delegates who include participants from African and Asian countries, have a direct vote in its continued development. Both repositories are live on GitHub at input-output-hk/Lean-blaster and input-output-hk/smartcode-verifier. The bytecode-level architecture means new languages that compile to UPLC will inherit verification support automatically, without additional toolchain work from language teams.