What is better than one ecosystem of ambitious teams, talented individuals, and bleeding-edge technology? Two such ecosystems. In this post, we provide the story of collaboration across the Starknet and interchain ecosystems that has been flourishing for a few months, covering work on a decentralized sequencer (Tendermint in Rust) and IBC.

For almost a year, Replicated Security has been successfully replicating the multi-billion dollar economic security of Cosmos Hub to the Neutron and Stride chains. A potential hindrance, known as unbonding pausing, of Replicated Security is that, in exceptional cases, the unbonding of tokens on Cosmos Hub could be delayed by more than the expected unbonding period of 21 days. Those potential unbonding delays concern delegators because they might not be able to retrieve their tokens on time.

Informal was born with a dual mandate to focus on formal methods and expanding Cosmos to Rust. Over time it has expanded its scope to better support Cosmos development and the growth of the interchain. In this post, we highlight the different areas of Informal's work, add context for each, and outline our plans for 2023. We also present the funding we've received from the ICF for our work over the years.

The origin of Informal Systems lies in a vision for a new kind of company. A better kind of company. A company owned by its employees. A company focused resolutely on improving the promises made to us by our software systems and our organizations. A company less likely to move fast and break things; a company that might move slow and fix things. This is the story of Informal's origins, as it spun out from the ICF on a mission to expand Cosmos and transform computing.

In this post, we go through the work done by Informal to formally model the Proof-of-Stake (PoS) system of Namada, a proof-of-stake L1 for interchain asset-agnostic privacy built on top of ABCI. We describe how we approached the process of modeling Namada’s PoS system in TLA+, and what invariants we decided to check and why. We also present a short tutorial on how to check Namada’s adherence to these invariants using Apalache, our model-checker.

We recently made a change to replicated security: if a validator commits an equivocation fault (colloquially known as “double signing”) on a consumer chain, they are no longer automatically slashed on the Cosmos Hub.

Informal Systems has been building out Interchain Security v1, which we'll refer to here as "replicated security". There are also several other forms of Interchain Security- opt-in security, and layered (or "mesh") security. In this post we will explore the differences between these forms of Interchain Security. We'll look at the logical differences, and we've also built a mathematical model to explore the economic security of different approaches.

Informal is a new kind of company: we are built on co-operative principles and we are determined to simplify and democratize tooling for organizational management. To this end we built themis-contract, a tool for drafting, modifying, signing, and compiling legal contracts in plaintext, using a mix of markdown templates and configuration files. While we've recently deprioritized feature development in order to intensify the focus on our other projects, we have been using the tool internally for our legal documents. This post details some of the highlights of our current process and explains a bit of the motivation behind our efforts in this direction.

Large parts of the work of Informal Systems in the Cosmos ecosystem is on protocol design, specification, and correctness. For reliable distributed systems, not all the truth lies in the code. Capturing the distributed aspects of the protocols requires a rigorous understanding of the interactions between the code run on the different machines in a system, in particular if machines may act in an adversarial way. We capture these interactions in English specifications, and formalize them in TLA+. We put much effort in this work, as particular protocol bugs are hard to find on the code level. At the same time these bugs can be expensive in the context of adversarial environments with economic incentives.

One of the critical issues when developing blockchain infrastructure is how to perform testing of complicated scenarios, involving multiple distributed nodes, possibly connected to several heterogeneous blockchains. While traditional tests are good and necessary at the level of unit testing, it becomes prohibitively expensive for developers to create (and maintain!) multi-node, multi-blockchain tests.

TLA+ is a tried and tested and widely adopted language for specifying systems. However, formal verification research has made huge leaps forward since the tooling for TLA+ was devised in the late 90s. Our research team has been actively working to fill this gap between state-of-the-art formal verification and the tooling for TLA+. We have been developing Apalache, a symbolic model checker for TLA+. Apalache leverages the power of SMT solvers to reason about states and transitions in terms of a logic of constraints, rather than in terms of individual states and transitions.

Since our last technical update, Informal Systems has continued to play a major role in the Cosmos project, focusing primarily on protocol formalizations, TLA+ specifications, and implementations in Rust. In addition, we're developing general purpose tools for formal verification, and using them on the Cosmos protocols and software.

Since spinning out from the ICF at the start of the year, we've been hard at work on a number of projects aligned with our mission of verifiable distributed systems and organizations. Here we'll provide an update on each of them.