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 specializes in the security of interblockchain protocols. We conduct security audits, operate network infrastructure, develop critical software, and carry out research at the intersection of formal methods and blockchain technology.

Contact Us


In partnership with Cephalopod Equipment Corp, we provide Proof of Stake validation and IBC relayer services to the Cosmos ecosystem and beyond. For more information about Cephalopod’s services please contact us at


We are a leading security auditor in the blockchain ecosystem. We take a unique approach leveraging Apalache and Model-Based Testing to conduct protocol and security audits of specifications and software that can find complex bugs. 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.