VsRocq est une extension pour Visual Studio Code et VSCodium qui fournit un support avancé pour le prouveur interactif Rocq (anciennement Coq). Il permet aux utilisateurs de vérifier des preuves mathématiques, de développer des logiciels certifiés et d'enseigner la logique formelle grâce à une intégration fluide avec l'éditeur. L'outil offre des fonctionnalités comme la vérification continue des preuves, une interface interactive pour explorer les objectifs de preuve et un panneau dédié aux requêtes.