Solarkraft
Solarkraft is a runtime monitoring tool for Soroban, powered by TLA+ and Apalache.
We have finished the activation phase and developed an MVP. See a 10-minute demo by Jure Kukovec. If you like it, read a series of our 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
Project Details
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.
Activation Award
We are grateful to the Stellar Community Fund for supporting our project via the Activation Award. Check our 3-minute pitch, and the project details below.
