В статье представлена текущая реализация языкового сервера для интерактивного доказателя теорем Rzk. Она анализирует соответствующие технологии, связанные с языковым сервером Protocol, расширениями VS Code и доказателями теорем, и как на их основе строится языковая поддержка для Rzk.