So you feed the LLM some C code like zlib and it rewrites and proves it. The goal is to make the code write-only and replace it with spec declaration? ... math

So you feed the LLM some C code like zlib and it rewrites and proves it. The goal is to make the code write-only and replace it with spec declaration? ... math ppl still cant accept the "x = 1;" statement :)