As a third-generation blockchain, Cardano incorporates state of-the-art technology that attracts the interest of computer scientists on the worldwide stage. In the past year, papers describing the consensus algorithm of Cardano have been presented at the leading cryptography conferences, and this month it was the turn of its smart contracts technology to be in the spotlight. Grigore Rosu, a professor in computer science at the University of Illinois at Urbana-Champaign, and his startup Runtime Verification have been working with IOHK since June 2017 to develop new technology based on formal semantics for Cardano, including a new virtual machine. He and his colleague Everett Hildenbrandt came to the UK last week to give presentations at the seventh Federated Logic Conference (FLoC), which this year is in the city of Oxford and runs from July 6-19 with about 2000 attendees. This major conference is held about every four years in various locations around the world, and under its umbrella stages together nine major international computer science conferences. These cover topics such as formal methods, logic and programming languages. Prominent figures from these worlds come to take part and keynote speeches this year are from Shafi Goldwasser and Silvio Micali, the cryptographers and Turing prize winners, and mathematician George Gonthier.

On Saturday, Grigore had the distinction of giving his first FLoC invited talk, at the "Logical Frameworks and Meta-Languages: Theory and Practice" workshop and his talk was about the K framework. It was a technical presentation, going into detail about the logical formalism underlying K, and matching logic, a first-order logic variant for specifying and reasoning about structure by means of patterns and pattern matching.

This technology, developed by Grigore and his start-up Runtime Verification, has been developed over the past 15 years and is used in mission-critical software that cannot afford to fail.  To this end, Runtime Verification has worked with companies including NASA, Boeing and Toyota and many others.  His collaboration with IOHK began after he was contacted by CEO Charles Hoskinson, who had spotted that the software vulnerabilities that had resulted in a number of hacks on blockchains and the draining of hundreds of millions of dollars, could have been prevented using the formal methods techniques developed by Grigore and his team.

The K framework was used to formally model the semantics of the Ethereum Virtual Machine, and the knowledge gained from this process was employed to design IELE, the virtual machine for Cardano that will be released in a test format in a few weeks' time. This is the first time this technology has been deployed within the blockchain industry. Importantly, K is a means to formally verify the code of smart contracts, so they can be automatically checked for the types of flaws that have led to catastrophic financial loss, and must be avoided at all costs.

Grigore said: "We designed IELE from scratch as a formal specification using K and generated the VM automatically from the specification. Therefore, there is nothing to prove about the VM in terms of correctness, because it is correct-by-construction."  He added: "We retrospectively analysed the EVM specification which we defined previously, and looked at all our attempts to verify smart contracts with it and then stepped back to think how should have a virtual machine been designed to overcome all those problems. We came up with IELE. This is an LLVM-like VM for the blockchain. For me as the designer of K, this is a hugely important milestone, and is the first time a real language has been defined in K and its implementation automatically generated."

On Wednesday afternoon, Grigore will give a second invited talk at FLoC, in the International Conference on Formal Structures for Computation and Deduction (FSCD), about the importance of formal analysis and verification for blockchain and virtual machines.  The presentation will be a little less technical than his first talk, and will cover Cardano, and how the tools developed by Runtime Verification allowed the automatic generation of a correct-by-contsruction virtual machine, IELE, from a formal specification.

And on Tuesday at the 31st IEEE Computer Security Foundations Symposium, Everett will present on how he and the team developed KEVM. Everett said: "KEVM is a formal specification of the Ethereum Virtual Machine (EVM) in K, which generates not only a VM but also a symbolic execution engine as well as a deductive program verifier for Ethereum smart contracts. There was a big need for such a complete formal EVM specification, because the previous semantics were either too informal or incomplete. Without a formal semantics of EVM the problem of verifying smart contract is meaningless."

With three talks in total at FLoC in Oxford, it's great to see this technology recognised at such a major international event. Security is of the utmost importance in designing and producing blockchains and we at IOHK put formal methods at the heart of our design approach. K has already been used to formalise C, Java, JavaScript, PHP, Python, Rust, and using these techniques we also plan to make IELE open to developers of many languages, not just Solidity. We will also offer our own languages, Plutus and Marlowe, which are currently in development with computer scientists including Philip Wadler and Simon Thompson. 

