As we approach Shelley on the Cardano mainnet, decentralization has, inevitably, become a topic of debate. Regardless of any initial founding intent, proof-of-work cryptocurrencies such as Bitcoin and Ethereum have become more centralized over time. The early days of Bitcoin enthusiasts mining blocks at the weekend are long gone and today we see a small group of specialized, professional mining operations dominating their respective chains.

In itself, this isn’t necessarily a bad thing – but if it happened to Cardano, it would run contrary to the vision of a decentralized, proof-of-stake protocol.

Cardano has been designed from the ground up with decentralization at its core and, in particular, in its stake delegation and reward mechanisms. On the Cardano network, pools above a certain size will not be competitive, and delegation rewards for everyone are optimal when there are many medium-sized pools. Every ecosystem benefits from diversity. Similarly, we believe that this approach offers the best balance between encouraging grass-roots involvement from skilled members of the community through to supporting those aiming to establish commercial stake pool businesses.

Pledging, and how it works

During pool registration, a pool operator can choose to pledge some personal stake to their pool to make the pool more attractive. The pledged amount can be changed on an epoch-by-epoch basis and will be returned when the pool is closed.

Everybody can operate a pool on the Cardano blockchain. No minimum pledge is required. Pool operators can optionally pledge some or all of their stake (or the stake of their friends and partners) to their pool to make their pool more attractive. The higher the amount of ada pledged, the more rewards the pool will receive, which will attract more delegation.

It is important to remember that there is also no maximum pledge, so a pool operator with a lot of ada to stake can maximize their own rewards by saturating the pool with the pledge and not attracting any delegation. This will of course only be possible for very few operators; most operators will try to attract delegation with a combination of pledge, low costs, low margin and good performance.

How attractive a pool is to delegators depends on four interacting elements:

• operating costs (the lower, the better);
• operator margin (the lower, the better);
• performance (the higher, the better);
• level of pledge (the higher, the better).

By pledging more, the pool operator can ask for a higher operator margin while still being attractive to delegators.

Why is pledging necessary?

Pledging provides a mechanism to encourage a healthy commercial ecosystem on the Cardano blockchain. The pledging mechanism is also necessary to protect the system against Sybil attacks. As I've discussed before, in a Sybil attack, someone with very little personal stake creates hundreds of pools with low margins and tries to attract the majority of stake to their pools. If this succeeds, they can control consensus and engage in double-spending attacks, create forks, censor blocks, and damage or even destroy the system.

By making pools with higher pledges more attractive, such attacks are prevented, because an attacker now needs to split their stake between many pools, making those pools less attractive and increasing the inherent cost of attempting a Sybil attack.

How influential will pledging be?

We face a classic trade-off here: we want the system to be as decentralized as possible and we want to give as many people as possible the chance to operate a stake pool, so pledging should not have a big effect on rewards.

On the other hand, we need to protect the system from Sybil attacks, and the higher the influence of pledging is, the more ada an attacker requires to succeed in such an attack.

The goal is clear: we want to set the influence of pledging as low as possible, while still being able to guarantee security.

How do we determine the influence of pledging?

The parameter that determines the influence of pledging will need to be set before the rollout of Shelley on the Cardano mainnet. However, the parameter has been designed to be flexible and adjustable over time. The Shelley Haskell testnet will provide an ideal opportunity to tune this parameter and test which values work and which do not. We’re also developing a calculator to help pool operators model different pledge amounts and work out how this might affect delegation and thus their rewards and revenues.

Reasonable values depend on many factors: How much stake does a typical pool operator own? How expensive is it to operate a node? How many people are interested in operating a pool? We gathered a lot of data during the Incentivized Testnet, and we will gain even more from the next testnet in close collaboration with our users.

We believe in our scientific approach and are confident that our design will lead to a decentralized, stable, and secure system – but science and mathematics only get you so far. You always have to make modeling assumptions, and no model can ever be as complex and colorful as the real world and the real people who make up the Cardano community.

