Applying formal methods at Input | Output: real-world examples

The previous blog post discussed formal methods and their role in blockchain development.

Building on the importance of formal methods, Input | Output (IO) demonstrates their practical application through real-world examples. By integrating these techniques into the development process, IO ensures robust, high-assurance systems that drive innovation in blockchain technology.

Implementation of formal methods at IO

IO uses formal methods when contributing to Cardano’s development to achieve strong guarantees on the functional and non-functional correctness of the core components of the system.

IO’s strategy involves:

• Getting involved early, at the research stage, working with researchers to formalize results
• Developing formal artifacts (specifications, models, prototypes, and production implementations) that can grow and change with the project
• Tuning the level of formality to the project
• Locking formal methods into the development workflow via continuous integration (CI) and testing
• Staying involved in the late development stages and beyond.

There are three commonly used techniques:

1. Specifications
2. Digital twins/formally verified models
3. Formally verified production code.

Specifications

Writing a specification is essential, as it provides a high-level overview of how the system is intended to function. If you don’t specify how the system is supposed to work, how can you test that it works as expected? Specifications address the system’s design and the key properties and requirements it must meet. For example, in a stablecoin system, a key property would be maintaining the peg. At the same time, in the Cardano ledger, it’s important that ada is not accidentally created or destroyed during regular system operations – a property known as ‘preservation of ada’.

IO’s specifications go beyond mere documentation – they are executable, serving as reference implementations and test oracles to verify the production implementation. IO engineers also prove key properties of the reference implementations, such as preserving ada property. This provides a realistic reference version of the real system or component that is faithful to the original design, capturing fundamental properties. This also ensures that design properties translate into code guarantees.

Digital twins

Often referred to as a digital twin, this setup acts like a clone of the real system, designed to behave identically. This captures the notion of conformance testing that IO engineers use extensively in the Cardano node to rigorously test the code in realistic ‘laboratory conditions’.

Formally verified production code

The next step is using the reference implementation in production, or rather, verifying production code. This requires fully detailed, high-performance, verified code that offers the highest level of assurance. This approach is actively pursued in projects such as Plutus High Assurance, which leverages the Lean theorem prover to verify smart contract code. Plutus Core already benefits from production code verification, where code generated from the Agda theorem prover is used in the production toolchain. The Cardano Foundation also uses agda2hs to verify the wallet production code that hasn’t been deployed yet.

If you’re reading this article using a Chrome-related browser, you’re probably using verified cryptographic code right now – a field that IO is also investigating.

Striking a balance

There is a balance to be struck between how precise methods should be used in different systems or different components. This depends on how critical the component is, what the consequences of failure are, and how amenable the domain is to formal methods. Every project is different. Fortunately, there are various formal method tools and methodologies available, ranging from standalone specifications, property-based testing, model checking, static analysis, and types for theorem proving and formally verified code. The goal is to enable the programmer to fully define the program, its requirements, invariants, and guarantees – and to have them all machine-checked. The level of formality is adjusted based on need and applicability.

Let’s take a look at several examples below.

Figure 1. Example of block diffusion

The figure above illustrates how the size of blocks affects the likely transfer delay across the internet.

The ledger rule example below checks if a transaction is balanced and the inputs are unspent, amongst other things. This rule is formalized in Agda, and it serves as a reference documentation and reference implementation for conformance testing.

Figure 2. Example ledger rule

The machine-verified theorem depicted below shows that the ledger satisfies the preservation of value. It states that the total amount of ada in the system is the same before and after the transaction is processed.

Figure 3. Example theorem – preservation of value

It’s worth noting that formal methods is a rapidly evolving field. What was exotic yesterday is commonplace today. Wherever possible, it is essential to use automated methods and tool support to save time and ensure the strongest possible guarantees.

A few examples of formal methods applied to Cardano

Cardano ledger layer

The Cardano ledger specification has evolved through the Cardano ledger eras, starting with a retrospective LaTeX specification for Byron and progressing in parallel with Shelley development and onwards. For the Conway ledger era, an Agda specification is in use. Formal methods help prove key properties of the ledger, notably ‘preservation of value,’ which ensures that ada is neither accidentally created nor destroyed as the ledger state is updated with each new block. The specification is compiled into a PDF for reading and Haskell for execution. This serves as a reference implementation for conformance testing against the production implementation. To date, this process has yielded no failures.

Plutus Core

There is a formalization of typed and untyped Plutus Core, which serves as a specification and reference implementation. Formal methods engineers prove type preservation and progress properties, ensuring that smart contract execution does not stall and that erasing types does not affect the behavior. Key optimizations on untyped Plutus Core are also verified, with the resulting code integrated into the production compiler. This is especially crucial in areas where the type system offers limited support to compiler developers. Currently, Cardano hosts over 90,000 smart contracts, 160,000 native asset policies, and 700m ada in total value locked (TVL).

The figure below illustrates the internal structure of the intrinsically well-scoped control, environment, and continuation (CEK) machine for untyped Plutus Core.

Figure 4. Plutus Core CEK machine

Cardano network layer

IO uses performance modeling to determine the performance envelope and set Cardano network parameters. Typed protocols ensure precise protocol adherence in implementation, with guarantees provided by the Haskell type system, requiring no additional proofs. The network layer has maintained over 2,200 days of uninterrupted uptime.

Agda2hs

The IO formal methods team, in collaboration with researchers from Delft University of Technology, the University of Edinburgh, and Chalmers University of Technology, created a DSL for writing verified Haskell code and presented it at The Haskell Symposium 2022. This tool has been used to verify the test generator in Plutus, where some properties are actually easier to prove than to test. This tool is also used in Ouroboros Peras to define verified Haskell test models that are verified to be sound against the formal specification. Additionally, the tool is used by the Cardano Foundation to verify wallet code, and IO engineers are also building a Rust backend for Agda.

The figure below illustrates the example of a verified program in agda2hs. On the left, you can see the annotated code for an insertion and binary search tree, guaranteed to maintain the tree’s invariants. In this case, the properties are inherently guaranteed and do not require additional proof. On the right, the generated Haskell code is shown after the annotations have been removed.

Figure 5. Example of a verified Haskell program in agda2hs

Plutus High Assurance

For Plutus High Assurance, the formal methods team is developing tooling in Lean to allow smart contract developers to automatically rule out certain types of problems in their contracts with a single click, as also prove custom properties directly on the real code.

Ouroboros Peras

For the Peras project, IO has introduced a formal specification of the protocol in Agda, verified test models generated using agda2hs, performance models of vote diffusion, a Cardano Improvement Proposal (CIP) written in literate Agda, and a prototype implementation in Haskell, which is conformance tested against the specification. The next phase of Ouroboros Peras is underway via Intersect, a scientific paper is nearing completion, and Peras is expected to launch on mainnet in 2025.

Figure 6. Ouroboros Peras methodology

The figure above shows how the Peras project methodology connects the design to the specification and implementation.

The final word

IO has proven the value of formal methods through extensive use in Cardano projects, where formal specifications and verification processes have identified and prevented critical issues. By embedding formal methods into the development lifecycle, IO ensures that the system meets its goals with high assurance, paving the way for more secure and scalable blockchain solutions.