Cardano has been an incredibly challenging and fun project to work on involving many teams throughout the world with different skills and opinions on design, process and quality. Our core technology team consists of Well Typed, Serokell, Runtime Verification, Predictable Network Solutions and ATIX, with IOHK leading them. Then we have external auditors such as Grimm, RPI Sec and FP Complete ensuring quality and holding us accountable to delivering what we have promised. When dealing with a consortium, it’s important to be aligned not only on day to day affairs, but on the broader engineering philosophy of why and how things should be constructed, as well as the pace of development. I’d like to spend a few paragraphs exploring the principles that guide our roadmap.

First, we can only grow as fast as our community. At the moment, more than half of our community has never used a cryptocurrency before. This reality means that while it would be awesome to introduce complex features like stake pools, blockchain based voting and subscribable checkpoints, they would be underutilized and therefore ineffective until the community catches up. To this end, we’ve provisioned resources towards a help desk tour, a dedicated support channel and trying to interact with our community as much as possible as they grow. This is tremendously time consuming, but it really does force our software to become simpler and more useable.

Cardano help desk tour, Tokyo sessions.

This effort challenges design assumptions, such as what the capabilities of the average node in our system should be. Throughout the next few months, a large part of our focus will be on answering questions, debugging software, improving the user experience and community education. The output will be that more people use Daedalus comfortably and back up their Ada, are able to use exchanges according to best practices, and understand why Cardano is a special project. It also means our software will slowly become more bug free and compatible with different configurations.

Second, we believe firmly in the vision of Satoshi that these networks must be resilient and distributed. Resilience means we cannot optimize around a collection of trusted or usually reliable nodes to maintain the network. Distributed means that wherever possible, every node contributes to propagating the network and its DNA. This creates tremendous design challenges. One is at the mercy of the weakest links when replication is the tool used for resilience because it dramatically slows the network as more users come online. While we feel that a protocol like Ouroboros is perfectly suited to properly balance these conflicting demands, we admit that general network and database capacities aren’t quite ready for this task. The sole – and temporary – advantage that Cardano enjoys here is that we are new and won’t feel the pain of scale for the next year.

Yet we must remain vigilant in our efforts to address these concerns systematically as we have done with Ouroboros. Therefore, many of the most significant network improvements will be scheduled for deployment in late 2018 and throughout 2019. Third, there is a difficult balance between research and deployment. We have great protocols and protocol developers. We also have a unique advantage in being able to quickly submit papers for peer review in order to promptly validate them or fail fast, instead of enduring difficult lessons of hindsight that can result in the loss of funds. However, we cannot allow the urge to have something ready soon for commercial advantage to drown out proper process. With Ouroboros for example, we have a serious and ongoing formal specification effort using Psi Calculus to model and remove all ambiguity from our consensus protocol. This effort has been fruitful in dramatically increasing our understanding of all the benefits and sins of Ouroboros, but will not yield working code until the second half of 2018.

Ouroboros Praos researchers, left to right: Bernardo David, Alexander Russell, Aggelos Kiayias, Peter Gaži

We deployed a rigorously built protocol for Byron, but one that does not enjoy a formal specification. There is always the chance we did something wrong, as with all software projects. There is always the chance we haven’t followed the intent of the scientists, despite our best engineering efforts. The broader point is that as our protocols increase in complexity, interdependence and with the use of more exotic cryptographic primitives, finding a balance will become more challenging. The saving grace we have is that many of our security assumptions are somewhat composable, we use great methods like Red-Black teams, peer review and formal specs, and using Haskell forces deeper conversations about intent.

The question of when to introduce smart contracts has become the most difficult issue of our roadmap. IOHK has brought some of the best minds from the programming language theory world, such as Professor Rosu and Professor Wadler, into the area of smart contracts. They have watched the world evolve from simple computers measuring performance in the megahertz and kilobytes of RAM to the internet age of big data, AI on demand and nearly unlimited processing power.

It’s an extraordinary honor and privilege to work with people with so much wisdom, hindsight and proven contributions to the fabric of computer science. Yet we also have the demands of Ethereum and the other systems that while lacking rigorous foundations have proven to attach a large following and much mindshare. We won’t accept the model of smart contracts is a closed matter and that these issues are now just a matter of optimization. We won’t accept that society is anywhere close to mass adoption of this new paradigm. It’s the beginning and it would be foolish to say Ethereum’s model is the one to back. Yet we acknowledge the need for something like that model. Therefore, we’ve decided to increase our allocation of resources towards two parallel tracks of research.

