Performances
RD Popularity Index
RD Growth Index
Comparison
Fundraising
Investment
Follow Updates
Follow Lists
People
About Informal Systems
Informal Systems is a distributed systems engineering and formal verification firm whose main output is Cosmos infrastructure software: the CometBFT BFT consensus engine, the Hermes IBC relayer and the Apalache model checker. It targets protocols that run but are hard to prove correct, since bridge and appchain failures usually come from edge cases in the consensus layer that ordinary testing does not reach. The method is to model a protocol in TLA+, express safety invariants as checkable assertions, and align the implementation with the model step by step.
Clients are teams running Cosmos SDK chains, operators that need IBC relaying, and foundations commissioning protocol audits. Unlike auditors that only issue reports, Informal maintains production code and formal specifications together, with the same engineers owning CometBFT releases, Hermes relaying logic and verification artefacts, closing a loop of writing specifications, changing implementations and re-running proofs whenever code moves.
Informal Systems was founded in early 2020 by Ethan Buchman, Zarko Milosevic, Josef Widder, among others, originating from the Interchain Foundation to provide rigorous protocol engineering for the Cosmos network. Its first major project was the Rust implementation of the IBC protocol and a TLA+ formal specification; model checking results led to protocol improvements, and the Hermes relayer was developed and deployed in production after the IBC launch in 2021. The team also formally verified the Tendermint light client and maintained its Rust implementation. In summer 2022, Informal took over maintenance of Tendermint Core (Go), restoring trust after the withdrawal of v0.35/v0.36, advancing ABCI 2.0, and releasing v0.37/v0.38. Its Apalache symbolic model checker was used in security audits and specification verification of several core protocols, including Tendermint consensus, light client, and fast sync. In 2023, Informal helped the Cosmos Hub ship V8 and V9, with V9 introducing Replicated Security, laying the foundation for shared security across chains. These efforts established the formal methods and infrastructure cornerstone of the Cosmos ecosystem.
In 2026 Informal Systems executed a deliberate contraction, announcing a return to two themes: trust in software and trust in money.
After the reorganisation, the formal-methods tool Quint and the multi-party clearing network Cycles became separate companies, while Informal Systems acts as an incubator and shared-services layer. Quint uses executable specifications to describe system behaviour and, as AI-generated code grows, serves as an intent layer that large models can reason about; Cycles offsets obligations among participants to cut the capital needed for settlement, starting with payments and extending to clearing networks for trading firms and exchanges. Hydro, built by Informal, completed its migration to the Cosmos Hub in August.
Informal Systems's Future strategy and roadmap: both ventures raise and operate independently, while Informal keeps research, leadership and shared functions, with the aim of making formal verification a routine part of shipping software in the AI era.
Ethan Buchman — Co-founder & CEO; co-founder of Cosmos and Tendermint, ex-Technical Director at Interchain Foundation.
Arianne Flemming — Co-founder & COO; ex-MD of R&D at Interchain Foundation.
Zarko Milosevic — Co-founder & CTO; EPFL PhD in distributed systems. Canadian worker co-op focused on formal verification.