I'm not an expert on modal logic, so take my answer with a grain of salt. I don't recall reading any discussion of a formal system where a quantified modal formula was an axiom of the system. (There may be some that I haven't come across, of course.) The point of adding quantification, and other devices that belong to first-order modal logical such as the property abstraction operator, is to increase the expressive power of the modal logic in order to use modal logic to formalize a broader range of natural language arguments that turn upon possibility and necessity.
Consider, for instance, the following "argument":
- Necessarily, the President of the United States is the President of the United States.
- Barack Obama is the President of the United States.
- Therefore, necessarily Barack Obama is the President of the United States.
3 would appear to follow from 1 and 2 by a substitution rule. But this is surely incorrect. It turns out that the problem is a kind of ambiguity in (1). It appears that we need a way to distinguish two different ways to ascribe modal properties, we need to distinguish, in other words:
1*. It is necessarily true of the President, that he is the President.
1**. It is true of the President, that he is necessarily President.
1* is a harmless conceptual truth, but 1** is a patent falsehood. But (3) would only follow only from 1** and 2, not from 1* and 2. So clearly, in order to avoid making fallacious modal arguments we are going to have to have some formal machinery to distinguish between cases like 1* and 1**.
Notice now that there isn't really any way to do this using just propositional modal logic. We're going to need some quantifiers, and we're going to need "property abstraction", which is the modal analogue to the definite descriptor in ordinary first-order logic. (For more details, I would recommend looking at the very nice exposition of this in the relevant chapter of Fitting and Mendelsohn's First-Order Modal Logic textbook.) In other words, the addition of the machinery isn't so much just to create new logical systems, but to give us the needed expressive power to avoid some paradoxes.