We have already seen some very positive contributions and debate on the topic, including on Reddit and a recent Cardano Effect show. The Shelley Haskell testnets will be the perfect training ground for us to continue to debate, assess and iterate, collaborating with stake pool operators to see what is optimal for everyone. Just as we saw with the success of the Incentivized Testnet and the recently launched Daedalus Flight user testing, it’s again the time to draw upon the community’s help to put our research into practice.

Today, we’re kicking off the ‘Friends & Family’ testnet, which will allow us to establish a robust network to test and iterate, before we roll it out to the wider community. We’ve gathered a small number of around 20 ‘pioneers’ to help us with this important initial work. By the time you probably read this, they’ll be briefed and we’ll have things underway.

In my last blog, I outlined how the Shelley experience will roll out within clearly defined phases. These first three phases will involve exploring and testing the new Shelley capabilities via a series of testnets. I thought it might be useful to offer a glimpse ahead to provide some additional context.

The rollout of the testnets will happen very much in parallel with our continued progress towards mainnet. So alongside the work on the Haskell Shelley testnet, the mainnet will be systematically upgraded to support the Shelley era protocol, that will enable staking, delegation and metadata.

Similarly, IOHK’s block-producing and public-facing relay nodes on the mainnet will be upgraded so that they are ready for Shelley, and the Blockchain Explorer, Daedalus Wallet, Wallet CLI and other user-facing software will be polished so that it can be used for mainnet.

Users will soon be able to go to the official Cardano websites or other providers such as Yoroi, to download a new wallet – currently in development – that will work with both Byron and Shelley era blocks. The Shelley-era Daedalus wallet will contain all the logic for staking and delegation that has been tested on the Incentivized Testnet, plus new features that are specific to the full Shelley protocol. Stakepool operators, exchanges and others will also be able to download Shelley-compatible nodes and to adapt their own software to support the new Shelley client API. However, during this period, the mainnet will still be running in Byron reboot mode with federated consensus governed by the OBFT (Ouroboros Byzantine Fault Tolerance) algorithm. Think of it as a time when forward compatibility is being integrated but not yet ‘switched on’.

The move to Shelley will be accomplished using the new hard fork combinator that has been developed by IOHK.The hard fork combinator allows a node to transition from one blockchain protocol to another. The Cardano node software that is running on the mainnet will gradually evolve so that it is able to deal with both Byron era and Shelley era blocks, and will be modified to include the hard fork combinator. When the time comes to move the mainnet from the Byron era to the Shelley era, IOHK will trigger a hard fork.

‘Switching on’ Shelley

This will activate the hard fork combinator within the nodes, and the nodes will then change from only producing Byron era blocks to only producing Shelley era blocks. After the hard fork, no new Byron era blocks will be recorded on the blockchain, and the nodes will be able to support distributed block production, staking and delegation. They will have seamlessly switched from the OBFT to the Ouroboros Praos consensus mechanism. We will have entered the Shelley era on the mainnet.

Distributed stake pools and Decentralization of Block Production

Central to Shelley is the idea of decentralization. IOHK believes that companies, systems, and platforms run by a single individual or central authority are more vulnerable and less fair. This is why it is crucial that we move block production to our supporters rather than keeping the power contained within our organizations.

The Cardano blockchain currently operates on a federated basis. Effectively, nodes ‘controlled’ by IOHK and EMURGO are responsible for block production, while Daedalus wallet users act as the nodes of the network. Shelley will mark the ‘beginning of the end’ of that era, as we move from Byron’s static federated system to an active, decentralized system.

At the moment, core nodes and relays are owned and operated by IOHK. The network propagates through relays into each individual wallet. Once the system decentralizes, nodes will be run by stake pool operators and networked with individual wallets. Once control of the system is transferred over, the community will be fully running the Cardano ecosystem.

