Los motores de base de datos son actualmente empleados como componentes esenciales en el desarrollo de sistemas informáticos. Inicialmente utilizados para el almacenamiento físico de información, en la actualidad ofrecen funcionalidades avanzadas que distan mucho de sus versiones iniciales. Entre estas funcionalidades se encuentran los triggers o disparadores, que ofrecen una alternativa eficiente para la incorporación de reglas de negocio en la base de datos. De esta manera es posible delegar responsabilidades que inicialmente son consideradas parte de la aplicación. Como cualquier componente en el desarrollo de software, es deseable garantizar la corrección de esta pieza del sistema. El objetivo de este trabajo es proponer una técnica para la verificación formal de propiedades de las operaciones de base de datos con la incorporación de triggers. Para esto se crea un especificación de las operaciones, en el lenguaje PVS, a partir de las definiciones de los disparadores. Finalmente, este modelo es utilizado para la demostración de propiedades deseadas.