A preprint makes a careful case for using the LLM as a per-function fact clerk, then letting Datalog and Z3 do the parts where hand-wavy code reading usually goes soft. The concrete claims are not small, including rediscovery of curl SOCKS5 and stb_vorbis bugs, a 102-byte ASan-triggering Vorbis input, and five libarchive findings. Worth reading becuase the evidence boundary is right there in the machinery, even if you still want to inspect the artifacts before treating it as a tool you can trust.