Proof - BFS gets shortest distance

Induction on the frontiers.
Assume for the n-1 frontier, we processed the previous n-1 layers.
At such state, we are going to process the n layer.
Since the algo should have processed the n-1 layers, the neighbors of the n-1 layers which are the n layers must be in the stack.
QED.