> Did you see the recent post about the slow loading times in GTA 5?

Did you? It seems pretty obvious to me that Rockstar knew that this was slow as hell, and they were showing ads during that time window. Business interests are not software engineering interests, so I don't think problems like that would go away with something like this, no.

I don't know, a lot of people in that thread argued that this must've actually cost Rockstar a lot of money. I'm not sure which side of the argument is true, both sound plausible to me.

The people who can't be bothered to play now, will demand R* do something about the cheaters and people who bought their way to the top already. The people they gained won't stay, because R* won't ditch the people who actually make them money.

So all this will really do is put more load on their servers, now that the bottleneck moved off of your hardware and back onto thiers.

No, formal verification would not help with code being accidentally quadratic due to a standard library function doing something different from what the author thought it did. The lack of a formally verified json parser is also almost certainly not why the author of the code chose to roll their own parser rather than using one the of many pre-existing libraries.