Past, Present, and Future of R&D at the ICF: Introducing Informal Systems

The Interchain Foundation (ICF) was founded in 2017 with the mission of promoting and advancing research and development in open and decentralized networks, with a particular focus on the Cosmos Network. Throughout 2017 and 2018, the ICF was a lean entity that primarily funded external development teams, like All in Bits (AIB), to build the software necessary to launch the Cosmos Hub. In late 2018 and early 2019, prior to Network launch, a handful of employees from AIB left to focus on building an independent team at the ICF to develop the funding program and a research and development organization at the intersection of formal verification and distributed systems. Led by Arianne Flemming, who took on the role of Managing Director, Ethan Buchman, as Technical Director, and Zarko Milosevic, as Head of Research, they joined Michael Niederer, who has been CFO of the ICF since early 2018.

Over the course of 2019, the Interchain Foundation significantly expanded its funding program and grew its R&D organization to a world-class team of over 10 people working on Cosmos software and protocols, including implementation work in Go and Rust, and formal verification work in TLA+. This post details the history of R&D activities at the ICF, including external collaborations with universities, growth of the internal team in 2019, and an exciting announcement of what’s next for the team in 2020: a new company.

External Collaborations

Since inception, the ICF has had a long term research focus, and concentrated on developing its capabilities through external collaborations. While 2017 was mostly focused on the foundational software for the Cosmos network, in 2018, the ICF began to participate in broader research efforts with world renowned universities on the frontiers of cryptography, distributed systems, and formal verification. In 2019 some of this expertise was brought in-house.

Cryptography
The ICF recognizes the foundational importance of advancements in cryptography and the potential for cryptography to unlock new landscapes in the design space of open and decentralized networks. To support the frontier of cryptography research efforts, the ICF was a founding partner in the Stanford Center for Blockchain Research, which is pioneering advancements in cryptographic primitives like accumulators, bulletproofs, verifiable delay functions, and more, with a focus on their application to blockchain technology. The ICF also provided funding to Alessandro Chiessa’s group at the University of California, Berkeley, which is innovating rapidly on zero knowledge proofs. Chiessa co-founded Starkware, as Chief Scientist in the West, to help commercialize these developments.

Distributed Systems
The ICF was founded to promote and advance R&D in open, decentralized networks — at their heart, distributed systems. While the Tendermint software marked a major advance in practical distributed systems, and Cosmos a major demonstration of that advance in a public economic network, the ICF has been pursuing collaborations with world-class researchers in distributed systems to advance the field further. To this end, Zarko has been leading collaborations with Rachid Guerraoui’s group at EPFL and with Fernando Pedone’s group at USI. The focus of these collaborations has been on specifying and improving Tendermint-related protocols like the fork accountability protocol, the gossip mechanism, and efficient syncing of Merkleized data stores.

Formal Verification
Based on experience during the development and launch of Cosmos, the team at the ICF came to recognize the increasing importance of practical formal verification, and turned its attention towards formally verifying Byzantine Fault Tolerant software. In particular, the ICF R&D team began collaborating with groups led by Josef Widder, Cezara Dragoi, and Igor Konnov, at TU Wien and INRIA, who collectively have been pushing the frontier on formally verifying Byzantine fault tolerant protocols and software via model checking and static analysis. In 2019, both Josef Widder and Igor Konnov joined the team at the ICF and have been working on specifying and verifying Tendermint-related protocols.

R&D Team, 2019

Inspired by the successful collaborations with external researchers, over the course of 2019, the ICF grew its internal R&D team to over 10 people, with a focus on formalizing the Tendermint and Cosmos protocols, improving the implementation in Go, and building a new implementation in Rust. The team served as a leading contributor to the Tendermint project, contributing major fixes, improvements, reviews, specifications, and tools. They also led many of the Tendermint Developer Sessions, which are publicly available and chart the course of research on things like Tendermint proposer selection, subprotocol architecture, light clients, and more.

While the first half of the year was focused on fixes and improvements to Tendermint in Go, the latter half turned towards the light client, formal verification, and development in Rust. Some of the major achievements of the ICF R&D team throughout 2019 include:

• Major fixes to Tendermint’s proposer selection mechanism, which was found to be broken during Game of Stakes
• A complete refactoring of the Tendermint blockchain reactor (“fast sync”) to make it easier to reason about, test, and verify its correctness, and to serve as an example for refactoring the other reactors.
• Contributions to the IBC specification process
• Tools for deploying testnets for deterministic scientific experiments and for developer-oriented network testing
• Extensive light client research and modelling, including a protocol for secure bisection, a detailed taxonomy of attacks, and initial TLA+ specifications
• Maintenance of tendermint-rs, the repository for Tendermint in Rust
• Initial implementation of the Tendermint light client in Rust
• Initial TLA+ specifications for other Tendermint components
• Improvements to Apalache, a symbolic model checker for TLA+

Through its participation in software development and research activity at the boundary of cryptography, distributed systems, and formal verification, the team at the ICF became increasingly interested in motivating an approach to software development that is driven by concerns of formal verification. As a result, the team has put increased effort and focus on specifications and formal languages like TLA+. In the same way that Test Driven Development is motivated by the need to write good tests, a Verification Driven Development approach is driven by the need to formally verify the software and protocols, providing greater assurances of correctness.

Additionally, through the operation of its Funding Program (see 2019 Year in Review) and its hiring pipeline, the ICF encountered the need for better tools to support its internal processes, and developed a vision to enable developers to manage their organizations the way they manage their software. In 2019, the team developed simple, plain-text solutions for the funding program and the hiring pipeline using Gitlab. The goal is to develop tools for use by other entities in the Cosmos ecosystem and beyond, to simplify their own operations. Eventually, these tools will be integrated with the Cosmos technology stack, allowing legal organizations to leverage the power of Cosmos blockchains to facilitate collaboration and correctness.

R&D Team, 2020: Introducing Informal Systems

Throughout 2019, as the team grew, they became increasingly motivated to develop an independent, financially and culturally sustainable R&D organization to allow for more flexible experiments in these exciting efforts to bring verifiability to the Cosmos ecosystem and beyond. While the ICF served as a fantastic incubator for these efforts, in the summer of 2019, the ICF decided to take steps to spin out the R&D team into an independent, cooperatively owned and governed entity to pursue this work further.

As of January 2020, the ICF R&D team is now an independent Canadian company, Informal Systems Inc, whose mission is to bring verifiability to distributed systems and organizations. In line with ICF’s values of decentralization, sovereignty, and sustainability, Informal is structured like a co-operative, where each member-employee has a single vote in important corporate matters. Informal will continue to be a key contributor to the Cosmos ecosystem, as the team continues and expands the work they began at the Interchain Foundation, including formally specifying the Tendermint and IBC protocols and implementing them in Rust. See Informal’s announcement on their blog.

This work is expected to greatly benefit the Cosmos ecosystem by increasing the correctness guarantees of the underlying protocols, providing an alternative implementation of core components, and expanding the developer ecosystem into the flourishing Rust programming language. Informal will also continue to help manage the ICF funding program and existing research collaborations, and is working with the ICF to transition the funding program to a more decentralized form, so it can better scale and incorporate feedback from a wider group of stakeholders. Ethan will continue to serve as Vice President of the Foundation Council, and Ethan, Arianne, and Andy (who had served as manager of the funding program at the ICF) will continue to provide various administrative support to the ICF.

Informal’s initial funding comes from the ICF in the form of a convertible note, research grant, and software development agreement with a 2 year horizon. Software deliverables include formal specifications for all core Tendermint and IBC protocols, implementation of the Tendermint light client and IBC in Rust, and implementation of a Tendermint full node simulator in Rust. Research deliverables include a verification driven development framework and its application to Tendermint and IBC in Go and Rust.

Informal also offers services including technical and executive education, consulting and design, and research and development with a focus on blockchains, distributed systems, and their formal verification. To learn more about Informal’s services, email them at hello@informal.systems. You can stay in touch with Informal by visiting them at https://informal.systems, subscribing to their blog, and following them on twitter.

The emergence of organizations like Informal, with open and decentralized corporate structures, is critical to the realization of the ICF’s mission of supporting open and decentralized networks. The ICF hopes to see more of these organizations emerge, to join the growing ranks of organizations taking leadership roles in the Cosmos ecosystem, and to reflect the values of Cosmos and the ICF in their corporate structure: open, decentralized, sovereign, secure, and sustainable. The ICF looks forward to the continued growth and collaboration of these entities and to their stewardship of the Cosmos, and welcomes Informal into their midsts.