Readers who would like to experiment with the KEVM testnet can do so through our Cardano testnets website. We are set to release the IELE on this same site in just a few weeks from now. Stay tuned for more updates.

Artwork,

Mike Beeple

It's the end of April and it already feels like a long time since February, when we announced version 1.0 of Mantis, our Ethereum Classic client built in Scala. After the success of Mantis 1.0 some of the Grothendieck team got temporarily drafted onto other projects. That, coupled with the two-month full-time Haskell training course some of the team were on earlier this year, meant that Team Grothendieck has been short-handed recently. In fact, internally this release is sometimes called "The Konrad Release" as it was developer Konrad Staniec who kept the 1.1 candle burning and the performance pull requests (PRs) coming.

For review of the PRs we did of course leverage the expertise of the whole team, and special mention to Alan Verbner and Nico Taller for their efforts in review and testing of the performance improvements to the complex pruning functionality.

While I'm listing contributors, many thanks to Lukasz Gasior and Radek Tkaczyk for taking time to review PRs early on and especially to Carlos Montero and Jeremy Townsend, two new IOHK developers who jumped head first into the Mantis code just as the test cycle was starting and were invaluable in reviewing PRs and testing the JSON RPC API. Also the testing team's Alan McNicholas for giving the release candidate a whirl and finding an installer bug! That's quite a lot of shoulders to the wheel.

The objective of the 1.0 release was to create a working product, while the 1.1 release aimed to take the working code and find and remove the performance bottlenecks. The most painful bottleneck identified was in synchronizing the blockchain. This was complicated by the fact that tuning that performance depends on quite a few factors, the speed of the network, the type of hard disk on the machine and the number and type of peers at the time of synchronizing.

For example on MacOs with an SSD and 8Gb of RAM Konrad was consistently getting about 17 hours for a full synchronization, whereas on an "small" EC2 instance this could take over a week! One of the reasons for this is AWS t2.small instances can be "limited" or "unlimited" referring to their CPU credits per hour. Once the limit of CPU credits has been reached, the synchronization slows down considerably. Our developer Jeremy Townsend wrote this up and it turns out this can be improved by using a "compute optimised" EC2 instance because the software now spends most of its time actually verifying blocks of transactions and those crypto functions are compute expensive!

Apart from performance, the "difficulty bomb" ECIP 1041 has been disabled – just in time too as the block where this becomes important rolls around in early May.

There have been no changes to the wallet interface in this release. A couple of fairly minor changes were considered but the Daedalus team is flat out and while they are on the team’s backlog list they did not rise sufficiently in priority for inclusion in this release. The only real implication of that in this release is how the block download progress is reported. It was quite confusing for users to see a 0.0% progress bar for such a long time. The reason is the synchronization for ETC is different to the synchronization for ADA, in that ETC implements 'fast sync' and ADA does not.

Fast sync downloads the state trie and the blocks in the blockchain. Ada has no fast sync and downloads only the blocks. In 1.0 the state trie was downloaded before the blockchain and when the state trie was fully downloaded the blocks began to download. The progress bar is only aware of the blocks and so continued to show "0.0%" while the state trie was being downloaded. In 1.1 the situation is better but not perfect. In 1.1, as a result of performance testing and improvements the block downloading begins straight away and the state trie downloads towards the end of the synchronization. The user will see the progress bar update as expected, however towards the end of the synchronization the progress will appear to stall. This happens while the state trie downloads. While this is not perfect and needs to be fixed, on the plus side the whole process is faster and so the frustration should be less. Thank you in advance for your patience with this.

The next release will be Mantis 2.0, currently slated for the end of the year, around Q4. This will be a significant release with significant new functionality. The Project Manager for this release, Ravi Patel, and a full-strength team will be introducing this functionality as it is prioritized.

On a general note, I feel the progress in ETC is picking up pace. Observing the external ETC community it seems there has been a lot of good organisational work done and dedicated people involved. I'm more optimistic than ever about the future!

