Push down automaton for Language of same number of as and bs
The usual approach is to prove by induction the following kind of statement:


  The set of configurations reachable from the initial state upon reading a word $w$ is ...


Here ... depends on $w$. Having proved this kind of statement, you can deduce which words are accepted by your machine, hence proving its correctness.