One is focused on fixing the issues that Ethereum’s hastily driven design process has yielded to the despair of those who have lost funds as a result. The other is focused on the ontology of smart contracts in general as well as different computational models that achieve similar ends without necessarily involving the new complexity or cost that Ethereum introduces. Professor Rosu’s team at the University of Illinois and the partnership with Runtime Verification is focused on the former effort. The work of Professor Wadler’s team is focused on the future and broader theory. We hope to establish more foundational research in the field of smart contracts, as Professor Aggelos Kiayias did with the GKL model and Ouroboros.

Next, there is the interplay between good partners like Bittrex, Ledger and others who are consumers of our APIs and have to deploy our software for thousands to use. The reality is that all interfaces are best guesses until they are used and then must change to conform with reality, not best intentions. We’ve already seen lots of room for improvement for our middleware layer, Daedalus’s design and also new features that would be helpful in making integration simpler and more cost effective. To this end, we’d like our first light clients to come from third parties instead of directly from IOHK, to force our documentation to improve and our software to become less arcane. Much of the effort towards Shelley (Cardano’s next major release) will be focused towards these types of improvements. They create a wonderful feedback loop that helps us make better decisions that benefit larger groups of users. Finally, the Cardano roadmap isn’t the property of IOHK, Cardano Foundation or Emurgo. It belongs to the community. When a cryptocurrency is new, it needs good shepherds to guide and steer, but we cannot allow the ecosystem to be ruled by a beneficent dictator or oligarchy.

This requirement creates some issues about scope. We have a clear idea of what needs to be done over the next 18 months to realize some of the technical requirements of Cardano from scalability to interoperability, but we cannot operate as a dictatorship pushing along and telling everyone to accept it. Cardano belongs to those who hold Ada. Thus we’ve decided to execute with three parallel paths. First, Shelley is our path to the full decentralization of Cardano. This must be done and we have decided to publish in full what Shelley entails. Next, there is the issue of Cardano Improvement Proposals (CIPs) and gathering consent for moving forward on whichever one is decided upon. We have invested a great deal of effort into building a solid voting system and will be releasing it for public review soon. This includes a standard for CIPs.

After Shelley, we will be proposing all changes to Cardano as CIPs and adding increasingly better democratic mechanisms to gather consent for these changes. The burden should be on us to inform and rally the community behind a direction. We cannot allow a technocracy to form alongside a cult of personality of the good leaders. Cardano must have the legitimacy of consent from its users. Finally, the roadmap needs to be often reviewed and updated. It cannot be a static document so we are going to run a monthly clock and update it frequently. We are also going to create a channel for people to proposal alternative roadmaps. As our users become more sophisticated and we accrue more enterprise partnerships, we fully expect divergent paths to be proposed and our hope is that they are better than our own. As a last thought, a cryptocurrency is only as good as the community behind it. We’ve been humbled by how amazing, patient and helpful our community has been. Our hope is that the roadmap is something we can build together over time and it becomes one of our strongest pillars.

To learn more about the project see the recent whiteboard video. Filmed on location at IOHK's Blockchain technology lab, Tokyo Institute of Technology - 東京工業大学

The IELE and K team Mathematical rigor and good design of programming languages and underlying virtual machines are critical for the success of blockchain technologies and applications. Indeed, decades of accumulated evidence show that formal techniques and their early adoption in the design of computing systems can significantly increase the safety, security and dependability of such systems. Moreover, when paired with good user interfaces that hide the mathematical complexity, such techniques can also increase the effectiveness, elegance and quality of code development. A good example is the recent success of functional programming languages and of automated theorem provers or constraint solvers.

