En este trabajo presentamos una propuesta para apoyar la enseñanza de métodos formales en una currícula de grado, usando el asistente de pruebas Coq y conceptos del área de Teoría de Tipos. Proponemos un taller de especificación, derivación y verificación de sistemas en los paradigmas de programación funcional e imperativo, que puede también ser adaptado a sistemas reactivos y de tiempo real. Describimos una primera experiencia en el desarrollo del taller y planteamos posibles cambios y extensiones.