January got off to a busier start than normal for IOHK because on top of all the usual research and development being carried out, pretty much the entire company traveled to Lisbon for our latest meetup. These week-long events are always hectic and challenging – where everyone comes together to push forward work on projects - but they are also fun, allowing people to meet face to face, sit down over a meal, and get to know each other. Now that we've had time to take stock of the week, what strikes me most is the tremendous amount of energy and effort going into all the work IOHK is doing. We made leaps forward on the various components of Cardano, such as the treasury and delegation. During the week there was a planned schedule of talks, workshops and meetings, organized in the style of a conference, but aside from that program, there were an incredible number of spontaneous discussions taking place. There were continual requests to book meeting rooms, or for 15-minute pow-wows in coffee breaks. Walking around the hotel, you'd always stumble upon small groups of IOHK people sitting around laptops in deep discussion.

Lisbon was a great opportunity to hear about the enormous strides being made by IOHK Research. Professor Aggelos Kiayias, IOHK Chief Scientist, set out plans for Ouroboros, the proof of stake protocol that underpins Cardano, which has been been rigorously constructed based on first principles and has undergone academic peer review. Further development of the protocol aims to speed it up, offer sharding, and eventually allow assets to flow between connected sidechains.

Aggelos says: "It was a very work-intensive week where almost all of the IOHK work threads converged under a single roof here in Lisbon. In terms of research, substantial progress was made on all our high priority objectives including incentives, delegation, wallet security, multi-sig capabilities, sidechains and smart contract support."

The development of Cardano took centre stage during the week. Delegation, a core mechanism of Cardano, was a subject of much discussion in three major meetings that were a continuation of discussions held in Edinburgh last year. Delegation is a mechanism that allows stakeholders to delegate their stake to other parties, such as stake pools, and in return receive some reward for doing so. It fulfils an equivalent function to mining in proof of work protocols and so must offer some benefit to those who delegate their stake. The considerations for creating a delegation scheme are complex and great care must be taken to ensure requirements are balanced fairly, from user privacy to the incentives offered.

Dr Philipp Kant, Director of Formal Methods, said the team is making progress so delegation can move beyond its initial description in a research paper to operation in real life. "In the last weeks we've had various meetings, where we reviewed the mechanisms that we have for delegation in Cardano, to make sure that we can fulfill all the requirements, including rewards for stakeholders who delegate. This week, having everyone in one room, we got to the point where we have a proposal," he says. "What I think we gained is that we've converged on good a scheme to use."

The delicate task of working through tricky problems was also highlighted by Dr Neil Davies, who along with Peter Thompson is leading work on Cardano's network layer, to make sure that its distributed system can deliver high performance even when scaled to millions of users. "There are complex issues when you're trying to construct a new way of organizing how people exchange value, to ensure it will be sustainable in the long term," he says. "This week was the quickest way of getting everybody up to speed, to see everyone's progress and review it among peers. We took a few knotty technical problems and had technical discussion to agree the way forward."

Everyone who came along to Lisbon said meeting in person had real benefits. Professor Philip Wadler, IOHK area leader for programming languages, is working on Plutus, a new language for programming smart contracts on Cardano that is inspired by Haskell, the language he pioneered and in which Cardano is built. Phil says: "Getting everyone in one place has been a real aid to kickstarting what we're doing with Plutus. We've considerably upped the person power involved and I'm excited to see what happens."

Phil also believes that IOHK's championing of peer reviewed research could have profound implications for the cryptocurrency field. "I found Charles's opening talk to be really inspiring, he says. "It's amazing that peer reviewed research isn't the standard in the industry but it's really exciting how IOHK has made that work and turned that into part of the value proposition. If that does nothing else but get others to pick that up, that would be fantastic."

It wasn't just Cardano development that was pushed forwards in Lisbon.

Partners were also present, including ZenCash, the Cardano Foundation, and representatives from Emurgo.

Michael Parsons, chairman of the Cardano Foundation, says: "Coming to Lisbon for the IOHK Global Summit was a rewarding experience on many levels, work, social, and cultural. I had great conversations with many IOHK executives and technology leads and enjoyed participating in a group Cardano webcast. IOHK organized a scenic Lisbon city tour followed by a chance to sample the local Portuguese cuisine, the fresh sea bass was spectacular! All in all, an impressive and worthwhile event expertly coordinated by IOHK, our development partners; I look forward to the next one."

