Josef Widder

> [ ] Josef's comments above Not sure what @adizere means here. Is there something I should do? Or should we add my comments to the spec?

It would definitely be useful to have this feature for MBT and audits. Actually I was surprised that it is not possible at the moment. I thought that because the...

> The thing is, we can simply remove some restrictions from Quint, and use the predicate directly, since apalache does accept that I am not sure I understand this completely....

Makes sense. Thanks! This is what I thought I understood, but I wasn't sure. I just wanted to be sure ;-)

The question was, what is the reason for the punishment delay? The delay stopped them to perform redeems for 24 hours. As the fees are spread over all participants, the...

I think for many specs we can work around that. Even in the draft spec that I have written, I first had written temporal formulas where indices don't range over...

There is another argument for the asynchronous explicit mature packet design (compared to the synchronous design with additional assumptions on delays and relative clock drifts etc). To the best of...

Thanks for the pointer! I guess the main problem is combination of the two types. E.g., if I have some temporal property A, and then in the process of refinement...

I agree. Up to know we have focused on the verification side, in particular regarding the structure and content of the English spec. As next step we should incorporate engineering...

It would be good to have tests when the primary (or secondaries) are not responding. In this case we should timeout and FetchLightBlock should report timeout errors. In case of...