Solarkraft is a runtime monitoring tool for Soroban, powered by TLA+ and Apalache.
We have finished the activation phase and developed an MVP.
🎥 Watch the 10-minute demo video by Jure Kukovec.
For more explanation, read our series of blog posts:
- Part 1: A New Hope – Why Smart Contract Bugs Matter and How Runtime Monitoring Saves the Day
- Part 2: Guardians of the Blockchain: Small and Modular Runtime Monitors in TLA+ for Soroban Smart Contracts
- Part 3: How to Run Solarkraft
- Part 4: The Force Awakens: Hybrid Blockchain Runtime Monitors
- Part 5: The Rise of Model Checker: Verifying Blockchain Monitors In and Near Realtime
Solarkraft is a tool for runtime monitoring of Soroban smart contracts. It tests whether a smart contract conforms to its specification during contract development, testing, and after contract deployment on the Stellar blockchain. The contract specification is written as an ensemble of TLA+ specifications, each capturing a property of the contract’s expected behavior.
Solarkraft inspects invocations of the timelock contract’s methods in the history of Stellar transactions. Whenever Solarkraft finds a deviation from the expected behavior (as prescribed by the monitor specifications) it reports a monitoring alert. Importantly, monitors are small snippets of code, not an entire specification. This makes them more accessible formal artifacts than usual.
We are grateful to the Stellar Community Fund for supporting our project via an Activation Award.
Check our latest pitch for our Community Award submission.
