Curvance appears to be a lending and borrowing protocol. In order to ensure their protocol was secure, they asked Trail of Bits to write a large amount of fuzz tests for their project. This included raw fuzzing looking for crashes and also invariant fuzzing to ensure that the protocol works as intended.
What are invariants? They are core properties of the system that should always hold true. I felt that the invariants for this went more into the actual functionality as opposed to high level invariants, but that is just semantics. As an example, "Calls to createLock with an amount value less than WAD fail" for the VeCVE functional invariants.
Many of the invariants were extremely specific to the functionality. It felt like "what would be bad if XXX went wrong". So, once the invariants were hooked into the Echidna fuzzer with a sufficient harness, they let it go to work. They found 12 unique bugs from this, including a few fairly catastrophic vulnerabilities. To me, the main reason this works is that the validations for specific pieces of functionality were so specific. People think fuzzing is the easy way, which really isn't the case.
The report notes that there are some limitations with this setup though. Oracle prices, and external token interactions are good example of large state explosion if not properly restricted. So, they had to really simplify this setup to make the fuzzing work. Overall, a good reference for writing deep invariants in order to find deep bugs!