Emurgo had two representatives present in Lisbon. One of them, Shunsuke Murasaki, said it was a chance to talk to the software developers working on Cardano and provide a bridge to development teams in Vietnam and Taiwan working on future applications. "I found this week to be very educational and inspiring," he says. "Emurgo has good partnerships and we will provide technical updates to our partners on Cardano development to accelerate their activity."

For Eileen Fitzgerald, Head of Programs, the week focused on everything from looking at software development methodology to having conversations with new people. "It was great to have everyone finally agreeing on where we are going, consolidating on how we are moving Plutus forward and the K Framework, the Daedalus roadmap, resources, and the direction for the next year," she says. She spent time developing the project management office, which she believes is the only project management office in the world focusing on blockchain development.

Of course, the week was a lovely reminder of how far we've come in the little over two years since the company was founded. More than 100 people working on IOHK projects were in Lisbon. That compares to about 35 people who were at the last meet up, in Malta. And the time before that, in Riga, we numbered fewer than 20 people. IOHK is now a much bigger organization and has recently been doing a lot of work to reshape its structure to adapt to having more people, more moving parts, and more projects.

IOHK in Riga 2016

IOHK in Malta 2017

IOHK in Lisbon 2018

And in the presentation from Charles Hoskinson, he set out business objectives for the next year and for the long term. Highlighting IOHK's pioneering approach to open source software development and high assurance methods he laid out how IOHK has led the way in the cryptocurrency industry.

"We broke new ground by being first to embrace peer review, transforming cryptocurrency from something regarded as amateur and suspect by the academic community into a rapidly emerging area of study within cryptography."

And Cardano's position as IOHK's flagship product was acknowledged.

"If we pull it off, it becomes the financial stack for the developing world capable of handling three billion users. That's the goal of Cardano," he said. "That will require an enormous amount of good technology. We had to bring all these people together to build a project like this. Cardano is the best protocol in the world. In the coming months, Cardano will get better, feature richness will come, and it will be an incredible product."

There was also time for relaxation, with several social outings, group dinners and a visit to the beautiful national park of Sintra, all expertly organized along with the general program by Leonidas Tsagkalias, Costas Saragkas and Tamara Haasen. Conversations about work were never far away though!

I'm looking forward to the next IOHK company meet up where I'm sure there will be even more people in attendance, and we will be able to look back and take stock of even more groundbreaking research and development. IOHK has already begun to set the standard for cryptocurrencies and reshape the way the industry works, so get ready for more exciting developments during the year ahead.

There has been a lot of change in the short time since Release Candidate 1 went out on December 22. Some of the team have swapped the short, dark days of winter for life in the Caribbean, as IOHK have sponsored an eight-week intense and high quality Haskell course in the University of the West Indies in Barbados. Meanwhile work has been getting done on the Daedalus Mantis integration 1.0 release.

The security audit report came in and was digested and published, and a close eye was kept on the bug reporting in Github and the Ethereum Classic forum.

Happily there were very few reported problems. There is a known issue with installing the Daedalus Mantis integration over an existing Daedalus wallet install and this will be fixed in a future version. For now the workaround is to uninstall the Daedalus wallet before installing the Daedalus Mantis integration. Unfortunately it is not possible to install both simultaneously, support for multiple wallet types is something the Daedalus team are working feverishly on.

The most visible impact of the security report was the dropping of support for the automatic download of the bootstrap database. This feature was based on MD5 checksum, which is more broken than we realized.

It is still possible to download a bootstrap database and install it by hand to reduce the amount of time spent syncing the network and it is recommended. Although a small bug fix to the discovery process and some tuning have also reduced the sync wait time, so both are good options now.

And so we can finally after a huge effort from the team and without further ado announce the release of the Daedalus Mantis Integration 1.0!

Planning for next release, 1.1, has already begun, focused on performance improvements and refactors and while we have no dates yet we expect it to be in the first half of this year.

Sincere thanks to those who supported the team, the project and Ethereum Classic over the past months, it is greatly appreciated.