Federated Block Production (Byron)

Following the hard fork, IOHK’s existing core nodes will initially produce all of the Shelley blocks, as in the Byron era. However, this will change over time, under the control of the built-in d (decentralization) parameter. This parameter can be considered as a control valve that allows increasing amounts of decentralization.

In the decentralization phase, the federated system will still produce a (steadily decreasing) portion of the blocks. As this happens, stake pools will begin registering, operating, and producing blocks and will start to earn rewards in proportion to the stake that is delegated to them. As time passes, more blocks will be made by stake pools and fewer will be made by the core consensus nodes. The balance between the two will be controlled by the d parameter.

Distributed Block Production (Shelley and Beyond)

We will use metrics like the amount of ada that has been staked to determine how quickly to change the d parameter and so to decentralize the network. Once the network has fully decentralized, the stake pools will completely take over block production. At that point, we will then be able to shut down the core consensus nodes and disable the d parameter. This is the first step towards the full decentralization of Cardano. We will return to that in future blog posts, when we discuss some of the exciting developments that the Shelley mainnet will enable.

The road towards Shelley has been long but creating a global financial and social operating system takes time, scientific rigor, and the support of an informed, passionate community. As always, we thank you for your support and encourage you to follow our official channels closely as the Haskell Shelley testnet and subsequent phases roll out.

Since the launch of the Incentivized Testnet marked the coming of the Shelley era last year, the Cardano platform has entered a fast-moving period of development. The Ouroboros Classic consensus protocol has supported Cardano Byron and the ada cryptocurrency for the past 30 months, and we’ll soon be switching to Ouroboros Praos. This is the version of our proof-of-stake (PoS) protocol that will initially power Shelley as Cardano decentralizes. It builds in the staking process with monetary rewards for ada holders and stake pool owners.

We upgraded Cardano on February 20 with a hard fork that switched the mainnet from the original consensus protocol, Ouroboros Classic, to an updated version, Ouroboros BFT. This BFT hard fork began a transition period under Ouroboros BFT, a slimmed-down version of the protocol designed to help us make the switch to Praos, while still preventing any malicious behaviour. Many probably didn’t even notice. For Daedalus wallet users, it meant a standard software update. Exchanges had to upgrade manually, but they had several weeks to do this and we were on hand to help.

The next event was the ‘Byron reboot’ on March 30. This released totally new code for many of the Cardano components, including a new node to support delegation and decentralization, and future Shelley features. A big advantage of the new code base is that it has been redesigned to be modular, so many components can be changed without affecting the others.

In turn, the BFT will act as the jumping off point for the Shelley hard fork, which will happen once we’re happy with the Haskell testnet. This second hard fork will be a similar process to the February one for exchanges, ada holders and wallet users, and, hopefully, just as much of a non-event.

However, while everything looks smooth on the surface, there is a lot of hidden activity going on. Like a duck serenely swimming across a pond – while its feet are furiously paddling below the calm waters – our blockchain engineers are hard at it.

So, we sat down two of the leading engineers on the Cardano project, Duncan Coutts and Edsko de Vries, to find out how they’ve done it. Duncan has been Cardano’s architectural lead for the past three years, and between them, Duncan and Edsko have spent 35 years using Haskell, the programming language being used to develop Cardano.

Duncan, how did you do it?

As described in the Cardano roadmap, IOHK’s blockchain engineers believe in smooth code updates. Instead of trying to do the jump from Ouroboros Classic to Praos in a single update – which would be an incredibly complex task – it’s been a two-stage approach using Ouroboros BFT as an intermediary (Figure 1). The BFT code is compatible with both the Byron-era federated nodes and the Shelley-style nodes released in the Byron reboot. It's like a relay race: one runner (in our case, running one protocol) enters the handover box where the other runner is waiting; they synchronise their speeds (so they're perfectly compatible with each other) and then hand over the baton (operating the mainnet), and then the new runner with the baton continues from the handover box for the next lap.

