3 ms·
As far as I know, it hasn't been formally verified. Andrea Lattuada (https://andrea.lattuada.me/ https://andrea.lattuada.me/) is more likely to have done work
by jamesmunns 3y ago
As far as I know, it hasn't been formally verified.
Andrea Lattuada (https://andrea.lattuada.me/ https://andrea.lattuada.me/) is more likely to have done work in his implementation of the algorithm than I did on mine.
I have run the testing with various dynamic analysis tools, but for sure this isn't formal verification. If someone is interested in doing it, happy to chat with them!
- anonymousDan 3y agoShouldn't be that hard to at least model check it in TLA+ I would have thought (albeit potentially more complex if trying to account for weak memory).