Merging formal methods and agile development to build Cardano
IOHK formal methods director Philipp Kant lays out our methodology for building software with flexibility and precision
9 April 2020 7 mins read
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.
…
New Shelley formal specifications complete
Formal specifications for delegation and incentives published
16 April 2019 3 mins read
The goal of the Cardano Shelley era is to bring full decentralization to Cardano, moving beyond the federated epoch and handing control of the ledger over to the community via stake pools. As part of the process of delivering Shelley, we create formal specifications which allow us to verify that the final code is in line with what the researchers initially envisaged in their…
Cardano is secure against fake stake attacks
Peer-reviewed design means Ouroboros is free from a flaw affecting many proof-of-stake blockchains
29 January 2019 6 mins read
Ada is not among the 26 cryptocurrencies identified by US researchers last week as being vulnerable to ‘fake stake’ attacks.
1 The Cardano blockchain underlying Ada is based on proof-of-stake (PoS), but its Ouroboros protocol uses no bitcoin code and is not affected by the PoSv3 problem.2 This is not just good luck, but a consequence of the thorough, formally-verified approach…
Recent posts
Applying formal methods at Input | Output: real-world examples by James Chapman
26 November 2024
From theory to implementation: why formal methods in blockchain development matter by James Chapman
25 November 2024
Hydra Doom Tournament by Fernando Sanchez
22 November 2024