Runtime Verification, a University of Illinois start-up founded by computer science Professor Grigore Rosu, has been recently awarded a research and development contract by IOHK to design a next generation virtual machine and a universal language framework to be used as core infrastructure for future blockchain technologies. The formal analysis and verification technology employed in this project was initiated by Prof. Rosu and his collaborators back in 2001, when he was a NASA scientist, and has been improved over more than 15 years of research and development both in his Formal System Laboratory (FSL) at the University of Illinois at Urbana-Champaign and at Runtime Verification, with generous funding of more than $10M from organisations including NSF, NASA, DARPA, NSA, Boeing, Microsoft, Toyota, and Denso. It is about time that aircraft grade, software analysis technology used for mission critical software gets deployed to smart contracts, the blockchain and cryptocurrencies. The project will be executed by a team of Runtime Verification experts led by Prof Rosu, who will work closely with students at the University of Illinois – also funded by IOHK – and with the IOHK research and development team.

IELE – A Register-Based Virtual Machine for the Blockchain

Based on learnings from defining KEVM, our semantics of EVM in K, we will design and define a new VM, which we call IELE (after the Mythological Iele). Unlike the EVM, which is a stack-based machine, IELE will be a register-based machine, like LLVM. It will have an unbounded number of registers and will also support unbounded integers. There are some tricky but manageable aspects with respect to gas calculation, a critical part of the design.

Here are the forces that will drive the design of IELE:

1. To serve as a uniform, lower-level platform for translating and executing smart contracts from higher-level languages, which can also interact with each other by means of an ABI (Application Binary Interface). The ABI will be a core element of IELE, and not just a convention on top of it. Also, unbounded integers and an unbounded number of registers will make compilation from higher-level languages more straightforward and elegant and, looking at the success of LLVM, more efficient in the long term. Indeed, many of the LLVM optimizations are expected to carry over. For that reason, IELE will follow the design choices and representation of LLVM as much as possible. The team includes an advanced PhD student from Vikram Adve’s lab at the University of Illinois, where LLVM was created, and who is an expert in LLVM.

2. To provide a uniform gas model, across all languages. The general design philosophy of gas calculation in IELE is “no limitations, but pay for what you consume”. For example, the more registers a IELE program uses, the more gas it consumes. Or the larger the numbers computed at runtime, the more gas it consumes. The more memory it uses, in terms of both locations and size of data stored at locations, the more gas it consumes. And so on.

3. To make it easier to write secure smart contracts. This includes writing requirements specifications that smart contracts must obey as well as making it easier to develop automated techniques that mathematically verify/prove smart contracts correct wrt to such specifications. For example, pushing a possibly computed number on the stack and then jumping to it regarded as an address makes verification hard, and thus security weaker, with current smart contract paradigms. We will have actual labels in IELE, like in LLVM, and structured jumps to those labels. Also, avoiding the use of a bounded stack and not having to worry about stack or arithmetic overflow will make specification and verification of smart contracts significantly easier.

Like KEVM, the formal semantics of EVM that we previously defined, validated and evaluated using the K framework, the design of IELE will also be done in a semantics-based style, using K. Together with a fast (LLVM-based) execution backend for K, it is expected that the interpreter obtained automatically from the semantics of IELE will be sufficiently efficient to serve as a reference implementation of IELE.

K as a Universal Language for the Blockchain

Besides EVM, several languages have been given a complete formal semantics in K, including C, Java, and JavaScript. Several others will be given K semantics as part of this project, including IELE itself, Solidity and Plutus. We want to allow all these languages, and possibly more as they are given K semantics, to be used for writing smart contracts. For that, we need to enhance the capabilities and implementation of the K platform itself, which will increase the practicality of all new and existing K semantics. We will implement several performance improvements not yet taken beyond proofs of concept, and develop production-quality implementations of analysis features such as the K symbolic execution engine, the semantics-based compiler (SBC), and the program verifier, which currently have only prototype-quality implementations in the academic K project.

Faster Execution

We plan to develop a concrete execution backend to K that will be at least one order of magnitude faster than the current one. The current one is based on translation to OCaml; we plan on translating to LLVM and specializing the pattern matcher to the specific patterns that occur in semantics. We believe it will be possible to execute programs against our KEVM semantics as efficiently as the reference C++ EVM implementation(!). If that will indeed be the case, and we strongly believe it will, then this will mark an unprecedented moment in the history of programming languages, when a language implementation automatically derived from a formal semantics of the language can serve as a realistic implementation of that language. While this was proved as a concept with toy languages, it has never been proven to work with real languages in practice. The K technology has reached a point where this is possible now. And not only to execute programs, or smart contracts, but also to reason about them, because a formal semantics, unlike an interpreter, can also be used for formal verification.

