Solarkraft is a runtime monitoring tool for Stellar Soroban, powered by TypeScript, TLA+ and the symbolic model-checker (a reasoning engine) Apalache.
Solarkraft is ready for first engine tests, in the form of a CLI-based MVP.
Recent updates: You can now write Solarkraft monitors in TypeScript! Additionally, we are working on comprehensive support for all Soroban features, including all Soroban storage durabilities and handling failed transactions.
Preparing for Warp 5! 🚀
We are grateful to the Stellar Community Fund for supporting our project in two generous funding rounds via an Activation Award and a Community Award. Check our project pitch for SCF #29:
If it has caught your attention, and you want to know more, reach out!
Blog
New! We have a series of blog posts dedicated to Solarkraft! Start reading:
-
Guardians of the Blockchain: Small and Modular Runtime Monitors in TLA+ for Soroban Smart Contracts (Solarkraft #2)
This is the second in a series of blog posts introducing Solarkraft, a TLA+-based runtime monitoring solution for Soroban smart contracts. The first post, “A New Hope – Why Smart Contract Bugs Matter and How Runtime Monitoring Saves the Day“ gives an overview of smart contracts, explains how traditional security fails to address major challenges…
-
A New Hope – Why Smart Contract Bugs Matter and How Runtime Monitoring Saves the Day (Solarkraft #1)
In this series of blog posts, I’m introducing Solarkraft, a TLA+-based runtime monitoring solution for Soroban smart contracts. We will start easy, with an overview of smart contracts, their principal vulnerabilities, and the traditional model of securing smart contracts, and an overview of how Solarkraft proposes a new solution.The following posts dive deeper into Soroban…