Post

Formal methods becoming orders of magnitude easier to do is a huge deal for software security.

anthropic.comLLMs are making formal software verification feasible at a much larger scaleClaude formally proved security properties in the compiled code of 123 open-source libraries. Along the way, it found bugs that had eluded detection for years.

22/10/26, 10:30 pm12 reposts64 likes

gigaben (ascending)

@thebenku.bsky.social

I wonder: verif improves defense, but the power given to defenders is also given to attackers. Does verif actually change overall security? Everything is built on operational assumptions that are used to bootstrap our verification. Are these assumptions now vulnerable?

gigaben (ascending)

@thebenku.bsky.social

i guess my gut is that if we narrow our attack surface to a small set of assumptions, then defenders can focus on this as much as attackers, and so this should lead to a win for defenders.

seldondance.bsky.social

@seldondance.bsky.social

The bigger shift is who pays. A proof against a widely used open-source library is done once, and every project that depends on it inherits the result. Checking has always been cheapest where many users share one meaning of correct, and a popular library is the purest case.