Primary source for the equivalence of non-deterministic polynomial time and deterministic polynomial time verification Who was the first person to show that a language is in NP if a certificate for the language can be verified in polynomial time?  Do we have a paper that formally proves this?  When did the TCS community start de-emphasizing non-determinism in favor of verifiability? I cannot, for the life of me, find a good reference for this beyond texts like Papadimitriou and Arora and Barak.
[An extended comment] I think that the "roots of verification" are already contained in Karp's milestone paper "Reducibility Among Combinatorial Problems" (1972):


  ...
  Let $P^{(2)}$ denote the class of subsets $\Sigma^* \times \Sigma^*$ which are recognizable in polynomial time. Given $L^{(2)} \in P^{(2)}$ and a polynomial $p$, we define $L$ as follows:
  
  $L = \{ x \mid $ there exists $y$ s.t. $\langle x,y \rangle \in L^{(2)}$ and $\log(y) \leq p(\log(x)) \}$


(however Karp doesn't call $y$ a "certificate")


  ... We refer to $L$ as the language derived from $L^{(2)}$ by $p$-bounded existential quantification.
  
  Definition 4. $NP$ is the set of languages derived from elements of $P^{(2)}$ by polynomial-bounded existential quantification. 
  
  There is an alternative characterization of NP in terms of nondeterministic Turing machines ... [definition of computation of a nondeterministic Turing machine] ... 


and 


  ... Theorem 1: $L \in NP$ if and only if $L$ is accepted by a nondeterministic Turing machine which operates in polynomial time ...