Explore @informalsystems Open Source projects

Informal Systems (@informalsystems)

informalsystems

Stars
2,669
Global Org. Rank 7,704 (Top 3 %)
Registered almost 5 years ago
Most used languages

Rust
35.4 %

Go
18.5 %

TLA 9.2 %

Python
7.7 %

TypeScript
7.7 %

Bluespec 4.6 %

Shell
4.6 %

SMT 1.5 %

HTML
1.5 %

Scala
1.5 %

Roff 1.5 %

Makefile 1.5 %

F* 1.5 %

Nix
1.5 %

Cairo 1.5 %

quint

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

tendermint-rs

Client libraries for Tendermint/CometBFT in Rust!

hermes

IBC Relayer in Rust

apalache

APALACHE: symbolic model checker for TLA+ and Quint

atomkraft

Advanced fuzzing via Model Based Testing for Cosmos blockchains

cosmos.nix

A reproducible package set for Cosmos, IBC and CosmWasm

basecoin-rs

An example ABCI application making use of tendermint-rs and ibc-rs

modelator

Model-based testing tool

tm-load-test

tm-load-test tool - Tendermint load test application

themis-contract

A command line-based parameterized contracting tool

unclog

Unclog your changelog

multisig

Painless multisig for many keys across many cosmos-sdk chains

cross-chain-validation

modelator-py

Utilities for the TLA+ ecoystem and model-based testing using TLA+.

CometMock

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

sovereign-ibc

Implementation of IBC modules by `ibc-rs` that can run with Sovereign SDK rollups

tla-apalache-workshop

Material for a workshop on Apalache and TLA+. To be populated with more examples.

vdd

Verification-Driven Development

testnets

Various different test network-related configurations for Tendermint

audits

Security Audits by Informal Systems

hermes-ibc-workshop

Hermes IBC Workshop - Fungible Token Transfer (ics-20) between two Starport chains

cosmwasm-to-quint

Semi-automated modelling and Model-Based Testing for CosmWasm contracts

gm

Tool to manage local gaiad instances - without docker

flex-error

atomkraft-cosmos

verification

Specifications of the protocols and the experiments on their verification

hermes-sdk

jsonatr

JSON Artifact Translator

apalache-tests

Benchmarks for apalache

context-generic-programming

Context-generic programming guide

gopherator

Modelator's cousin for Golang

apalache-bench

Apalache Bench Tests

vscode-itf-trace-viewer

VS Code extension for viewing ITF traces

mtcs

Multilateral Trade Credit Set-off

itf-rs

Rust library for consuming Apalache ITF traces

audit-celestia

Workspace set up for collaboration in the Celestia audit

ibc-starknet

Meta repository for managing IBC Starknet projects

stakooler

The koolest tool for Cosmos stakers

megablocks

Prototype to investigate an Atomic IBC solution based on Megablocks

quint-ml-experiments

got

Game of Tendermint

themis-tracer

A tool for managing complex contexts for developing critical systems

quint-sandbox

Material used in interactive demos and tutorials

gravity-dex-demo

Instructions to run the Gravity Dex Demo

chainpulse

Monitoring tool for IBC relayers

agoric-kernel-models

TLA+ models for Agoric Swingset Kernel

hydro

Hydro (aka AtomWars) project repo

kvstore-plus-plus

KVStore++ is an ABCI application that can be used for testing with multiple CometBFT releases

hermes-hackatom-demo

Demo for Hackatom - Hermes

cycles-sandbox

A playground for Cycles demos, experiments and prototypes.

apalache-chai

Chai: Client for Human-Apalache Interaction

ics29-fee-tla

consumer-chain-tool

One-click Consumer Chain Tool

sov-rollup-starter

itf-go

Go library for un/marshalling ITF files

quint_awesomwasm24_workshop

merkleeyes

OsmosisAtomkraft

Informal Systems Atomkraft adaptations and TLA specs for Osmosis audit project

euc

End-user computing for a better user experience

safe-regex

Fork of https://gitlab.com/leonhard-llc/safe-regex-rs

noir-ecies

ignite-blog

Cosmos-SDK blockchain following Ignite's Blog tutorial

economics-analysis

Economics analysis for various projects

ibc-proto

IBC Proto Rust implementation

reactor-experiments

Experiments to help us establish a concurrency architecture for Tendermint in Rust

cgp-workshop

Workshop materials for context-generic programming

partnership-heliax

cosmwasm-ibc

Facilities for implementing ibc-rs-powered light clients and applications as CosmWasm contracts.

hermes-sovereign-relayer

IBC Relayer for Sovereign SDK, powered by Hermes SDK