Skip to content
@informalsystems

Informal Systems

Informal Systems

Welcome to our Github!

Informal Systems is an employee-owned organization working on lots of open-source software, with particular emphasis on the Cosmos Ecosystem. We're also pushing the boundary on making formal methods software more accessible to developers.

See below for an index of some of our work on Cosmos and on Formal Methods!

Cosmos

We believe the Cosmos values of sovereignty and interoperability are essential to a healthy interchain economy. We're proud to play a key role in nurturing the interchain as stewards of core pieces of the Cosmos stack, including CometBFT and the Cosmos Hub.

Some of the software we steward is located in other Github organizations:

In our Github org, you can find:

  • tendermint-rs - rust libraries for interacting with tendermint or CometBFT
  • hermes - industry leading IBC relayer software
  • cosmwasm-to-quint - advanced fuzz testing for CosmWasm applications
  • multisig - manage multisigs across many keys and chains
  • stakooler - simplify accounting for staking rewards
  • basecoin-rs - simple rust application built with ABCI and IBC
  • cosmos.nix - Nix integration with Cosmos projects
  • gm - manage local gaiad instances - without docker
  • tm-load-test - load testing for tendermint or CometBFT

Formal Methods

We believe that formal specification is critical to improving the quality of software development and we are committed to making formal methods more accessible to the average developer with delightful tooling.

We built Quint, a specification language designed to delight engineers. Quint builds on the semantics of the widely adopted TLA+ language but introduces modern syntax and tooling that is more familiar to, and usable by, everyday software engineers.

We also built Apalache, a symbolic model checker for TLA+ and Quint, enabling advanced invariant checking for specifications.

  • Quint - a delightful specification language with modern tooling
  • Apalache - symbolic model checker for TLA+

We leverage our tools to perform industry leading audits on blockchain software. Contact us for an audit today!

Organizational Tools

Occasionally we'll build other tools to improve our internal processes

  • themis-contract - legal contracting for developers
  • unclog - avoid merge conflicts when building your changelogs

Pinned Loading

  1. tendermint-rs tendermint-rs Public

    Client libraries for Tendermint/CometBFT in Rust!

    Rust 620 225

  2. hermes hermes Public

    IBC Relayer in Rust

    Rust 451 332

  3. quint quint Public

    An executable specification language with delightful tooling based on the temporal logic of actions (TLA)

    TypeScript 834 37

  4. cycles-quartz cycles-quartz Public

    Secure SGX Sidecar for CosmWasm

    Rust 24 2

  5. multisig multisig Public

    Painless multisig for many keys across many cosmos-sdk chains

    Go 37 10

  6. CometMock CometMock Public

    Drop-in replacement for CometBFT in end-to-end tests

    Go 25 2

Repositories

Showing 10 of 155 repositories
  • hermes-sdk Public
    informalsystems/hermes-sdk’s past year of commit activity
    Rust 12 Apache-2.0 4 35 6 Updated Dec 20, 2024
  • ibc-starknet Public

    Integration of IBC with Starknet

    informalsystems/ibc-starknet’s past year of commit activity
    Cairo 7 Apache-2.0 1 21 1 Updated Dec 19, 2024
  • beacon-kit Public Forked from berachain/beacon-kit

    A modular framework for building EVM consensus clients ⛵️✨

    informalsystems/beacon-kit’s past year of commit activity
    Go 0 147 0 0 Updated Dec 19, 2024
  • hydro Public

    Hydro (aka AtomWars) project repo

    informalsystems/hydro’s past year of commit activity
    Rust 6 Apache-2.0 2 19 (1 issue needs help) 0 Updated Dec 19, 2024
  • malachite Public

    Flexible BFT consensus engine in Rust

    informalsystems/malachite’s past year of commit activity
    Rust 38 Apache-2.0 2 57 (10 issues need help) 3 Updated Dec 19, 2024
  • quint Public

    An executable specification language with delightful tooling based on the temporal logic of actions (TLA)

    informalsystems/quint’s past year of commit activity
    TypeScript 834 Apache-2.0 37 207 (5 issues need help) 12 Updated Dec 18, 2024
  • libp2p-dog Public

    Rust implementation of the Dynamic Optimal Graph protocol for libp2p

    informalsystems/libp2p-dog’s past year of commit activity
    Rust 0 0 0 0 Updated Dec 18, 2024
  • cosmos-sdk Public Forked from cosmos/cosmos-sdk

    ⛓️ A Framework for Building High Value Public Blockchains ✨

    informalsystems/cosmos-sdk’s past year of commit activity
    Go 0 Apache-2.0 3,884 0 1 Updated Dec 17, 2024
  • stakooler Public

    The koolest tool for Cosmos stakers

    informalsystems/stakooler’s past year of commit activity
    Go 4 Apache-2.0 0 7 3 Updated Dec 16, 2024
  • audits Public

    Security Audits by Informal Systems

    informalsystems/audits’s past year of commit activity
    TLA 15 Apache-2.0 3 0 1 Updated Dec 16, 2024