atomkraft
A model-based end-to-end testing framework for Cosmos SDK blockchains, using TLA+ models to generate and execute test scenarios.
Overview
Atomkraft Cosmos is a community-driven test suite for Cosmos SDK blockchains, built on the Atomkraft framework. It enables automated, model-based end-to-end testing by generating concrete test scenarios from abstract TLA+ specifications, allowing developers to validate core blockchain functionality efficiently.
Key Features
- Model-Based Testing — Uses TLA+ models to describe system behavior and automatically generate diverse test traces.
- Automated Test Generation — Produces multiple test scenarios from concise TLA+ assertions via the Apalache model checker.
- Real Blockchain Execution — Executes generated abstract traces against live Cosmos SDK blockchains using custom reactors.
- CI-Ready Test Suite — Provides pre-generated pytest scripts for seamless integration into continuous integration pipelines.
- Trace Visualization — Supports the Informal Trace Format (ITF) and integrates with VSCode plugins for easy trace inspection.
Philosophy
Atomkraft Cosmos emphasizes rigorous, automated validation of blockchain behavior through formal models, aiming to deliver high test coverage and reliability for Cosmos SDK modules with minimal manual effort.
Related Projects
Found a gem we're missing?
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.