The Daedalus Flight process has helped us quickly develop and test a new wallet and, once everyone is running that on the mainnet, and once we finish swapping over the core nodes, the old code is redundant. We are in that transition phase right now, with a new mainnet Daedalus wallet released on April 24.

Our aim is to have a ‘graceful entry into Shelley’, as IOHK chief Charles Hoskinson describes in his whiteboard video about the hard fork. A vital tool in making this move has been creating a hard fork combinator.

That sounds like farm machinery. What is it?

A combinator is just a technical term for something that combines other things. For example, addition is a combinator on numbers. A hard fork combinator combines two protocols into a single protocol. We call this a sequential combination of the two protocols because it runs the first protocol for a while and at some point it switches over to the second. In our case, this is two versions of Ouroboros as we move from BTF to Praos.

The clever part of all this has been the use of discrete modules that do their job, while knowing as little as possible about each other and the blockchain. Simplicity is the key here and this process of taking out the details we call ‘abstraction’. Most of the consensus modules don’t even have to know that they’re dealing with a cryptocurrency and could be putting pretty much anything on a blockchain. For example, we’ve done seminars using the example of a Pokémon ledger on a Ouroboros blockchain. The only thing that’s different is the ledger rules; the consensus is all the same. You just set it up – ‘instantiate’ it in the programming jargon – with the rules for playing Pokémon rather than for UTXO-style accounting.[For readers with a technical interest, watch out for Edsko delving further into the ‘abstraction’ process and combinators in a future blog post.]

You make it sound simple

In fact, it’s tricky because Cardano is running the ada cryptocurrency, and a pile of other things, at the same time. Think of it as changing all the wheels on a car while you’re driving along and towing a caravan. So we have to be sure we can do this in a totally reliable way.

We could have tackled this as a one-off task, but it made sense to do it in a generic way using a protocol combinator. We chose this route because we get a better result and the testing that is vital to ensuring the code works is made far easier. On top of that, there will be more hard forks to come, which made the choice even clearer. For example, as we near the culmination of Cardano’s development and move through the Goguen, Basho, and Voltaire eras, there will be at least one hard fork at each stage.

So how did you cope with the tricky bits?

Well, first off, we had to do it without research to turn to. The researchers describe a single protocol as a free-standing, perfect thing. But that’s not where we are. We are trying to run Praos after having started with a chain that was using something else. What Edsko’s working on, going from one protocol to another in a generic way, is just not covered in the research. And it’s hard, it’s complicated. All the details need a lot of thinking, a lot of scratching your head. But switching between Cardano code bases is not the sort of thing the academics can expect to get published. It doesn’t have a novel aspect and is seen as just an implementation issue.

Edsko, can you give us an example?

As Duncan says, for the researchers, these implementation issues are trivial but dealing with them is 99% of what we do. Take the problem of time for a blockchain. It’s what I’ve been banging my head against for a couple of weeks. Time is divided into slots where the chain can contain at most one block per slot. We often need to convert between slot numbers and time in the real world, for example when a node needs to know ‘Is it my turn?’ to generate the next block. This is fundamental to Cardano, but the length of a slot changes after the hard fork. For Byron, a slot is 20 seconds; for Shelley, it will be two seconds, or perhaps one. To really complicate things, the exact point of time when the hard fork is made is decided on the chain itself. Yet, I need to know when the changeover point is. It’s a quandary: to do slot conversions I need to know the state of the blockchain, but to know the state I need to know the slot conversions!

This is real chicken-and-egg territory with many complex things to disentangle. We have to be very precise with how we do things. It might be trivial in theory, but it’s very difficult to disentangle things and make sure it’s not a circular problem.

We can’t afford for it to be wrong, so how do you know you’re right?

