I provide a tableau system and completeness proof for a revised version of Carnap's semantics for quantified modal logic [1946]. For Carnap, a sentence is possible if it is true in some first order model. It is a fundamentally semantic conception of modality. As with second order logic, no sound and complete proof theory can be provided for this semantics. Arguably this contributed to the disappearance of Carnapian modal logic from contemporary philosophical discussion. The proof theory I propose comes much closer to Carnap's semantic vision and provides an interesting counterpoint to mainstream modal logic.