Program logics are a powerful formal method in the context of program verification. Can we develop a counterpart of program logics in the context of language verification? This paper proposes language logics, which allow for statements of the form \(\{P\}~\mathcal {X}~\{Q\}\) where \(\mathcal {X}\) , the subject of analysis, can be a language component such as a piece of grammar, a typing rule, a reduction rule, or other parts of a language definition. To demonstrate our approach, we develop a number of language logics for analyzing various aspects of programming languages. We illustrate our language logics to the analysis of a faulty programming language. We have also implemented \(\textsc {Lang}\text {-}\textsc {n}\text {-}\textsc {Assert}\) , an automated prover for our logics, and we report on our experiments with the tool, which include the above-mentioned analysis on the faulty language. Ultimately, our language logics do not fully verify languages. Nonetheless, we believe that this paper provides a strong step towards adopting the methods of program logics for the analysis of languages.