Duncan: That’s an excellent question. My reply is that you come to the answer on two levels. The first is intellectual: you analyse the problem, you do the maths, you talk to colleagues and wrestle with it until you can see how it all fits together. Second, we do all our QuickCheck testing to give us the confidence that this does what we think it does. We do extensive testing that really takes us into the unusual cases that you might never think of, including this changeover. We can do 100,000 tests every time we change a line of code. [Lars Brünjes has written about how John Hughes, one of the creators of Haskell, has helped IOHK develop its testing strategies.]

Edsko: Yes, I agree with those two points. In terms of the combinator, I resolve these things by thinking about the guarantees that the code I write needs to provide, and which guarantees that it, in turn, needs from the ledger. I sketch a mathematical proof that this ‘if-then’ reasoning is indeed justified, and then turn to the formal method teams. The formal methods team are the people who set up the mathematical rules that describe the blockchain, and they can then tweak the rules in such a way that they provide the required guarantees.

In terms of Duncan’s second point, I know the time issue I mentioned above is correct by thinking hard mathematically, and by testing. Timing decisions are easy when we have the full blockchain, but are hard when we have to make predictions about the future. Fortunately, the way we set things up means I can easily create testing blockchains. So, I can create a full blockchain, then slice this chain in half. I take the first half and consider that to be in the present; and set the other half in the future. Then I can use the ‘present’ (first half) to make predictions about the ‘future’ (the second half) and verify them against the whole thing (on which the calculations are easy). If they match, then I know everything is OK.

When did you start on this?

Right after Duncan came up with the genius idea of the OBFT. So I’ve been thinking about the combinator on and off for about 18 months. It was a design goal from the very beginning of our modular rewrite of Ouroboros starting in October 2018, with my first commit to the GitHub repository. We had a prototype demonstration with OBFT and Praos soon after, in December 2018.

And how many people have been involved?

Duncan: Many people have been working on the consensus code, but whenever we have anything really hard, like this combinator, we give it to Edsko: he’s our software engineer extraordinaire! This is Haskell programming as free climbing, rather than climbing with the ropes of formal methods for support.

Any final thoughts?

Duncan: The code that was running is right now being phased out and pretty soon the code that was running Cardano a month ago will no longer exist. Once everyone is running the new code on the mainnet and once we finish swapping over the core nodes, the old code is redundant. We are in that transition phase right now and no one is shouting that the sky is falling. No one has noticed it.

Edsko: That is quite an achievement in its own right. The idea of OBFT was crucial in making the transition, but it’s not relevant any more once we make that transition to Shelley. This has been a way for us genuinely to ditch legacy code, which is often very difficult to do, as the banks know to their cost.

Duncan: And if it all works fine, you won’t notice anything.

Duncan and Edsko, thank you for your time. I think we’d better let you both get back to it.

Following the successful Byron reboot of Cardano, we are beginning our phased transition to the Shelley mainnet. This means moving from a static, federated system to a dynamic, decentralized Cardano blockchain.

The process begins with a series of Haskell Shelley testnets, culminating in the Shelley upgrade hybrid phase.

The Haskell Shelley testnets will be a different experience from the previous Incentivized Testnet (ITN) for both stake pool operators and general users/ada holders. This is because the ITN and the Haskell testnets have been created with different goals in mind.

The ITN was designed to give stake pool operators experience in building their critical infrastructure, while allowing IOHK’s engineers to test the new incentive mechanisms with real ada, delegated by actual ada holders. The Haskell Shelley testnet is about ensuring that the Shelley mainnet is calibrated to be a best-in-class experience from day one. Unlike the ITN, the Haskell Shelley testnet will not involve ‘regular’ ada holders: the testnet will not be incentivized. Each phase is intended to run for a much shorter period – weeks rather than months. We will, of course, be testing out the operation of the wallet, explorer, and so on, but using a faucet distributing test ada that doesn’t offer rewards. Ada holders will be able to try Daedalus and the explorer on the public testnet and provide feedback, but without using real ada.

