Using Gemini 2.5 Pro, I added a fairly complete set of high level requirements, low level requirements, and unit tests. Doing so discovered a couple low priority issues with the internal functions. Most were around parameter checking. Since these are all internal functions, those issues were very unlikely to be a problem. So, I would rate the improved quality due to the unit testing as minimal.

However, the effort highlighted why certified code is difficult and expensive. For the 680 line source file, there are not 3,800 lines of test code. That's ignoring the effort to generate a set of high and low level requirements.