> If you have a limited budget of tokens as a defender, maybe the best thing to spend them on is not red teaming, but formalizing proofs of your code's security.

You can only do this if you have a very clear sense of what your code should be doing. In most codebases I've ever worked with, frankly, no one has any idea.

Red teaming as an approach always has value, but one important characteristic it has is that you can apply red teaming without demanding any changes at all to your code standards, or engineering culture (and maybe even your development processes).

Most companies are working with a horrific sprawl of code, much of it legacy with little ownership. Red teaming, like buying tools and pushing for high coverage, is an attractive strategy to business leaders because it doesn't require them to tackle the hardest problems (development priorities, expertise, institutional knowledge, talent, retention) that factor into application security.

Formal verification is unfortunately hard in the ways that companies who want to think of security as a simple resource allocation problem most likely can't really manage.

I would love to work on projects/with teams that see formal verification as part of their overall correctness and security strategy. And maybe doing things right can be cheaper in the long run, including in terms of token burn. But I'm not sure this strategy will be applicable all that generally; some teams will never get there.