In our last post, we covered the origins and early ambitions of Informal Systems as it spun out from the ICF in January 2020. Informal started as a worker-owned team of 12 people led by Ethan Buchman (CEO), Arianne Flemming (COO), and Zarko Milosevic (CTO). We grew from these humble beginnings in 2020 to become the largest core development entity in Cosmos, with some 40+ people working on interchain focused R&D. In this post, we highlight different areas of Informal's work, add context for each, and outline our plans for 2023. Finally, we present the funding we've received from the ICF for our work over the years.
Informal's motivating thesis is that interchain technology is foundational to transforming the quality standards of three key, intersecting institutions in society:
Software - how it's built and deployed
Money - how it's issued and distributed
Organizations - how they're owned and governed
Each of these institutions is supposed to provide certain kinds of guarantees and support to the people that use them, but they constantly fail. The quality standards are abysmal. And together they comprise the modern techno-capitalist system, which is destroying the planet and our souls. It's high time someone tried to do something about it, in a deliberate, consistent, and holistic way.
Enter Informal. Our mission is to transform the quality standards of these institutions. Attention to quality is attention to promise making - what guarantees are provided, how are they tested, what if they fail? Our strategy for upgrading these institutions is united by attention to the structure of the promises inherent in each. So what's the plan? Well:
Software - executable specs to guarantee correctness of protocols and software
Money - collaborative financial tools to guarantee the discharge of debts
Organizations - cooperative language and organizational design to guarantee putting people first
We believe the Cosmos project, its technology, vision, and the interchain it's brought to life, provides an essential substrate for realizing this mission. Informal is thus deeply dedicated to the success of Cosmos and the interchain, and we seek to build a resilient organization capable of stewarding complex open-source public goods projects, both for the interchain, and for the more general institutions of software, money, and organizations to be built on top.
Since spinning out from the ICF in 2020, Informal has carried a dual focus on formal methods and the Cosmos technology. Our initial contracts were focused on formal methods work (Apalache, protocol design, verification, testing) and the development of Tendermint and IBC in Rust. But with the fallout from All in Bits in early 2020, the responsibility of maintaining the core Cosmos software in Go became distributed across a number of companies. The ICF created a new subsidiary called Interchain GmbH (IG) to bring on engineers that had left All in Bits, to keep working on the main implementations of Tendermint and IBC. Other engineers went elsewhere. Informal's executive team worked to support the ICF as it got new contracts in place to ensure Cosmos development continued uninterrupted. Over time, it became increasingly clear that, despite its initial plans, Informal needed to pivot to better support the ICF & Interchain GmbH, and contribute more deeply to core Cosmos development. Informal's scope would expand as it took on increasing responsibility across Cosmos, notably for Tendermint in Go (and now, CometBFT) and the Cosmos Hub.
Today, Informal works on a number of core Cosmos projects funded by the ICF, including: Tendermint (recently forked to CometBFT), the world-class BFT consensus engine; IBC, the dominant blockchain interoperability protocol; and the Cosmos Hub, the anchor blockchain of the Cosmos ecosystem. Informal has also received support for some of its work on Apalache, an industry-leading formal methods engine, which is used to secure Cosmos software, and for its work on Collaborative Finance, a new approach to designing monetary and financial systems that can better connect blockchain tech to the real world.
In addition, Informal offers highly-acclaimed security audits to projects across the interchain, and we validate on many Cosmos networks, partnering with projects and communities to help them succeed.
We'll take up each of these focus areas, below.
Informal believes that formal methods can have a transformative impact on software engineering, and the key to getting there is delightful yet powerful tooling for executable specifications. Apalache is the engine behind Informal's formal methods work, where it is actively used to support Cosmos protocol design, development, security review, and testing.
Apalache is a symbolic model checker for formal specifications written in TLA+. It allows engineers to formally specify their protocols and verify their properties, enabling them to find bugs early and reason more effectively through complex sections in their protocols and software architecture. TLA+ is used by top tech companies like AWS, where it is widely acclaimed for its utility in security-oriented engineering, and Apalache is seeing enthusiastic adoption in the TLA+ community, including recognition from Leslie Lamport himself (the inventor of both TLA+ and the very field of consensus protocols).
Apalache grew out of research at TU Vienna and INRIA Nancy, led by Igor Konnov and Josef Widder (both founding members of Informal), along with Helmut Veith, a world renowned computer-scientist. It was industrialized and popularized by Informal, where it is actively developed and maintained with support from the ICF, other research grants (eg. from the City of Vienna), contributions from graduate students, and revenues from Informal's security business. Apalache has been augmented with Model-Based Testing tools (like Atomkraft), which can auto-generate complex test cases for real software from simple specifications. Members of the Apalache, Model-Based Testing, and Protocol Design teams at Informal have used these tools over the years to find and fix bugs across the Cosmos software and protocols. Informal's formal methods work has helped grow the general understanding of Cosmos protocols and improve the security and robustness of implementations, and continues to serve as a magnet for talent in Cosmos.
Apalache is built to provide more accessible and powerful capabilities and to evolve the TLA+ language to be more user-friendly. The Apalache team introduced a type-checker for TLA+, called Snowcat, which allows spec writing to proceed far more smoothly and reliably. The team recently released Quint, a new specification language that improves over TLA+, leveraging the power of Apalache, but designed to be far more accessible and delightful for developers to use. Quint is already being used by community members, with support from Informal, for the design of new IBC protocols. Our goal is to delight developers in their efforts to specify, understand, test, and verify their software and protocols, and to make Quint the gold standard of blockchain specification, to become as accessible as documentation to all those who reason about blockchain protocols - from engineers, product developers, and protocol designers, to executives, investors, journalists, regulators, community organizers, and beyond.
Today, thanks in-part to the support of the ICF, Apalache has matured into a leading open-source formal methods engine, capable of verifying previously unverifiable protocols and finding complex bugs in real software. And Quint, which emerged out of Apalache R&D, holds great promise in successfully nurturing a discipline of delightful, executable specifications, both within Cosmos and beyond. We believe Apalache and Quint are key stepping stones in our journey to change computing.
In 2023, Informal is working on completing the integration between Quint and Apalache, and on supporting engineers across the Cosmos stack (CometBFT, IBC, Cosmos Hub, Cosmos-SDK, CosmWasm) to write better specifications and tests for their software, enabling them to improve their reliability and develop with more confidence. The team will be especially focused on IBC specification efforts this year, in support of ongoing improvements to IBC's multi-stakeholder standards process.
If you think about blockchain protocols - even if you're not an engineer - consider getting started with Quint.
Tendermint - the world-leading Byzantine Fault Tolerant (BFT) consensus engine - is a key part of Informal's DNA. Ethan was Tendermint's lead developer for years, and did his Master's thesis on it. Zarko, who has a PhD in BFT systems from EPFL, was its first and lead researcher, finding and fixing a key liveness issue in the protocol back in 2017. And Igor and Josef, computer scientists who have made breakthroughs in the formal verification of BFT systems, were the first to turn their techniques to the verification of blockchains, and to formally verify core safety properties of the Tendermint algorithm.
When Informal spun out, it was doing Tendermint protocol design and specification, and it was implementing Tendermint client libraries in Rust. We published papers on the Tendermint light client and the BlockSync Reactor, combining formal specs, verification results, and integrations with the software. The light client work especially was foundational for the security of IBC, as the Tendermint light client is the dominant means for Cosmos chains to verify each other's state. Across the blockchain ecosystem, light client protocol development (colloquially known as the "security of bridges") remains an ongoing and complex problem, ripe to benefit from formal modeling and test generation. We look forward to blockchain bridges and light clients being specified in Quint.
Over the years, Informal has continued its protocol design and testing efforts for Tendermint, using its tools and expertise to test and verify protocol specifications and implementations in Go and Rust. We worked on subtle changes to the consensus, like proposer-based time stamps, which allow for a more accurate BlockTime to be produced for applications. And of course, we've been leading the effort to specify and implement ABCI++, unlocking powerful new capabilities for blockchain application developers, but also potential foot guns. With great power comes great responsibility. For more on ABCI++, see this presentation from Sergio Mena, a Technical Lead at Informal.
Informal's early efforts on Tendermint in Rust focused primarily on client libraries to support interacting with the main Tendermint Core node in Go. Chief among these libraries is the Tendermint light client, which is a core part of IBC in Rust, including ibc-rs (the message handlers) and hermes (the IBC relayer). Informal also maintains protobuf files, RPC & websocket clients, and an ABCI client/server system for building out Tendermint-based systems in Rust.
There were some early efforts to begin a full node in Rust, beginning with a compatible socket peer, but these were ultimately deprioritized in order to better support the full node in Go, whose development had moved from All in Bits to a new team at Interchain GmbH. Informal thus started building a Tendermint in Go team in late 2021, which would work closely with the Interchain GmbH team in 2022 before becoming the main steward for the project, forking it, and rebranding to CometBFT in 2023.
Moving forward at Informal, CometBFT is now under the extremely strong leadership of Thane Thomson (Project Lead) and Adi Seredinschi (Product Owner, moving over from Hermes), with Sergio Menia (Technical Lead) and other engineers highly experienced in distributed system design and implementation. The team hosts a highly active and regular Community Call and maintains an up-to-date Project Board detailing key priorities.
The team's core focus now is finalizing the release of ABCI++ and supporting users of its methods, which enable new approaches to MEV, oracles, mempool privacy, and other kinds of more advanced network guarantees. In addition, the team is focused on major improvements to the operational overhead of running CometBFT nodes, including storage and bandwidth reductions, and more control over the RPC/indexing system. This will benefit all chains and operators in the ecosystem and enable further innovation in services built around CometBFT chains. They have also begun a formalization of the peer system, the gossip patterns, and the interaction between reactors in preparation for improving Comet's modularity and evolving its core protocols. If Tendermint was the foundation on which the interchain was conceived, CometBFT is here to take the interchain to the next level.
IBC has been a key focus for Informal since its inception. We believe IBC is the ideal base protocol for a new kind of internet of community computers, and therefore its security, usability, and performance are critical. Between our work on the IBC protocol design, security auditing, implementation in rust, the Hermes relayer, production relayer operations, and IBC developer relations, we have played, and continue to play, a key role in the development of the IBC protocol and network over its history.
One of Informal's major achievements was production deployments of Hermes with the launch of Osmosis in the summer of 2021. After 1.5 years of developing IBC in Rust - including a complete overhaul of IBC's underlying data structures and formatting in the 2021 Stargate upgrade and many protocol changes - Hermes was in production, contributing significantly to the early success of IBC. While anyone could run Hermes permissionlessly to relay IBC packets between sovereign blockchains, Informal received relaying contracts from Osmosis (and later, others) to provide assurances on IBC service quality for the new IBC connections. Over time, many other relayer operators would come online and service critical infrastructure functions in the interchain ecosystem - and many of them use Hermes. Hermes maintains ongoing collaborations and is complementary to the Go Relayer maintained by Strangelove, which is also widely used across the ecosystem.
In 2022, Hermes saw significant stabilization and performance improvements, and v1.0 was released, moving the project into a more maintenance-oriented mode and reducing its team size. Hermes still keeps up with new IBC protocols and plans to continue (ICA, ICQ, ICS, fees, channel upgrades, etc!). It is also preparing to support non-Cosmos chain types more readily, and to integrate more directly with the peer network and the consensus protocol. Informal has been actively exploring designs for more performant and scalable IBC nodes that are more inherently native to interchain realities. The Hermes team at Informal was originally built by Anca Zamfir, an outstanding systems engineer, and the person with perhaps the most complete understanding of the IBC networking protocols in the world. Her quiet contributions to the birth and growth of the interchain likely outweigh in impact those of almost anyone you might find on Twitter. Anca is now working with teams across Informal on their engineering processes, while Romain Ruetschi and Sean Chen lead the current Hermes team.
Over the years, Informal has played an active role in IBC protocol design and quality assurance. Members of Informal, like Ethan, Zarko, Anca, and Josef, were all part of the early multi-stakeholder design meetings for IBC led by Chris Goes, and played an active role in the protocol's design as it matured from 2019-2021. In 2020, Informal audited much of the original IBC implementation, resulting in critical fixes, leading up to its launch. Over the years, we would continue to support protocol design, review, and testing of key pieces of IBC as they were developed, like fees, Interchain Accounts, Interchain Security, and more. We've similarly been involved in supporting security reviews and testing of other interoperability modules, like the Gravity Bridge, which has formed the basis for many connections between Cosmos chains and Ethereum.
Informal also maintains ibc-rs, an implementation of the IBC protocol messages and handlers in Rust, for use by Rust-based blockchain applications. While historically our primary focus on Rust development has been hermes, the ibc-rs handlers recently matured substantially and are being used actively by teams developing in Rust, like Nomic and Anoma. We intend to continue developing ibc-rs as IBC protocols evolve and development of Rust applications expands, working to ensure the library is generally usable by different application paradigms and that it supports compliance with specifications, extensive testing, and delightful integration experience.
As a general purpose and increasingly adopted protocol, IBC has seen significant investment from many teams over the years, helping to secure its place as the leading interoperability protocol for blockchains. Informal is among these teams and continues to invest heavily in the growth of IBC, especially in support for hermes development, relayer operations, ibc-rs libraries, protocol specifications, testing of IBC applications, and the general accessibility of IBC as a new technology and paradigm.
When Informal spun out from the ICF in Jan 2020, it wasn't focused at all on Cosmos Hub development. We did believe strongly in the vision of a strong and stable Cosmos Hub, but we weren't initially contracted to work on it, other than through our work on general-purpose pieces of the Cosmos stack like Tendermint and IBC, and the tooling we built for protocol design and testing. That said, Informal did strive to take payment for its work when possible in ATOM to encourage incentive alignment.
Over the years, as we observed repeated challenges faced by Cosmos Hub development, predicated primarily around the lack of a consistent, dedicated team, Informal took steps to start building a more focused team directly that could serve the interests of the Cosmos Hub community.
Beginning in 2021, Informal took an active role in leading protocol design for Interchain Security. We believe Interchain Security is the optimal initial approach to scaling the Cosmos Hub's security, enabling the Hub to extend its functionality, build stronger partnership relations with other blockchains, and lay a foundation for further innovation in interchain services and shared security protocols. While Informal worked on protocol design, we did not have the resources to pursue building a product engineering team for the Cosmos Hub, until we hired Jehan Tremback in 2021, who would take leadership over the product development of Interchain Security at Informal Systems and start building a team for it, especially over the course of 2022.
While there were attempts to grow a Cosmos Hub team at Interchain GmbH in 2021 and 2022, they were beset by repeated organizational challenges, and members of their Cosmos Hub team would ultimately join Informal in 2023. Under Jehan's leadership as Product Owner, along with Marius Poke (Project Lead), Informal built an integrated Cosmos Hub product engineering team of 12+ people, dedicated full-time to working on advancing the Cosmos Hub, and delivering the first version of Interchain Security to usher in a new era of development and ecosystem expansion. The team built out the Interchain Security brand and protocol, integrated it into the Gaia software, attracted and supported prospective partner chains, and actively researched new protocols like the Interchain Scheduler and Mesh Security to support the ongoing advancement of the services offered by the Cosmos Hub.
Of course, the Informal Cosmos Hub team can only succeed through the active cooperation and collaboration of many different stakeholders across the Cosmos Hub community, from validators, to delegators, service providers, other development teams, and more. The community has proven time and again that no single developer team controls the Hub.
That said, with the support of the ICF, Informal has offered and built a dedicated and effective product engineering team to support the Cosmos Hub. And with the recent launch of Replicated Security, and the upcoming launches of the first partner chains, the Hub community is embarking onto new terrain of collaborative growth. Informal is proud to steward software into this new terrain, and to work towards closer and more transparent funding relationships between core Cosmos Hub development and the Cosmos Hub community.
Starting this year, Jehan began publishing regular monthly updates about the Cosmos Hub, which you can subscribe to on our blog. Working with the Community team at the ICF, we will soon begin hosting Community Calls to better support and engage with the Hub community. Some details on the team's roadmap for 2023 can be found in the January update. Subscribe to the blog for more!
Informal is motivated to bring Cosmos tech to bear on real-world socioeconomic issues, which is essential to realizing the Cosmos mission. Our latest effort, Collaborative Finance.systems/, is focused on just that, an approach to helping communities develop more sustainable economic relationships by collaborating to reduce their debts.
Ethan Buchman has for years emphasized the importance of a monetary localism that can be realized using the Cosmos philosophy and technology. He's expressed this as the ultimate purpose of Cosmos. This localism reflects a quality of sustainable systems - the representation of stakeholders in their state machines. The Cosmos design philosophy is precisely oriented to enable experiments in such representation. Modern Proof-of-Stake is one such experiment, which Cosmos pioneered and leveraged to provide a new mode of building, deploying, and operating blockchains. But Proof-of-Stake, and the Decentralized Finance increasingly built above it, while remarkably effective, are not nearly sufficient to stage the intervention necessary to empower a more sustainable monetary and financial system.
Informal has always believed in a more localist orientation to monetary and financial system design. But there seemed to be a catch. While examples of localist monetary systems abound, they often seem to struggle from a problem of scale and financial viability. Perhaps the most successful are the mutual credit systems of the WIR Bank, Sardex, and Grassroots Economics, which have for years or decades enabled businesses to issue credits against their future production. But others, like time banks and LETS, have typically struggled to grow. Scrip currencies, issued by companies and towns, have proven critical and successful but have been quickly stamped out by central authorities. This is all suggestive that blockchains might have something to offer here (indeed, Grassroots Economics is built on Ethereum tech and exploring a move to Cosmos), but it still felt like something was missing.
Enter Fleischman, Dini, and Littera - experts on complementary payments systems - and their paper on Liquidity Saving through Obligation Clearing. As a prominent local currency community member put it, Someone Just Turned the Lights On. The essential idea is that monetary system design must start from the graph of obligations in the credit network. From there, the liquidity needed to discharge debts can be minimized by taking advantage of partial discharge of obligations along credit cycles and chains. Hence, liquidity savings. This is a profound difference from the way most blockchains projects, and the banking system itself, obsess over the provision of liquidity. But CoFi is unique in that it provides a natural integration point for blockchain and banking liquidity sources. It's effectively a semi-permeable membrane between local and global currency systems.
The Fleischman et al. paper was the key that Ethan and so many others needed to unlock explosive potential for a more collaborative finance. And so, with some initial support from the ICF in 2022, Informal recruited all three authors to found a Collaborative Finance initiative at Informal to expand research in this new approach to monetary design and to support communities using Cosmos tech to realize it. While Informal continues to actively grow the CoFi project, funding for CoFi from the ICF was discontinued in 2023 as part of its ongoing budget cuts.
Collaborative Finance is seeing growing recognition as a unifying approach to many complementary monetary system designs. The academic work is even attracting the attention of Central Banks and their associations, with whom our team members consult on policy and collaborate on research. CoFi offers an alternative direction to the Draconian prospects of CBDCs, one that can simultaneously reduce systemic risk, preserve privacy, and encourage more distributed and sustainable growth.
We've also been working with various communities across the world to support their complementary currency systems and their use of Cosmos tech. We are collaborating on research with groups like Grassroots Economics, Blockscience, and others, and we are preparing for the release of our core graph algorithm and more details on CoFi architecture. Stay tuned.
Throughout its history, Informal has built independent business lines leveraging its expertise and open-source tools and has always aspired to reduce the proportion of its funding from the ICF. In particular, we've seen significant demand for both our security auditing and staking businesses, both of which have grown into industry leading offerings acclaimed across the interchain. Informal has become widely acclaimed especially for security audits, which we began offering in 2021. And our validator team, working closely with many others, has been instrumental in enabling and supporting the growth of new networks. We are honoured to work together with amazing teams across the ecosystem to create a more secure and reliable interchain.
Doing justice to our work as security auditor and network operator will require dedicated posts in and of themselves. Suffice it to say here that, historically, we prioritized the Cosmos mission over our own business development goals in order to fill gaps that emerged in core Cosmos development. This meant turning down opportunities and throttling growth. But as those gaps have been increasingly filled over the years by our own work and the work of others, Informal has been expanding its business offerings and is looking forward to working with ever more teams across the interchain. We'll have more to say on all that in future posts.
In the last post, we mentioned that Informal spun out from the ICF with a $2.5M convertible note investment. We've also been executing against service agreements with the ICF, covering much of the work just reviewed above on formal methods, protocol design, Apalache, testing, Tendermint (and CometBFT), IBC, the Cosmos Hub, and CoFi.
In 2020, when Informal spun out from the ICF, it was around 12 people. By the end of the year, it had grown to ~18, and almost all efforts were focused on the ICF contracts. In total, for its services over the year, primarily on protocol design & testing, Apalache, IBC security, and initial development of tendermint and IBC in Rust, Informal received ~$4.5M in funding from the ICF.
In 2021, Informal grew to ~36 people over the year, mostly working on ICF-related contracts. This included growth in its core formal methods and Rust teams, as well as expansion into two new teams: Tendermint in Go, and Interchain Security (Cosmos Hub). In total, for its services over 2021, Informal received ~$6M from the ICF. In addition, the ICF started paying ATOM bonuses on a per-person basis in late 2021 to support incentive alignment, and Informal received 40k ATOM.
In 2022, Informal grew to ~54 people over the year, with ~45 working on ICF-related contracts - including on Tendermint in Go, the Cosmos Hub, Hermes, protocol design & testing, Apalache, ibc-rs, IBC security, and CoFi. Growth was primarily focused on Tendermint in Go and the Cosmos Hub, as Informal increasingly came to steward both, working to revive development velocity. Informal was also called on for some organizational and operational support at Interchain GmbH. In July of 2022, Informal received a hiring freeze notice from the ICF, responding to market conditions. In total for its services over 2022, Informal received ~$13.4M from the ICF, as well as 279k ATOM in incentive bonus.
Towards the end of 2022, and in anticipation of ICF budget cuts for 2023, Informal took preemptive steps to reduce the size of its formal methods team and to consolidate primarily on CometBFT and the Cosmos Hub, as well as reprioritizing Informal's own business goals (growing its security audit offering). The total contract size with the ICF in 2023 is expected to be roughly similar to 2022, accounted for primarily by growth on the CometBFT and Cosmos Hub teams, and cuts to the formal methods and CoFi teams.
Informal's on a mission to transform the quality standards of software, money, and organizations. We believe interchain technology, and secure public blockchains, are critical to achieving that mission. As a cooperatively owned entity, we're committed to high standards of care and performance in our work together and with the larger community as we collectively develop and operate the open-source interchain technology that inspires us all.
Informal is deeply dedicated to the success of Cosmos and the interchain. We have grown to become the largest steward of open-source public goods in the ecosystem, both for the interchain, and the Cosmos Hub. And our services in security auditing and network operations have come to be highly sought after as we partner with an increasing number of projects in the ecosystem.
We look forward to leading components of the Cosmos ecosystem into new eras of development, collaborating with the larger community on their long-term plans, evolution, and sustainability (as well as on other key public goods) as we work to transform the standards of software, money, and organizations the same way Cosmos transformed blockchains.
Moving forward, we plan to publish more regular updates about our teams and funding as we work with the larger interchain community towards a more sustainable and decentralized funding of core public goods.
We're excited to have built an organization capable of balancing open-source public goods development, with deep tech R&D, sustainable service businesses, and a vision for a more delightful future. And we're excited to share more about who we are, what we're up to, and how it works with all of you. 🥂