I only am familiar with formal verification in the context of a hardware class, which is like programming but the cost:benefit is wildly different (can’t fix a

I only am familiar with formal verification in the context of a hardware class, which is like programming but the cost:benefit is wildly different (can’t fix a physical chip after it has been fabricated very easily) and the types of designs are very different. But, the impression I got was that the rigors of the formal verifier would sort of impose a limit on the complexity of the design just based on… completing in a reasonable timeframe and in a reasonable amount of memory space. Maybe the true victory of demanding formal verification would be fixing: > software is big and complicated and hard to get right By making big complex programs a pain to work with, haha.