(The immediate question everyone has when contemplating this is "Can we get the LLMs to write the proofs and verifications?" and the answer is "yes, for uninteresting or unlikely to fail invariants, no for anything complex," with an asterisk for "maybe, if you hooked it up to an automated […]