Semantics-Based Compilation

One of the most challenging components of the K framework that will be built in this project is what we call semantics-based compilation. The following picture shows how SBC works:

We have implemented a rough prototype and were able to make it work with a simple imperative language, which we call IMP. Here is an example:

The program to the left is transformed, using the semantics, into a much simpler program that looks like an abstract machine. The four states represent the “instructions” of the new language L’, and the edges are the new semantic rules of L’. As seen, the semantics of the various sequences of instructions has been symbolically summarized, so that the amount of computation that needs to be done at runtime is minimized and everything that can be done statically is hardwired in the new semantics of L’, so all done before the program is executed. Preliminary experiments are encouraging, confirming our strong belief that the resulting SBC programs will execute one order of magnitude, or more, faster:

These improvements to the K framework will not only yield a reasonably efficient prototype of executing smart contracts on IELE, but, more importantly, will give us an approach to write smart contracts in any programming languages that have a formal semantics in K.

We, the K team at RV and at UIUC, are very excited to pursue this new project with IOHK. This gives us a unique chance to demonstrate that the K technology is ready to transit to the real world, in a space where security and trust in computation are paramount. It almost feels like smart contracts are the opportunity that K was waiting for all along, like what it was designed and implemented for.

Why do we need transaction fees?

There are two main reasons why transaction fees are needed for a cryptocurrency like Cardano:

People who run full Cardano nodes spend time, money and effort to run the protocol, for which they should be compensated and rewarded. In contrast to Bitcoin, where new currency is created with each mined block, in Cardano, transaction fees are the only source of income for participants in the protocol.

The second reason for transaction fees is the prevention of DDoS (Distributed Denial of Service) attacks. In a DDoS attack, an attacker tries to flood the network with dummy transactions, and if he has to pay a sufficiently high fee for each of those dummy transactions, this form of attack will become prohibitively expensive for him.

How do transaction fees work?

Whenever somebody wants to transfer an amount of Ada, some minimal fees are computed for that transaction. In order for the transaction to be valid, these minimal fees have to be included (although the sender is free to pay higher fees if he so wishes). All transaction fees are collected in a virtual pool and then later distributed amongst participants in the Cardano protocol.

How are the minimal transaction fees calculated?

The minimal fees for a transaction are calculated according to the formula

a + b × size,

where 'a' and 'b' are constants and 'size' is the size of the transaction in Bytes. At the moment, the constants 'a' and 'b' have the values

a = 0.155381 ADA,
b = 0.000043946 ADA/Byte.

This means that each transaction costs at least 0.155381 ADA, with an additional cost of 0.000043946 ADA per Byte of transaction size. For example, a transaction of size 200 Byte (a fairly typical size) costs

0.155381 ADA + 0.000043946 ADA/Byte × 200 Byte = 0.1641702 ADA.

Why did we pick this particular formula? The reason for having parameter 'a' is the prevention of DDoS attacks mentioned above: even a very small dummy transaction should cost enough to hurt an attacker who tries to generate many thousands of them. Parameter 'b' has been introduced to reflect actual costs: storing larger transactions needs more computer memory than storing smaller transactions, so larger transactions should be more expensive than smaller ones.

In order to arrive at the particular values for parameters 'a' and 'b', we had to answer questions like:

• How expensive is one byte of computer memory?
• How many transactions will there be on average per second?
• How large will a transaction be on average?
• How much does it cost to run a full node?

We had to estimate the answers to those questions, but now that Cardano is up and running, we will be able to gather statistics to find more accurate answers. This means that 'a' and 'b' will probably be adjusted in future to better reflect actual costs.

We even plan to eventually come up with a scheme that will adjust those constants dynamically in a market driven way, so that no human intervention will be needed to react to changes in traffic and operational costs. How to achieve this is one focus of our active research.

How are fees distributed?

All transaction fees of a given "epoch" are collected in a virtual pool, and the idea is to then redistribute the money from that pool amongst people who were elected "slot leaders" by the proof of stake algorithm during that epoch and who created blocks.

At this stage of Cardano, where all blocks are created by nodes operated by IOHK and our partners, fees are already collected (to prevent DDoS attacks), but they will not be distributed and instead will be burnt.

