Informal Systems RPGF nomination

PGF Ops Genesis RPGF Nominations
1

Hey, Adi Seredinschi here. I am with the Informal Systems cooperative and I would like to nominate my organization to the RPGF program for their contributions to two areas of interest, as follows.

Contribution to IBC

Informal Systems bootstrapped their development work on IBC as soon as the organization was established in January 2020. One of our first open-source repositories was GitHub - informalsystems/hermes: IBC Relayer in Rust. This initial repository hosted, among others, English and TLA+ specifications of the core parts of the IBC protocol, model checking results (which led to some changes to the protocol), plus Rust implementations of an IBC relayer and IBC modules.

In summer 2022, the repository was split in two main parts:

  1. GitHub - informalsystems/hermes: IBC Relayer in Rust which hosts the IBC relayer, and
  2. GitHub - cosmos/ibc-rs: Rust implementation of the Inter-Blockchain Communication (IBC) protocol. which hosts the IBC modules in Rust.

The Hermes IBC relayer started being used in production IBC operations with the launch of IBC in 2021, and was an essential piece of the IBC production rollout and growth. The majority of production operations today employ Hermes for its reliability, comprehensive features, and documentation. The documentation (https://hermes.informal.systems/) and discussions & issues in the Hermes repository are of separate interest because they document several challenges, outages, or corner cases that the IBC protocol faced in production so far.

Building a core IBC stack in Rust had a benefit for correctness, because it led to manual code inspection across the two implementations (Go and Rust), which still leads to discovering bugs, inconsistencies, or under-specified behavior.

Contributions to Tendermint and related libraries

On the Tendermint front, an important contribution was to the Tendermint light client, both on a research side as well as implementation. Concerning research, Informal contributed to the specification of the light client, which was formally verified and documented in this repo tendermint/spec/light-client at main · tendermint/tendermint · GitHub as well as academic publication intended for a broader audience (https://arxiv.org/pdf/2010.07031.pdf). Concerning implementation, the GitHub - informalsystems/tendermint-rs: Client libraries for Tendermint/CometBFT in Rust! repository hosts a variety of Rust libraries, most importantly a Tendermint light client implementation, used in production IBC today.

Towards bridging the gap between our IBC & Tendermint work, we also prototyped GitHub - informalsystems/basecoin-rs: An example ABCI application making use of tendermint-rs and ibc-rs. This project served as a basic method of bootstrapping a Tendermint ABCI application which uses both tendermint-rs libraries and the IBC modules in Rust and therefore to build a non-Cosmos-SDK node that is IBC-compatible. The major impact of basecoin-rs is that it allowed us to test integration of our IBC modules and Tendermint libraries, as well as the Hermes IBC relayer, against a production (Gaia) node. This effort was heavily inspired from work done by an EPFL student while interning at Informal Systems in the fall of 2020: GitHub - CharlyCst/tendermock: A mocked Tendermint node for integration testing of IBC protocol..

Starting in summer 2022, Informal Systems also started stewarding the Tendermint Core (soon to be renamed) implementation in Go. Our first mandate was restoring confidence in the software and restoring the integrity of the team after several iterations of churn in team composition, which led to withdrawing releases v0.35 and v0.36. On a technical aspect, this meant our major area of focus is QA and overall increasing confidence in the quality of the software. It also involves shipping ABCI 2.0, ongoing as part of releases v0.37 and v0.38, which includes salvaged code (i.e., cherry picked) from earlier withdrawn releases. Finally, it also involves ensuring a tighter integration of Tendermint Core with its growing array of user-cases, beyond the Cosmos stack, such as privacy-first applications and the wider IBC-powered Interchain.

Main contact: Arianne Flemming arianne@informal.systems.

2 Likes
2

Adding here one more area of interest that warrants nomination to RPFG program for Informal Systems. The credit for this nomination (and for writing this) goes to the Apalache team in Informal Systems, to name primarily Shon F. shonfeder (Shon Feder) · GitHub and Igor K. https://github.com/konnov.

Development of Apalache

Apalache is a symbolic model checker for TLA+ and Quint (integrated in Q1/2023). The model checker is released under the Apache 2.0 open source license and is available at the Github repository: GitHub - informalsystems/apalache: APALACHE: symbolic model checker for TLA+.

The model checker is listed on Leslie Lamport’s TLA+ page as one of the three tools in the portfolio of verification tools for TLA+, alongside the explicit-state model checker TLC and the TLAPS proof assistant. Apalache checks safety for bounded executions and inductive invariants for unbounded executions, assuming that all data structures are finite. The tool leverages the SMT solver Z3, from Microsoft Research. Since Apalache translates specifications to symbolic constraints, it is particularly useful for analysis of distributed protocols and smart contracts that have very large state spaces. For instance, it is able to check the basic invariants of token-based protocols, which deal with very large integer values.

Apalache started as an academic project at Vienna University of Technology (TU Wien) in 2016, after receiving funding from the Vienna Science and Technology fund (see project ICT15-103). In 2018, the project development was reinforced by the Veridis group at Inria, Nancy, which Igor Konnov (the Apalache principal investigator) joined as a researcher. In 2019, Igor Konnov and Josef Widder (principal co-investigator) joined the Interchain Foundation, and soon helped to found Informal Systems. This initiated the technology transfer of Apalache into the Interchain space. The industrial development was partially funded by: the Interchain Foundation, Informal Systems, and Vienna Business Agency (via the grant No. 3590634 of the Innovation/18-21+ track).

Since entering into the Interchain ecosystem, Apalache has been instrumental in specifying the behavior and expected properties of several key protocols:

  • a TLA+ specification of safety and accountability of Tendermint consensus. This specification includes model checking results with Apalache for 4-7 validators.
  • a TLA+ specification of the light client that is used in conjunction with Tendermint consensus. This specification also includes model checking results with Apalache. The modeling and experimental results are exposed in the arxiv report.
  • a TLA+ specification of the fast synchronization protocol. The modeling and experimental results are exposed in the paper at ISoLA’20.

Beyond protocol specifications, Informal Systems has applied Apalache in a number of security audits. Among the projects that we are allowed to disclose, Apalache was applied in the audits of the Injective Protocol (2021) and Evmos (2021). Successful applications of Apalache at Informal Systems spun-off two new open source projects: the Quint specification language and the Atomkraft testing tool.

The theoretical foundations of the Apalache technology were published in several academic papers, most notably, at ACM OOPSLA 2019 and TACAS 2023 (accepted to the conference). A recent exposition and a comparison with TLC and TLAPS can be found in the paper at ISoLA’22. A number of talks and presentations can be found at the Apalache page in the talks section.

2 Likes