Certainly I'm glad we have better tools now, and know the rules. Sure beats the old days. As for verification, well I'm big into Lean 4 and it plays well with NSA since transferring theory and proofs between finite and infinite saves a lot of labor on the computer.
Oh I wasn't trying to say that NSA is in any way non-rigorous, only that if you make it rigorous it does require some machinery that is itself not terribly straightforward.
As for whether that's worth it or not, I have no strong opinion.