The Shelley experience will roll out within clearly defined phases. The first three phases will involve exploring and testing the new Shelley capabilities and moving to a situation where we are ready for full Shelley mainnet deployment.

Phase 1: Pioneers and the ‘Friends & Family’ phase

The rollout will begin with an invitation-only ‘friends and family’ testnet. During this phase, IOHK will first spin up and run a Shelley-only test network internally. We will then invite about 20 trusted stake pool operators – we’re calling them ‘pioneers’ – to join this (initially closed) network. These operators will comprise a small group who have demonstrated a high level of technical skill and community contribution during the ITN.

These pioneers will blaze the trail for others to follow as we head to full Shelley deployment on the Cardano mainnet. In this important first phase, we’ll be asking them to perform specific functionality tests to capture their valuable feedback while exploring the capabilities of the Haskell Shelley platform. We expect to invite more pioneers to join us – a few at a time – as we add features and prove the reliability of the testnet.

In this ‘closed alpha’ testing phase, IOHK will focus on tuning system parameters such as the saturation threshold, network resilience, and decentralization. Furthermore, IOHK’s engineers will see the Ouroboros Praos consensus mechanism working outside of simulation. The pioneer phase will give IOHK’s engineers the opportunity to address any issues in a controlled environment, with feedback and support from stake pool operators, before moving to the next phase. The findings will be communicated to the Cardano community and opportunities will be taken to learn about and improve the Shelley system.

This phase will also be all about producing high-quality technical documentation and support. The pioneers (supported by the community as a whole) will help us produce documentation that will make it easy to set up and run stakepools, and give our technical support team an understanding of the issues that our users will face.

Phase 2: Opening up the testnet – the public phase

The community response to the ITN was incredible, and we are blessed with having a wealth of skilled stake pool operators in the community. We’ll keep everyone informed through every step of the process and – as ever – our repos will be fully open. But for purely practical reasons, we’ll be working 1-2-1 with just a small group of around 20 operators at first. But our goal is to open things up as soon as we can, with full public access in the next phase.

This will allow all the stake pool operators who participated in the ITN to redeploy their previously constructed infrastructure, and to tune their stake pool to the new Haskell settings. This testnet will run as closely as possible to mainnet conditions, including mixing Byron and Shelley era blocks.

During each evolution in the transition to Shelley, IOHK is placing an emphasis on community training and collaboration. Decentralization of knowledge is just as important as decentralization of the platform. Pioneer participants in the alpha testnet will provide crucial support in advising the remaining stake pool operators on configuration and use of the Shelley system. And as operators acclimatize, we’ll also be asking them to support and bring new operators on board.

Phase 3: The balance check

The third and final phase prior to mainnet deployment is the balance check. This will bring together the Byron and ITN transaction histories, and prepare the mainnet for the Shelley era. At this point, the ITN rewards and mainnet balances will be consolidated. After this point, it will no longer be possible to earn rewards on the ITN. However, users will be able to check their rewards and confirm them in mainnet wallets. We’ll share full details of what ada holders need to do to reclaim their ITN rewards a little nearer the time. The balance check phase will last for only a couple of weeks before we start moving towards decentralized stake pools and the Shelley era.

How we will select the pioneers

We are selecting the pioneer group based on a number of criteria, devised in collaboration with the team at the Cardano Foundation. Pool operators must have a deep knowledge of running stake pools on the ITN, as well as competency working with Linux, and come from a range of backgrounds and geographical locations. Some will be working with cloud solutions providers to run their pool, others with their own hardware – we’ll have a mix. By selecting pioneers from different geographical regions, we will be able to ensure a global reach, and test out our new network implementation.

