Our Products

Informal builds and maintains open source products at the intersection of distributed systems and formal-verification. We primarily build distirbuted systems software in Rust, using TLA+ as a specification language. You can find our work on Github.


tendermint-rs is an implementation of the Tendermint system in Rust, providing Byzantine Fault Tolerant State Machine Replication for applications in any language.


ibc-rs is an implementation of the Interblockchain Communication protocol in Rust. IBC enables secure, packet-based communication between indpendent blockchains.


Apalache is a symbolic model checker for TLA+. Model check larger and more complicated protocols in less time with Apalache.

Themis Contract

Themis Contract is a tool for drafting and signing legal contracts from the command line. Simplify and expedite your contract management process.