[nwatson]

You might model software data and operations in some formal system at various levels using a language like "coq" and develop some formal verification proofs. I've not read this book that apparently explores verifications like these: "Certified Programming with Dependent Types: ...".

I'm not sure what types of enterprises actually use formal verification since it's very costly. Writing software is much faster than verifying it. Embedded auto, aerospace, industrial applications, sure. Facebook? I doubt it.

Such methods could be useful, maybe coupled with fuzzing, for breaking software too. It might suggest avenues for exploit.

Systems like coq are used more naturally in math proofs, but even there it's very hard to apply.

[philipodonnell]

It came up for me when designing a custodial management system for cryptocurrencies, where you could design it in such a way that the different steps/sensitive data were divided among separate systems and communication channels. I wanted some way to divide up responsibilities for processing a transaction (initiation, audit, control, approval, transmission) and then prove that any single component could be 100% compromised without allowing further unauthorized transactions. Even introducing temporary transformations (encryption/hashing) and re-routing keys specifically to prevent collisions of that data.

I noticed how similar the thought process was to GDPR work I've been involved in, where, for example, we can keep track of Last name and Phone Number in our company, but they could never be at rest unencrypted and unhashed in the same system. Or First Name + Job Title + Location but only 2 of those three can co-exist. It seemed like the kind of thing that would have a formal way of expressing. Our GDPR consultants were unhelpful in that.