Hacker News new | past | comments | ask | show | jobs | submit
m1el | on: LLMs are making formal software verification feasible at a much larger scale
> rather than having to translate the whole program into Rocq

Translating your program to Rocq is vastly easier than to write a proof for a binary.