Are there open free USB designs?
The usual place to look is opencores – if you only include FPGA-proven designs you also rule out these that only look good on paper. Your USB functionality is under the "Communication controller" category.

Formally verifying a design is a tough task, and I congratulate you on the choice of first looking into something basic.

I personally am not so sure that formally verifying a USB controller is the only way to go – in the end, both sides of a USB link have to cooperate, and being correct doesn't help you if you still can't work with the (possibly incorrect) other end (I don't even think the USB spec is formally proven).

However, I'd encourage you to look into yosys, whose author held a pretty interesting talk about how to prove designs (rather than just testing it) based on induction.



Since the USB standards are open, you should probably just download and read the specs, too.