Domain-specific languages for hardware can significantly enhance designer productivity, but sometimes at the cost of ease of verification. We present PEak, an open-source hardware design and specification language, which aims to improve both design productivity and verification capability. PEak does this by providing a single source of truth for functional model, formal specification, and RTL implementation. PEak has been used in several academic projects, and PEak-generated RTL has been included in fabricated hardware accelerators. In these projects, the formal capabilities of PEak were crucial for enabling both novel design space exploration techniques and automated compiler synthesis.