The origin of Informal Systems lies in a vision for a new kind of company. A better kind of company. A company owned by its employees. A company focused resolutely on improving the promises made to us by our software systems and our organizations. A company less likely to move fast and break things; a company that might move slow and fix things. There’s plenty broken out there already - just look around. The entire world system has gone structurally short itself. Shouldn’t we be figuring out how to go long? What else could sustainability possibly mean?
Informal’s origins are also deeply tied up in the history of Cosmos; in its philosophy, in its founder conflict, and in its organizational evolution. From the Cosmos philosophy, Informal draws on a core principle that state machines must better represent their stakeholders - and that in turn, companies must better represent their employees. From the founder conflict, suffice it to say, Ethan and Jae had a strong difference of opinions on how to run a company. And organizationally, Informal spun out of the Interchain Foundation (ICF) right before the fallout at All in Bits (AiB). Informal has persisted in supporting the ecosystem to move forward and rebuild ever since.
The founding leadership team of Informal - Ethan Buchman (CEO), Arianne Flemming (COO), and Zarko Milosevic (CTO) - all worked together at All in Bits in 2017-18. That early history of Cosmos is told here. But Informal’s history picks up about where that one leaves off. Throughout 2018, Ethan, Arianne, and Zarko felt that a team at the ICF should be built up to develop a grants and research program, and to fund development of Cosmos beyond AiB. By the end of 2018, Zarko had moved to the ICF to better support research collaborations with various universities on cryptography, distributed systems, and formal methods. By early 2019, Ethan and Arianne would leave AiB to join the ICF as well - it was time to build capacity there, to support the coming launch of the Hub, develop a grants and delegation program, and grow the ecosystem. So that’s exactly what they did.
Under the leadership of Ethan, Arianne, and Zarko, in 2019, the ICF started to hire some amazing people - people like Anca Zamfir, Josef Widder, Thane Thomson, Adi Seredinschi, Igor Konnov, Andy Nogueira, Greg Szabo (who also moved from AiB) and others, people who are still part of Informal today, and who continue to play key roles in Cosmos. These people have some of the most advanced understandings of the Tendermint and IBC protocols and software in the whole world, and have been instrumental in their development.
At the ICF, both Ethan and Jae served on the Foundation Council. The history between them made things difficult for the new team there, especially when it came to longer term planning and collaboration on the core Cosmos software with Jae and AiB. So the ICF’s R&D team was motivated and encouraged to instead work on formal methods, the development of key pieces of Cosmos in Rust (like tendermint and IBC), and to think about spinning out. The team was also eager to build a long term sustainable business, and to take a more active role in governing their organization. By the end of 2019, the ICF’s Foundation Council ultimately agreed for most of the team at the ICF, then around 12 people, to spin out into a new, employee-owned company to work on formal specification of the Cosmos protocols and initial implementations in Rust.
In January 2020, the team spun out of the ICF into the newly incorporated company, Informal Systems. Informal was structured as a workers cooperative, with each employee receiving a single voting share once they had been with the company for 9-months (the gestation period of a human). Informal’s mission was to bring verifiability to distributed systems and organizations, and it set to work on formal methods and rust development within Cosmos.
At this point, Jae was still running AiB, which had 10% of the ATOM supply and had grown to some 50 people, with contracts from the ICF to lead Cosmos development. The ICF had also been granted 10% of the initial ATOM supply, and was managing its reserves of BTC and ETH from the Cosmos fundraiser. By late 2019, the value of ATOM and the ICF's treasury had appreciated considerably. Ethan, as the other founder of Cosmos, and Arianne, who had been leading the foundation, would thus spin out the R&D team they had built at the ICF into a small new company, owned by its employees, working on formal methods and Rust, with a couple years of funding from the ICF, while AiB continued to lead the core.
But at the same time Informal was planning to spin out, independent challenges were mounting at All in Bits. By Feb 2020, less than two months after Informal was born, virtually the entire Cosmos engineering team quit AiB. While AiB significantly reduced its contributions to core development, the company retained its large ATOM treasury. Still today, more than three years later, while Informal has grown to become the largest core developer in Cosmos and the lead developer of the Cosmos Hub, Informal’s total ATOM holdings represent less than 0.2% of the total ATOM supply. Informal remains committed to improving the health and sustainability of the Cosmos Hub and interchain development ecosystems.
Initial funding for Informal came from the ICF, and was structured in three forms: a convertible note investment, a deliverables-based software development agreement, and a research grant. Informal would take payments in a diversity of assets from the ICF, including ATOM, BTC, ETH, and fiat, and would structure its operations to limit the amount of ATOM it sold.
The ICF’s convertible note investment in Informal was for $2.5M, and would give the ICF a future stake in Informal, plus interest. As part of the spin-out and investment, Michael Niederer, the CFO of the ICF, was elected to Informal’s Board of Directors. While Informal was intended to develop an independent sustainable business, and has since inception set goals to reduce the proportion of its funding from the ICF, it was important for Informal to be aligned with the Cosmos mission and to support key public goods. Indeed, over the years, as pieces were missing in core Cosmos development, Informal would prioritize the Cosmos mission over its own business development and seek to fill the gaps.
Informal’s software development agreement with the ICF included a number of formal protocol specifications and software deliverables, expected to be delivered over the course of two years. Deliverables included formal specs of all IBC and tendermint subprotocols to support their security, verification, understanding, and implementation. They also included a Rust implementation of the IBC relayer (which would become hermes), the IBC handlers (now being used by Anoma, Nomic, and others), as well as pieces of a new consensus engine (a fabled “Tendermint in Rust”). The goal of this development was to increase the security of the Cosmos software and protocols, and to successfully expand the Cosmos ecosystem into Rust - goals which were all achieved, and which continue to be renewed. While Cosmos in Rust is flourishing today, the effort to develop Tendermint in Rust was ultimately put on hold in order to prioritize supporting, and eventually leading, the core Tendermint project in Go, which in 2023 was forked into CometBFT.
In addition to the software development agreement, Informal received a research grant payable over 2 years, to work on protocol design, applied formal methods research, formal verification, and testing of Cosmos software and protocols. The research funding was intended to support a growing team and bootstrap a longer term research function in the Cosmos ecosystem with the potential to meaningfully transform computing - making software more understandable, verifiable, and correct. In this regard, Ethan, Informal, and Cosmos have long been inspired by the Sun Microsystem’s mission: to kick butt, have fun, don’t cheat, love our customers, and change computing forever.
To change computing, Informal wanted to make formal methods more accessible and useful to software projects and engineers, providing them with a developer friendly specification experience that integrates well into their software development lifecycle. This is a long-term goal, and will take years to fully realize. Informal has from the beginning pursued a strategy that balances longer term R&D on the formal methods toolchain with more direct application to the Cosmos software and protocols. This has allowed us to build open source tools like the Apalache formal methods engine and our new specification language Quint, but to also focus on protocol design and audits on core Cosmos protocols and software, formally verifying key protocol properties, techniques to verify IBC in Rust, and open-source tooling to improve specs, testing, understanding, and verifiability across the Cosmos stack. This work has in turn served as an attractor for world class researchers and engineers towards the Cosmos ecosystem.
Over the years, Informal grew from these humble beginnings to become the largest core development team in Cosmos, leading development of core products like CometBFT, the Cosmos Hub, and Hermes, and contributing to many more. In the next post, we'll go into detail on Informal's work and funding, highlighting essential technologies at the heart of the interchain and what's in store for their future. Stay tuned!