Announcing: Interchain security v0.1 Pre-Release

Informal Systems is excited to announce the v0.1 pre-release of Interchain Security! Interchain Security is a feature which will allow the Cosmos Hub to share security with other blockchains. On a technical level, this means that the Cosmos Hub validator set will gain the ability to validate other blockchains alongside the Cosmos Hub. These blockchains are called “consumer chains”, and will be secured by the Cosmos Hub’s billions of dollars of staked ATOMs.

Cosmos and the Era of Community Computers

At the heart of Cosmos is the idea that sovereignty and interoperability are the keys to a sustainable civilization. In this talk originally presented at HackAtom Seoul 2022, Ethan Buchman, co-founder of Cosmos, outlines the vision for Cosmos and what is to come in this new era of Community Computers.

Building with Interchain Security

Cosmos has emerged as the leading platform to build blockchains devoted to a single application. Cosmos chains provide more scalability, configurability, and sovereignty than deploying a contract on a smart contract platform such as Ethereum.

An Overview of Interchain Security v1

Interchain security v1 is the first version of Interchain Security, which allows Cosmos blockchains to lease security to each other. Code for v1 is expected to be completed by the end of Q1 2022, and the feature should launch on the Cosmos Hub with a governance proposal in Q2 2022.

The Informal System: Introducing Workflow

Last year we published Informal Organizations, describing our initial corporate structure and a summary of our background research on worker cooperatives, ESOP-owned S-Corps, and more sustainable financing and incubation for organizations. In this post, we provide an overview of our emerging internal organizational structure at Informal, and the theory behind it. Our goal with Informal is to create a new kind of organization, a democratic structure that aims to rebalance the power dynamics between capital and labour towards something more sustainable and non-extractive, something that nurtures long-term employment and real wealth creation through R&D, entrepreneurship, and innovation.

Interchain Security: From One Chain to Many

At Informal Systems, we are currently helping to build out Interchain Security. There is an exciting dynamic that we think will arise once it is fully operational on the Cosmos Hub.

Themis Update

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.

Dev Update: Cosmos Protocol Design and Formalization

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.

Dev Update: Model-Based Testing

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.

Dev Update: Apalache

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.

Configuration Files in Terms of User Empowerment

Informal Systems envisions an open-source ecosystem of cooperatively owned and governed distributed organizations running on reliable distributed systems. Our view on the technical and ethical dimensions of software configuration is part of this vision. This post frames the problem of software configuration in terms of user accessibility and empowerment and records our current thinking regarding best practices for configuration file formats.

Informal Organizations: Iterating on Cooperative Ownership

Our mission at Informal Systems is not just about distributed systems, it’s also about the organizations that grow along with them. Our vision is an open-source ecosystem of cooperatively owned and governed distributed organizations running on reliable distributed systems. To achieve this vision, we begin with ourselves, adopting a democratic structure that aims to rebalance the power dynamics between capital and labour towards something more sustainable and non-extractive; something that nurtures long term employment and real wealth creation through R&D, entrepreneurship, and innovation; something more like a Zebra than a Unicorn.

Q2 2020 Technical Progress Update

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.

Q1 2020 Technical Progress Update

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.

Start your career with Informal Systems
Start your career with Informal Systems

Explore career opportunities at our cooperatively owned and governed organization, with world-class expertise in distributed systems, formal verification, and open-source ecosystem.

Apply Now