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.