As soon as Cardano enters its next, fully decentralized stage, fees will be distributed as described above.

What next?

Coming up with a solid scheme for fee distribution is a challenging mathematical problem: How do we incentivize "good" behavior and promote efficiency while punishing "bad" behavior and attacks? How do we make sure that people who participate in the protocol receive their fair reward, while also ensuring that the best way to earn money with Cardano is to make the system as reliable and efficient as possible? The trick is to align incentives for node operators with the "common good", so that rewards are highest when the system is running at optimal performance.

These are questions studied by the mathematical discipline called Game Theory, and we are proud to have prominent game theorist and Gödel Award laureate Prof. Elias Koutsoupias of the University of Oxford working with us on finding solutions to this problem.

IOHK received both Bitcoin and Ada for its contract to work on the Cardano project. IOHK converted most of its Bitcoin at the time of receiving it to fiat in order to ensure project stability. With respect to IOHK's holdings of Ada, IOHK does not expect a need to liquidate any of its Ada to cover immediate costs related to the Cardano project until 2019. However, like most ventures in the cryptocurrency space, we have made certain payroll commitments in Ada to several IOHK personnel, contractors and third party firms.

Therefore, IOHK will voluntarily adopt the following vesting schedule for its Ada. A third of IOHK's Ada holdings will be immediately available to IOHK. A third will be made available after June 1st of 2018. The final third of IOHK's Ada will be made available after June 1st of 2019.

Charles Hoskinson will not receive any Ada until the final third of supply unlocks in June of 2019. When the computation layer of Cardano is released next year, IOHK will move its total Ada supply into a custom vesting contract to reflect the above policy.

In the spirit of full disclosure, IOHK's initial Ada address is:

As for Emurgo and the Cardano Foundation, we have requested both partners to make a similar statement about use of funds. As they are independent businesses, they will do so at a time and manner of their choosing.

The technology was conceived in an Osaka restaurant more than two years ago and from that small beginning Cardano has been built into a leading cryptocurrency. The project has amassed a team of experts in countries around the world, has generated more than 67,000 lines of code, and has a strong and growing community in countries across Asia and beyond. Along the way, Cardano has set new standards for cryptocurrencies with best practices such as peer review and high assurance methods of software engineering. The official launch was held in the district of Shibuya in Tokyo on Saturday October 14 for an audience of about 500 people, who had each won a ticket through a lottery held on social media. Excited cryptocurrency enthusiasts, Ada holders and business people from across Japan queued to get Cardano t-shirts and souvenir physical Ada coins, before going into the main hall to hear about how Cardano was created and the vision for its future. "The first thing we did when we knew the project was real was to build great partnerships," Charles Hoskinson, founder and CEO of IOHK, told the audience. "Our chief scientist is based at University of Edinburgh, it is a wonderful place, where they built the heart of Cardano. We have a lot of wonderful people at the University of Athens, they are rigorous, making sure that the theory works. And we have people at Tokyo Tech who work on multi party computation and look to the future, and work out how to make Cardano last a long time." The vision for Cardano, Hoskinson said, was that it would pull together academic research and bright ideas from computer science to produce a cryptocurrency capable of much more than its predecessors.

This "third generation" cryptocurrency would be able to scale to a billion users, using a proof of stake algorithm, Ouroboros, which avoided the huge energy consumption of proof of work cryptocurrencies. Features that would be added to Cardano to help it scale included sidechains, trusted hardware, and RINA, or recursive internetwork architecture. Sustainability would be part of the design by way of a treasury system to fund development indefinitely, allowing stakeholders to vote on proposed changes to the protocol. Meanwhile, the computation layer of the technology, would be innovative in using a tool called K Framework to allow developers to write smart contracts in the programming language of their choice, he said. Security is paramount to cryptocurrency because flaws in code increase the risk of hacks and the loss of coin holder funds, unfortunately witnessed too often. With that in mind, Duncan Coutts, head of engineering at IOHK, explained how the company approaches software development: cryptography research papers are translated into code using the technique of formal specification. This involves a series of mathematical steps that progressively take the cryptography closer to the code that the developers write, a process that allows checks to be made that the specifications are indeed correct.

