ibc icon indicating copy to clipboard operation
ibc copied to clipboard

Published 20 hours ago • verified publisher icon cosmos

TLA+ spec of CCV

Open Kukovec opened this issue 2 years ago • 1 comments

This PR ports and updates the previously created CCV TLA+ spec from https://github.com/cosmos/interchain-security/tree/jk/ISaudit. It includes additional modeling of provider-side timeout.

Kukovec avatar Jan 16 '23 15:01 Kukovec

@mpoke applied the review suggestions. Decided to leave the invariants from the old QA document (but the link is fixed), since it is unclear how we will proceed with it.

p-offtermatt avatar Apr 04 '23 11:04 p-offtermatt

As discussed we will close this PR and add a link to the existing Quint spec.

crodriguezvega avatar Mar 28 '24 16:03 crodriguezvega