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.
Informal Systems is excited to announce a partnership with Cephalopod Equipment Corp, a Toronto-based company operating infrastructure for decentralized intelligence.
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.
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.
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.
Enabling Transformation with Blockchains.
All proceeds from this online webinar will go to FoodShare Toronto and Hamilton Health Sciences Foundation
The Research and Development team from the Interchain Foundation (ICF) has officially spun out into a new Canadian company, Informal Systems (Informal), to continue its R&D work on the Cosmos Network software and protocols in an independent operating structure that allows for more flexible experimentation. See the corresponding announcement from the ICF.
© 2020 Informal Systems Inc. All rights reserved.