Pioneers will be expected to commit a set number of hours per week to supporting the rollout program, give direct feedback and provide advice to the community and mentor others at subsequent phases. Bringing others on board and supporting them along the way will be a crucial part of the role. To be clear, as ever, all our repos will be open so we encourage everyone to get involved. As always, IOHK’s developers value input from every member of the Cardano community. Anyone who wishes to is encouraged to spin up their own nodes. If they are skilled developers they can also recommend enhancements to the Shelley Haskell code base because all the information will be published through GitHub.

We’ll be looking to expand the network rapidly with more pools as soon as this earliest testing phase delivers the results we want.

Ensuring an easier start for everyone

The Haskell Shelley code base has been developed with formal methods and the high assurance Haskell programming language. So while we anticipate that some minor elements will need addressing, we believe that the initial experience should be free of any major issues. This is the approach that we have used for the Byron reboot, with great success, and we will be building on the code base that we have developed there. The approach will deliver even greater benefits for Shelley and beyond, by allowing us to deploy software much more quickly than in the past, with new features subject to rigorous and careful checks even before coding has been completed.

Our goal is to provide a plug-and-play solution to get stake pool operators up and running. This means they should be able to pick up a pre-prepared docker image or AWS instance, for example, and their stake pool will be launched. We will, of course, also provide standalone binaries and source code for those with more experience, or who have specific configuration requirements.

We’re now in the final stages of preparation and things are heating up (you may have recently seen a tweet that the new node has produced its first block). With that successful first step completed, we’ll be sharing dates and more details very soon. We’ll also be publishing further blogs outlining the other key steps and milestones in the process. Keep an eye out for those and meanwhile stay tuned to IOHK’s social channels. We’ll be sure to let you know as we start rolling things out.

Form and function

IOHK is building Cardano into a global financial and social operating system. This enormous task requires both quick iteration and absolute precision. It is why IOHK has chosen to combine the speed of agile development with high assurance code and formal methods. Fusing flexibility and formality led our engineers to pioneer this modern development philosophy.

IOHK believes firmly in research, formal methods, functional programming, and building in a rigorous manner. As a competitor in the blockchain development industry, we also have to consistently demonstrate progress and create value for our global community of stakeholders. This means we can’t compromise on robustness or on development speed and flexibility. In an ever-changing marketplace this is a challenge, so our developers have to strike a balance.

Agility versus formality

The start-up standard for developing technology has been to build a minimum viable product quickly and then continually iterate until it is ready for the mass market. This is known as an agile process. It is a great way of showing that a project is advancing while eventually building a fully functional product. However, an agile methodology assumes there will be bugs and weaknesses in each step of development that can be ironed out later. This is fine if there is no value at risk – but, with virtual currencies, there is an enormous amount of money and stakeholder trust on the line.

Building a digital asset on a blockchain provides several challenges to overcome in terms of organizing a development process. As a proof-of-stake cryptocurrency, Cardano is a distributed system in an adversarial environment where consistent performance is critical. The protocol has to maintain security in the face of malicious actors attempting sabotage. This means that no one can afford to build quickly and deal with problems later.

Trust is essential for a currency to be accepted and correctness proofs are an important way to increase the veracity of a system. This is why the code should not only be correct, but there should be evidence of its correctness, such as extensive meaningful tests and mathematical proofs. In a young industry like cryptocurrencies, IOHK engineers have to anticipate the addition of new features while maintaining the correctness guarantees established in the initial version. The platform can only scale globally if it is able to grow while maintaining security and utility for everyone. This is why Cardano developers streamlined their methodology, combining a variety of tools ranging from property-based testing all the way to machine verifiable proofs, to create high assurance software even in the presence of changing requirements.

Research to code

The methodology begins with scientific research. To date, IOHK has released more than 60 research papers that have contributed to creating the platform. Each paper examines a critical aspect of blockchain technology from first principles. How do we gain consensus in a decentralized way? How is a smart contract designed? What is the right reward structure to incentivize good behavior? IOHK researchers examine these questions, and submit their answers to scientific journals and conferences. These papers contain proofs that must pass rigorous peer review. Then, to ensure that the quality of our software does justice to the science, it is developed using formal methods.

