Comment by y1n0

I fully agree it’s harder to read. I do chip design and I feel like formal is more common in this area, but I generally restrict it to very simple properties that are easy to understand without having to mentally solve a sudoku puzzle.

It’s to easy to write an assertion that looks like it checks what you want it to, and gives you a false confidence when it passes, only to figure out after a field failure that it wasn’t checking what you thought at all.

But I’d pay for a commercial set of properties and assertions that had guarantees, and not worry about their complexity. For something standard like cache protocols and bus protocols.

Other cases it needs to be pretty straightforward to grasp by a peer reviewer in minutes, or it’s not worth it.

But when you can hit the sweet spot, a set of easily understood properties (or complex but trusted properties), formal can save massive amounts of time.