NP Problem definition – verifiable on DFA vs. solvable on NFA
First, let me correct you: instead of a DFA there should be a deterministic Turing machine running in polynomial time, and instead of an NFA there should be a non-deterministic Turing machine running in polynomial time.

As you mention, both definitions are equivalent, and for this reason there is no single "go to" definition – you can use whatever definition is more appropriate in any single case.

Any formal development of complexity theory would necessitate picking one of these and then showing that the other is equivalent, but this is best left to the developers of these formal frameworks.

There are in fact many variants of Turing machines, so there are more than two definitions of NP. Even more equivalent definitions are provided by other models of computation such as RAM machines. Since all these definitions result in the same complexity class, they are all equally well definitions of NP.