This repository includes formal models of different Internet Computer (IC) components. Many of the models model canisters (IC smart contracts), but some model other aspects of the platform (e.g, subnet splitting, or a basic model of the consensus algorithm, or SEV/SNP upgrades).
The repository is organized by the different analysis tools. Currently, there are TLA+ models and Tamarin models.
NOTE: if you've come here from the blog post describing the TLA+ models, note that they've now been moved to the tla subdirectory. Adjust the paths accordingly.
We're currently not accepting external contributions.