VSMIPS A formally verified MIPS processor with a classic 5-stage pipeline without bypassing. Exceptions and interrupts are not handled. The processor is implemented in Simplog and verified in Isabelle/HOL.