Duncan Coutts, IOHK Director of Engineering, presenting at the Cardano launch event

"I’m passionate about bringing clever ideas from computer science and using them in Cardano," Coutts said. "And I’m obsessive about software quality. Beautiful software is like beautiful mathematics or poetry." Aside from engineering, the other twin pillar of IOHK is research, and Bernardo David went on stage to talk about the rigour supporting the papers that IOHK produces. David is an assistant professor at Tokyo Tech where IOHK has a research partnership, and was one of the team that produced Ouroboros, a provably secure proof of stake algorithm. On the question of whether people should accept the quality of the research, he pointed to the paper’s peer review through its acceptance to Crypto 2017, the annual cryptography conference held in California. "This is the first proof of stake paper that was published in a big conference so you can trust the largest and most respected cryptography conference in the world," he said. "You don’t have to take my word, you can trust all the other cryptographers."

Michael Parsons, Chairman of Cardano, speaking at the Cardano launch event

The launch event introduced the other important organisations supporting Cardano, such as the Cardano Foundation. The Swiss-based standards body acts as the guardian of the protocol and its duties include providing information to the community and working with governments to shape regulation. Michael Parsons, chairman, announced that Ada holders would be able to store their coins in the Ledger hardware wallet and integration was being worked on. Plans for the future included working with a respected London think-tank to produce blockchain research. Thanking the community, he said: "Cardano is a blockchain protocol with integrity. We are dedicated to helping it derive its full potential and make the world a better place. You supported us to help make Cardano what it is, so thank you." The third organisation supporting Cardano is Emurgo, which is based in Japan and extends support and advice to anyone wishing to build applications on the software.

Ken Kodama, CEO of Emurgo, emphasised the advantages of Cardano’s technology over older cryptocurrencies, and said: "Emurgo sees a bright future that Cardano will provide a more trustable way of identifying individuals and also a reasonable, and faster payment method to people who don't have them now. Emurgo will play an important role in plugging developers and startups to the Cardano ecosystem." Kodama, along with Darren Camas, senior adviser to Emurgo, spoke about how a network was being established in other Asian countries to support its growth. Camas said: "The question for us is how do we help Ada become the fuel that powers financial technology, not only in the developed world but in Malaysia, Vietnam, Argentina, Nigeria… How do we bring more people from across the globe to transact in the Cardano ecosystem?"

After the presentation crowds formed outside the hall to have their photos taken with the Cardano team. Some people who came along were longstanding supporters of the project, such as Naomi Nisiguchi, from Mie Prefecture. She works as a manager in the construction industry and has had an interest in cryptocurrency for four years. "Around two years ago I heard about Ada and that Charles Hoskinson was involved," she said. "I’ve been following the news on Facebook and I’m very interested to learn how the project will move on."

Ken Kodama, CEO of Emurgo, speaking at the Cardano launch event

Many people had plans regarding Cardano. Takashi Kawaguchi set up Fintech Academia last month to give Japanese people information about cryptocurrencies, and came along because he believes Cardano has the potential to rise up and be on par with Bitcoin and Ethereum. His website would provide educational resources that would help people understand and trust crypto, he said, and learn that it wasn’t an enemy, but represented the future.

Other people at the event were planning business interests, such as Nobuyoshi Hayashi from Tochigi prefecture, who owns a consultancy and wants to begin offering cryptocurrency advisory services. The launch itself is only the beginning for Cardano, with many new features to be added during the next three years that will cement its position as the leading cryptocurrency. Mario Larangeira, specially appointed associate professor at Tokyo Tech, was in the audience, and said it was a great time to be working in cryptography. "To be part of this project is challenging, complex but also very exciting," he said. "Now we are working on multi party computation and putting even more cryptography into Cardano, for example with Kaleidoscope, new research that is being produced at Tokyo Tech with Bernardo David and Rafael Dowsley."

Bernardo David, IOHK Research Fellow, speaking at the Cardano launch event

There was much hard work ahead, agreed Charles Hoskinson, and holding an event in Tokyo with Cardano partners was a very special occasion. "This is a really fun event," he said. "Cardano has its largest community here in Japan and we felt it was so important to have a launch event to thank the community for being so supportive, loyal and patient. The point of this event has been to talk about where we came from and where we plan on going, and meet some new people and make new friends."