I am pleased to be able to write about the latest release from Team Grothendieck in conjunction with Team Daedalus. It's called the Daedalus release and it combines the functionality of the highly thought out Daedalus Wallet and the Mantis Ethereum Classic Client.

The previous release of the Mantis client was the beta release in August and since then we've been busy both supporting the Daedalus integration and improving the code base, making it ready for production. 

We are now delighted to make our first release candidate available. Download the Daedalus Mantis integration for Windows 10 and MacOS. 

Make sure to check the downloaded binary file against the fingerprint listed on the download page!

The installer installs both Mantis backend and Daedalus wallet and sets up a secure connection between them using an SSL certificate.

The Mantis part of the integration has been packaged with a Java Virtual Machine included to allow fast and easy setup of the client. This initial release has focused on the basic wallet to wallet transfer function and enjoys the safety features Daedalus is known for. This is still very new software, it is not recommended to use this wallet for any high value transactions because we consider this release to be a live test. For users who already use Daedalus Wallet for Cardano, these are currently separate products: one targeting ETC users and one for Cardano users and should not be installed side by side. Near future releases will provide a more integrated experience. 

Ethereum Classic, for all it strengths, suffers from the same synchronization issue as other blockchains – it takes an impractically long time. Reducing this time will be a priority for future releases but at the moment it's quite impractical to wait for days to sync up the chain, and a synchronized chain is required to allow use of the wallet. 

The solution for this is to use our prepackaged bootstrap databases. Anyone familiar with the beta release will remember the bootstrap databases we provided to users to circumvent the download wait. 

The easiest way to get a bootstrap database is through the installer. The installer will download a bootstrap database, check that there's enough free space (~33GB) and then check the downloaded file’s fingerprint. All that being done, it will unzip the file to the appropriate database folder and then clean up after itself. This process can take as little as fifteen minutes or in the worst case several hours depending on the network and disk resources available. The compressed bootstrap file itself is of the order of 10GB.

The log file, located by default in the $HOME/.mantis/logs folder gives a step by step account of the download process.

Upon successful completion, starting the Daedalus wallet will show an almost synchronized database which should take less than an hour to complete its synchronization, depending on how many days pass between when the database was created and installation time.

The second way to install the bootstrap database is to make sure Mantis is stopped and then download the file and unzip it into the $HOME/.mantis/leveldb folder. Remember to delete or move the previous contents of the folder. When Daedalus is restarted, it will pick up the database and the wallet should be up to date in less than an hour. Again, the time will depend on how old the bootstrap database is at the time of download.

To protect your self against MITM attacks always compare the hash of the bootstrap database against the hash published on the Mantis download website.

macOS users must use the manual bootstrap method for now!

Users should be aware that stopping the wallet also stops the Mantis backend and so ends the synchronization process. 

As well as the Daedalus Mantis integration we also announce release candidate 1 of the Mantis command line client. This is a continuation of the command line client we released in August. It is almost identical but where the default configuration is set up for Daedalus, the command line default is set up for "normal" use. Normal use just means that any client can connect to Mantis over HTTP rather than over HTTPS. It also is available for use on Linux and contains no prepackaged JVM.

Apart from the wallet integration, CPU mining has been added to the feature list. In the last release we provided integration with an external miner, this version allows Mantis to perform CPU mining by simply turning on a flag in the configuration.

At about 17.30 GMT on Monday 11 December the first block reward reduction took place, the visible effect of ECIP 1017 and Mantis handled it as expected. After block 5,000,000 the reward for mining a block was reduced by 1 ETC. It was vitally important that all clients implemented this change to prevent a network split. 

Peer discovery, maintaining a gradually changing list of good peers as discovered by asking our peers for their peers and so on is another feature added since the beta release. 

I witnessed a lot of hard work going into this code base and I'm very pleased for the whole Mantis team, Team Daedalus and our DevOps troops who wrestled tirelessly with our various continuous integration pipelines. Their hard work has culminated in a software release they can be very proud of. 

Christmas is just around the corner here in Ireland and will be a welcome break. But January 2018 will be here soon and we will start our security audit of the Mantis code base – and more technology related adventure beckons!