Formal verification, or formal correctness proofs, are powerful tools when designing your FPGA or ASIC "gateware". They help finding bugs sometimes missed in simulation, triggered by corner cases you didn't think to check. This talk will give a little background on how they work, the available ecosystem of tools, show some small examples on how to use them, and some practical results from real-life usage.