• Stars
    star
    417
  • Rank 103,829 (Top 3 %)
  • Language
    Scala
  • License
    Apache License 2.0
  • Created over 9 years ago
  • Updated 4 months ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

APALACHE: symbolic model checker for TLA+ and Quint
Apalache Logo

APALACHE

A symbolic model checker for TLA+

main badge

Apalache translates TLA+ into the logic supported by SMT solvers such as Microsoft Z3. Apalache can check inductive invariants (for fixed or bounded parameters) and check safety of bounded executions (bounded model checking). To see the list of supported TLA+ constructs, check the supported features. In general, Apalache runs under the same assumptions as TLC.

To learn more about TLA+, visit Leslie Lamport's page on TLA+ and his Video course.

Releases

Check the releases page for our latest release.

For a stable release, we recommend that you pull the latest docker image with docker pull ghcr.io/informalsystems/apalache:main, use the jar from the most recent release, or checkout the source code from the most recent release tag.

To try the latest cool features, check out the head of the main branch.

For more information on installation options, see the manual.

Getting started

Website

Our current website is served at https://apalache.informal.systems .

The site is hosted by github, and changes can be made through PRs into the gh-pages branch of this repository. See the README.md on that branch for more information.

The user documentation is automatically deployed to the website branch as per the CI configuration.

Our old website is still available at https://forsyte.at/research/apalache/ .

Community

Help wanted

Want to contribute? Here is a list of issues that could be solved without knowing too much about the internals of Apalache. Solving these issues would improve usability! Please comment in the relevant issue, if you are going to solve it.

  • Writing annotations in the JSON format: #804
  • Add support for VIEW in the TLC config: #851
  • Translate \E x \in STRING: P and \A x \in STRING: P: #844
  • Interval analysis for a..b: #446

Industrial examples

Talks

Performance

We are collecting apalache benchmarks. See the Apalache performance when checking inductive invariants and running bounded model checking. Versions 0.6.0 and 0.7.2 are a major improvement over version 0.5.2 (the version reported at OOPSLA19).

Academic papers

To read an academic paper about the theory behind Apalache, check our paper at OOPSLA19. For the details of our novel encoding using SMT arrays, check our paper at TACAS23. Related reports and publications can be found at the Apalache page at TU Wien.


Apalache is developed at Informal Systems.

With additional funding from
the Vienna Business Agency.

Past funding from Der Wiener Wissenschafts-, Forschungs- und Technologiefonds.

More Repositories

1

quint

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

tendermint-rs

Client libraries for Tendermint/CometBFT in Rust!
Rust
610
star
3

hermes

IBC Relayer in Rust
Rust
441
star
4

atomkraft

Advanced fuzzing via Model Based Testing for Cosmos blockchains
Python
77
star
5

cosmos.nix

A reproducible package set for Cosmos, IBC and CosmWasm
Nix
56
star
6

basecoin-rs

An example ABCI application making use of tendermint-rs and ibc-rs
Rust
55
star
7

modelator

Model-based testing tool
Python
53
star
8

tm-load-test

tm-load-test tool - Tendermint load test application
Go
46
star
9

themis-contract

A command line-based parameterized contracting tool
Go
46
star
10

unclog

Unclog your changelog
Rust
36
star
11

multisig

Painless multisig for many keys across many cosmos-sdk chains
Go
35
star
12

cross-chain-validation

TLA
33
star
13

modelator-py

Utilities for the TLA+ ecoystem and model-based testing using TLA+.
Python
28
star
14

CometMock

Drop-in replacement for CometBFT in end-to-end tests
Go
25
star
15

sovereign-ibc

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

tla-apalache-workshop

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

vdd

Verification-Driven Development
21
star
18

testnets

Various different test network-related configurations for Tendermint
Python
15
star
19

audits

Security Audits by Informal Systems
TLA
15
star
20

hermes-ibc-workshop

Hermes IBC Workshop - Fungible Token Transfer (ics-20) between two Starport chains
TypeScript
14
star
21

cosmwasm-to-quint

Semi-automated modelling and Model-Based Testing for CosmWasm contracts
Rust
14
star
22

gm

Tool to manage local gaiad instances - without docker
Shell
13
star
23

flex-error

Rust
13
star
24

atomkraft-cosmos

TLA
12
star
25

verification

Specifications of the protocols and the experiments on their verification
9
star
26

hermes-sdk

Rust
9
star
27

jsonatr

JSON Artifact Translator
Rust
8
star
28

apalache-tests

Benchmarks for apalache
SMT
6
star
29

context-generic-programming

Context-generic programming guide
Rust
6
star
30

gopherator

Modelator's cousin for Golang
Go
5
star
31

apalache-bench

Apalache Bench Tests
HTML
5
star
32

vscode-itf-trace-viewer

VS Code extension for viewing ITF traces
TypeScript
5
star
33

mtcs

Multilateral Trade Credit Set-off
Rust
5
star
34

itf-rs

Rust library for consuming Apalache ITF traces
Rust
5
star
35

audit-celestia

Workspace set up for collaboration in the Celestia audit
Makefile
5
star
36

ibc-starknet

Meta repository for managing IBC Starknet projects
Cairo
4
star
37

stakooler

The koolest tool for Cosmos stakers
Go
4
star
38

megablocks

Prototype to investigate an Atomic IBC solution based on Megablocks
Go
4
star
39

quint-ml-experiments

F*
4
star
40

got

Game of Tendermint
Shell
4
star
41

themis-tracer

A tool for managing complex contexts for developing critical systems
Rust
4
star
42

quint-sandbox

Material used in interactive demos and tutorials
Bluespec
3
star
43

gravity-dex-demo

Instructions to run the Gravity Dex Demo
Go
3
star
44

chainpulse

Monitoring tool for IBC relayers
Rust
3
star
45

agoric-kernel-models

TLA+ models for Agoric Swingset Kernel
TLA
3
star
46

hydro

Hydro (aka AtomWars) project repo
Rust
3
star
47

kvstore-plus-plus

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

hermes-hackatom-demo

Demo for Hackatom - Hermes
TypeScript
2
star
49

cycles-sandbox

A playground for Cycles demos, experiments and prototypes.
Rust
2
star
50

apalache-chai

Chai: Client for Human-Apalache Interaction
Python
2
star
51

ics29-fee-tla

TLA
2
star
52

consumer-chain-tool

One-click Consumer Chain Tool
Go
2
star
53

sov-rollup-starter

Rust
2
star
54

itf-go

Go library for un/marshalling ITF files
Go
2
star
55

quint_awesomwasm24_workshop

Bluespec
2
star
56

merkleeyes

Go
1
star
57

OsmosisAtomkraft

Informal Systems Atomkraft adaptations and TLA specs for Osmosis audit project
TLA
1
star
58

euc

End-user computing for a better user experience
Shell
1
star
59

safe-regex

Fork of https://gitlab.com/leonhard-llc/safe-regex-rs
Rust
1
star
60

noir-ecies

Roff
1
star
61

ignite-blog

Cosmos-SDK blockchain following Ignite's Blog tutorial
TypeScript
1
star
62

economics-analysis

Economics analysis for various projects
1
star
63

ibc-proto

IBC Proto Rust implementation
Rust
1
star
64

reactor-experiments

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

cgp-workshop

Workshop materials for context-generic programming
Rust
1
star
66

partnership-heliax

Bluespec
1
star
67

cosmwasm-ibc

Facilities for implementing ibc-rs-powered light clients and applications as CosmWasm contracts.
Rust
1
star
68

hermes-sovereign-relayer

IBC Relayer for Sovereign SDK, powered by Hermes SDK
Rust
1
star