Remember you can open a Github issue right here from Discord with the /create command.
Stella Issue Detector
#[old] Solarkraft
fallow sailBOT
stray dagger
Solarkraft aids smart contract developers and auditors in finding critical bugs both during development and after deployment.
Solarkraft allows you to write brief code snippets of expected contract behavior (runtime monitors), and to verify that on-chain transactions conform to this specification.
For example, the following Solarkraft monitor specifies that a claim against a timelock contract should revert if an upper claim time bound is no longer satisfied:
MustRevert_claim_BeforeTimeBound(env) ≜
Balance.time_bound.kind = "Before" ∧ env.timestamp > Balance.time_bound.timestamp
🚀 Using our SCF #24 Activation Award, we’ve developed an MVP consisting of:
- a language for writing runtime monitors based on TLA+
- a CLI fetcher component that retrieves relevant transaction data from Horizon
- a CLI verifier that checks the retrieved transaction data against given runtime monitors using the symbolic model checker Apalache
- a case study using the timelock contract from soroban-examples
🎬 Check out our demo video on YouTube
📚 For more details on how to write runtime monitors, take a look at our (growing) series of technical blog posts
fallow sailBOT
stray dagger
[old] Solarkraft