They'd estimated about 4-6 months for a two person team, made from some of the best engineers in the service, focused entirely on it to get it written, tested and out to production.
They decided to use TLA+ to model, despite neither engineer having used it before. They lost about a week to getting up and running with it (one engineer's only complaint was how tied in to Eclipse it was), and then spent the res of the month working on and modelling the whole task.
It found problems. A whole bunch of them. The fixed the model until finally TLA+ gave them an all clear.
Then came the coding. Well... that didn't take very long at all. The TLA+ model effectively outlined all the code and methods for them. The actual programming ended up being almost a cookie cutter simple code.
In total, the new and complicated component went from drawing board to tested and ready for production in about 2 months. Despite having had to learn TLA+, it ended up taking less time than if they'd not written the TLA+ models in the first place.