Interesting report on Anthropic's efforts to formally verify code: https://www.anthropic.com/research/formal-verification with more details in the appendix https://www-cdn.anthropic.com/files/4zrzovbb/website/6867eadf760258fa8b42a504600cd3c036d16358.pdf
Especially interesting for me personally: as a formal methods researcher I started looking at cybersecurity a few decades ago in the hope that security might be a killer application for formal verification. We managed to get some results, eg. verifying some security and safety properties of an SSH implementation (see https://www.cs.ru.nl/~erikpoll/papers/wits.pdf), but even for Java code this was very labour-intensive, so that we did not even begin to attempt it for C code or binaries.
www.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.