Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Model and verify IBC connection versioning in TLA #117

Closed
3 of 4 tasks
ancazamfir opened this issue Aug 14, 2020 · 0 comments
Closed
3 of 4 tasks

Model and verify IBC connection versioning in TLA #117

ancazamfir opened this issue Aug 14, 2020 · 0 comments
Assignees
@istoilkovska

Comments

@ancazamfir
Copy link
Collaborator

Summary

Following up on issue cosmos/ibc#459 opened by @adizere.
Add connection versioning to the connection TLA model in https://github.com/informalsystems/ibc-rs/tree/master/docs/spec/connection-handshake/L2-tla

Problem Definition

Described in cosmos/ibc#459

Proposal

A couple of proposals are described in cosmos/ibc#459.

We should:

  • model the current ICS spec and SDK code and show the safety issue
  • model the proposals and verify safety and liveness properties

For Admin Use

  • Not duplicate issue
  • Appropriate labels applied
  • Appropriate contributors tagged
  • Contributor assigned/self-assigned
@adizere adizere mentioned this issue Aug 25, 2020
Merged
6 tasks
@hu55a1n1 hu55a1n1 transferred this issue from informalsystems/hermes Sep 29, 2022
livelybug pushed a commit to octopus-network/ibc-rs that referenced this issue Oct 14, 2022
@istoilkovska @adizere
Relayer TLA+ refactoring (cosmos#117)
8e3716c 
* relayer restructuring

* refactoring the relayer

* changed file structure

* removing v2

* Added RelayerDefinitions.tla and addressed some comments

* Update docs/spec/relayer/README.md

Co-authored-by: Adi Seredinschi <[email protected]>

* addressed comments

* fixed fairness constraint

Co-authored-by: Adi Seredinschi <[email protected]>
shuoer86 pushed a commit to shuoer86/ibc-rs that referenced this issue Nov 4, 2023
@tac0turtle
rename confio to cosmos (cosmos#117)
39702c6 
Co-authored-by: Marko Baricevic <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@istoilkovska istoilkovska

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@ancazamfir @istoilkovska