In essence, this means that IOHK engineers specify what the code should do mathematically. That way, they can ensure that when the code is run, it contains the desired properties designed into it. The code is written in Haskell, a high-assurance functional programming language with a strong type system. While Haskell is a great tool for implementing reliable software, it is not foolproof, so the code still needs to be tested. A great way to write tests is using QuickCheck, which allows developers to state properties that should always hold in a program. QuickCheck then generates test cases, and searches for minimal counterexamples that violate those properties.

In code that interacts with the external world, in particular network applications, it can be hard to find minimal counterexamples. This is because the order of execution is not deterministic: it can change every time the software is run. The same code can be run hundreds of times, and only fail once. We can get around this by using simulations with deterministic execution order. Running tests in simulation allows us to reliably find and fix a class of bugs in testing, which would otherwise only occur randomly in production.

Bridging the gap

To get a picture of the development methodology employed for Cardano, let’s consider the metaphor of bridge building. When a civil engineer builds a bridge, a large portion of their time is spent behind a desk. The civil engineer plans a design, calculates the statics, and orders geographic surveys. During that time, nothing happens at the building site. An observer would be unable to see any progress being made. For building bridges, this is the correct approach. If the planning is not accurate, it is difficult and expensive to correct problems at a later stage. Ultimately, the result would be a delayed bridge at a higher cost, or one which fails completely. Lack of visible progress is a good price to pay for a functional and safe bridge.

When building software, making changes in later stages is much easier than in construction. That is what enables the common agile development approach. If an agile developer was building a bridge, they would construct a pillar in one rapid sprint and then the next in a second sprint. The gap between the pillars would be spanned in a final sprint and, if things didn’t hold up, the developers would add on one more sprint to fix any issues. While progress would be demonstrable at the building site, the final product would likely have a great deal of problems built into it. This creates clean up work at the end of the project which could have been avoided by better planning at an earlier stage. Furthermore, the minimum viable product would likely be given to a small group of people for a test drive with the expectation that it would fail in order to alert developers of bugs. Needless to say, it is best that bridges aren’t designed in this way.

When hearing the words 'formal methods’, a lot of people in software development think about the civil engineering approach, which is dubbed ‘waterfall’ and generally shunned. This is a common but unfortunate misunderstanding. Indeed, using appropriate formal techniques allows us to have our cake, and eat it too: to have an overall design (a deliberate design, not an accidental one from fitting together pieces developed in sprints), to show progress continuously, and to retain the ability to react to changing requirements.

A key technique employed by IOHK developers is executable specifications. These are high level designs, which abstract over low level details, written in a language that the computer can understand and execute. Executable specifications can be used as prototypes to show progress, get feedback from users, and test assumptions. On top of that, lower level details can be added via successive refinements. Our developers build the bridge to solve the biggest problems first then add pillars to reinforce it at a later time. In a software system, the pillars would be features like saving data to disk, or using performant algorithms, which are needed for a final product, but which are not essential to demonstrate the overall functionality.

Using executable specifications, we get the benefits of proper planning without sacrificing flexibility. IOHK developers can fix what the system should look like on a large scale, and then implement suitable components as needed. Continuous testing guarantees that each component fits the overall design. This helps prevent problems that are common in a late integration approach. With this methodology, we get the best of both worlds: we can use a top-down design (avoiding late integration troubles, having a good handle on the overall design at all times), and have working code early (demonstrating progress, and allowing for tests and feedback through the whole process).

Future proof

Ultimately, the method of construction should be determined by what is being built. IOHK is building a global social and financial operating system which requires rigor and speed. Formal versus agile is a false dichotomy. Instead, we’re continuing to develop our methodology which fuses the best of both approaches: formal techniques within an agile delivery framework, with robust, higher assurance code upon which we can build for all our futures.