Indeed, this formalization effort spotted a flawed argument in one of the original publications and worked around it to repair the result.