Hacker News new | past | comments | ask | show | jobs | submit
jsenn | on: LLMs are making formal software verification feasible at a much larger scale
This is really cool work. The particular spec structure/methodology does seem awkward though:

1. Prove the ASan-instrumented binary doesn't crash

2. Prove the non-instrumented binary doesn't crash

3. Prove the instrumented and non-instrumented binaries have the same behaviour (under a particular model of a Linux process's behaviour)

This is a clever hack for automatically generating a formal spec for an existing program, but the fact that you need ASan in there makes it seem like this is less general than it sounds. Could the agents directly prove that out of bounds memory accesses don't occur on the original binary and skip ASan altogether? It's convenient to let the spec just be "it doesn't crash", and ASan provides a crash when the other bad things you care about happen (i.e. out of bounds memory accesses), but I wonder if modelling the memory accesses directly would simplify things.

saagarjha | parent
Agents can't really reliably prove things (at least not cheaply) hence the desire to chain together tools that can be checked.