[otterley]

Would formal validation of these algorithms (e.g. with TLA+) help avoid such bugs?

[happyPersonR]

I thought there was in the past and some of the flaws found were addressed in facebooks version of this

https://doi.org/10.1145/3452296.3472912

Toward formally verifying congestion control behavior | Proceedings of the 2021 ACM SIGCOMM 2021 Conference

[kedihacker]

I think a audited algorithm where each type is strictly defined like int32 added to that really help with what exactly should be inputted to it so it remains correct.