As far as I know, it hasn't been formally verified.

Andrea Lattuada (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!