We found a first bug! The very last slide on loop formulas reloaded misses a technical detail:

The slides underlying the video on loops have a bug on page 245: the theorem misses that set X must be a model of the program. This is fixed in the new version of the slides.