From theory to implementation: why formal methods in blockchain development matter

Reliability, security, and efficiency are crucial factors when dealing with complex and fast-evolving decentralized systems such as blockchains.

At Input | Output (IO), formal methods are a cornerstone in achieving these goals. With a rigorous mathematical approach, IO addresses challenges unique to blockchain development – such as unpredictable network conditions, the security of financial data, and the need for fast iteration of cutting-edge research. This post explores why formal methods are indispensable to IO’s approach and how they help build robust solutions that enhance the Cardano blockchain.

What are formal methods?

Formal methods encompass a range of techniques that involve applying mathematical rigor to software and hardware design and implementation – from requirements to specification, implementation, and execution. These techniques can be used early to assess feasibility and clarify requirements, to streamline and accelerate the development process, or later to verify system behavior and ensure its smooth updating. Formal methods can be applied to various system aspects, including correctness, security, and performance.

But what actually are formal methods? Some helpful intuition can be gleaned from the fact that this term is already used in primary education, where it roughly means ‘show your working!’

For example, when a young child adds two numbers, they might use sometimes unreliable mental arithmetic or a systematic and reliable technique like a ‘chimney sum’. The latter is a basic form of formal method often taught in school, albeit possibly under different names. Systematic approaches like this help ensure accuracy and allow a third party to verify the answer.

This process may be slow on paper, but fortunately, it can be easily automated by a device such as a calculator – or a phone. This is an example of the prototypical formal method in production. There is no need to check the individual steps of adding two large numbers as the calculator does it for us. This allows focusing on the more important challenge of determining which calculation to do first and then making practical use of the answer.

In school, the responsibility for checking usually falls on the teacher, and answers are either right or wrong. This can make blurting out the answer tempting (at least it was for me). However, after leaving school and having spent over 25 years as a programmer, it’s clear that finding and fixing code errors (debugging) is a demanding process. Debugging is much easier when the code is readable, the intention is clear, thorough testing is in place, and the chosen programming language helps prevent entire classes of bugs.

In software development, one generally must continue iterating until reaching the correct solution. Therefore, an approach that steers developers towards the correct answer quickly, with a high probability of accuracy, is a sweet spot, avoiding the inefficiency of trial and error.

This simple idea of ‘showing your working’ (which helps break down the problem to reach an independently verifiable solution) is very powerful. It extends from basic arithmetic techniques learned in school to the implementation of the large systems that we build at IO.

Why do formal methods matter?

Building blockchain systems presents three key challenges that formal methods help address:

1. Testing a blockchain system in realistic conditions is challenging, as it operates on public internet infrastructure, run by a decentralized community with diverse hardware and a complex web of real-world interactions, identities, credentials, and transactions. Cardano, for instance, has over 3,200 stake pools and 1.3 million delegated wallets. Investing extra effort in design, high-quality code, and defining performance and security parameters before testing and subsequent deployment helps ensure a smooth user experience on mainnet. This saves time during development and testing and helps avoid unexpected issues (with Cardano boasting 2,200+ days of uptime) when new features are launched on mainnet.
2. Blockchain systems handle financial assets and sensitive data, making integrity and security essential. Cardano, with over 90,000 smart contracts and 160,000 native asset policies, demands robust protection against bugs, which can be difficult – or even impossible – to fix without severe consequences. Identifying issues as early as possible, ideally during initial design, helps to mitigate risks effectively.
3. IO builds on cutting-edge research to develop novel systems that deliver timely solutions to users. Rapid and accurate iteration from design to implementation is essential and minimizes costly development delays. Also, it results in a principled and well-understood design that’s easier to optimize, modify, secure, and leverage in the future.

In 2025 and beyond, Cardano aims to offer a range of solutions for:

• Faster finality with the Ouroboros Peras consensus protocol
• Optimized throughput with the Ouroboros Leios consensus protocol
• Improved scalability with Hydra Tail rollups

• Interoperability via the release of partner chains.

New nodes and node architectures, greater integration with other systems, fees payable with different tokens (Babel fees), intents, confidentiality, and Self-sovereign identity (SSI) solutions with hybrid apps, Midnight, and Hyperledger Identus will help drive these initiatives forward.

Formal methods, including mathematical specifications and proofs, ensure high-assurance software and user confidence in managing digital funds. IO’s extensive use of these methods in Cardano projects has prevented critical issues, demonstrating their value in building secure and scalable blockchain systems.

The next blog post will dive deeper into how IO implements formal method techniques into developing projects within the Cardano ecosystem and will showcase several examples. Stay tuned!