Find an additional case study, and write TLA+ monitors for it - Githubissues

freespek / solarkraft

Solarkraft: a runtime monitoring tool for Soroban, powered by TLA+ and Apalache

Apache License 2.0

12 stars 0 forks source link

Find an additional case study, and write TLA+ monitors for it #13

Closed andrey-kuprianov closed 1 week ago

andrey-kuprianov commented 6 months ago

Currently we have a single case study, a manual demo with the Timelock contract. We need to identify 2-3 additional case studies from soroban-examples, and write specifications for them in the form of TLA+ monitors.

This is the first stage for the above, with only 1 additional case study. This issue is completed when:

[x] 1 additional case study contract is identified;
- ~Liquidity pool contract: non-trivial, with interesting properties.~: this is for the second case study
- Token contract: sufficiently complex for the first pass.
[ ] inner workings of the contract are understood and documented;
[ ] correctness properties of the contract are formulated;
[ ] correctness properties are encoded as a composition of (simple) TLA+ monitors.

thpani commented 1 week ago

Closing this in favor of #136

@andrey-kuprianov If you wish to contribute another case study, this is very welcome!