It doesn't necessarily solve this completely, but it can be used to significantly reduce the amount of code you have to manually audit. For example, you could u

It doesn't necessarily solve this completely, but it can be used to significantly reduce the amount of code you have to manually audit. For example, you could use tokens to represent permissions, and arrange your code so that only a small portion of your code can create them. Then you can rely on the presence of that token indicating that a check has been performed in the rest of your code. The type system is a tool to reduce the space of invalid inputs.