How helpful are these TLA specs for actual ibc-rs or ibc development?

[michwqy]

I am new to blockchain and not familiar with formal analysis. I wonder how helpful these TLA specs are for actual blockchain development. Does it help to find some design or implementation bugs? Any assistance you can provide would be greatly appreciated.

[adizere]

We used the TLA specs for:

• developers to gain more familiarity with the protocol
• to find and catch bugs, see disclosure here: https://github.com/informalsystems/hermes/blob/master/docs/disclosure-log.md
• for a higher-level description of the protocols, which onboarding developers might be able to understand faster than reading the relayer codebase in Rust directly