Our Products

Blockchain Infrastructure

We are a leading contributor to the Tendermint and Cosmos projects, focused on formally verifiable implementations in Rust.


The Tendermint blockchain system—a Byzantine Fault Tolerant state machine replication engine for applications written in any programming language.


The Interblockchain Communication (IBC) protocol—a protocol for secure, packet-based communication between distinct blockchains.


Hermes is a an open-source Rust implementation of a relayer for the Inter-Blockchain Communication protocol (IBC), released under the ibc-relayer-cli crate. Learn more.

Formal Verification Tools

We develop tools for formal verification of distributed systems protocols and implementations.


A symbolic model checker for TLA+—formally verify TLA+ specifications for real-world distributed systems protocols and generate tests for software implementations.

Model Based Testing

We are developing “Model Based Testing” (MBT) methodology and tools around the TLA+ specification language and the Apalache model checker, allowing us to auto-generate tests for real implementations (eg. in Go or Rust) from an underlying TLA+ model.

Our infrastructure powers the network.

Our Services

Informal Systems is a full-suite Research & Development institution. We offer basic and applied research, software development, consulting, and education, with a focus on formal verification, distributed systems, and blockchain technology.

Contact Us


We are partnered with Cephalopod Equipment Corp to provide validation and relayer services to the Cosmos ecosystem and beyond. For more information about Cephalopod’s services please contact us at validator@informal.systems.


We are a leading security auditor in the blockchain ecosystem. We take a unique approach of leveraging Apalache and Model-Based Testing to conduct protocol and security audits of specifications and software. You can read more about Informal’s security audits in our audits repository. Contact us for more information on protocol and security audits for your project.


We work with clients on bold research problems at the intersection of formal verification and distributed systems, where our research team has made pioneering advances. We maintain active collaborations with leading scientists around the world, and regularly publish our research.

Whether developing a new verification technique, designing a new distributed system, or verifying the correctness of a blockchain consensus algorithm, we help make formal verification more accessible, and distributed systems more reliable, for organizations large and small.