Right, in effect you break down the possible function states along with a more rigorous form of targeted unit testing.

I don’t believe they used coq, but the sel4 Linux kernel is one of the most famous formally verified applications/systems.

https://github.com/seL4/l4v

The way to beat vulnerabilities is to use formally verified building blocks in my opinion.

You should look into Coq as it seems to have some good traction.

https://coq.inria.fr/