We present a prototype for a tool that enables programmers to verify their code as they write it in real-time. After each line of code that the programmer writes, the tool tells the programmer what it can prove about the program so far and indicates potential oversights or potentially violated assumptions. Once the programmer has finished writing the program, it is already verified with a mathematical correctness proof. Other tools providing real-time feedback already exist, but ours is the first one that only relies on a small trusted proof checker and that provides a concise summary of all the facts that are provable at the point in the program currently being edited, as opposed to only indicating whether user-stated assertions or postconditions hold.
Program verification requires loop invariants, which are hard to find and tedious to spell out. We explore a middle ground in the design space between the two extremes of requiring users to spell out loop invariants manually and attempting to infer loop invariants automatically: Based on the observation that a loop invariant often looks quite similar to the symbolic state right before the loop, our tool asks users to express the desired loop invariant as a diff from the symbolic state before the loop, which has the potential to lead to less verbose and more maintainable proofs.
We prototyped our technique in the interactive proof assistant Coq, so our framework creates machine-checked proofs that the developed functions satisfy their specifications when executed according to the formal semantics of the source language. Using a verified compiler proven against the same source-language semantics, we can ensure that the behavior of the compiled program matches the program's behavior as represented by the framework during the proof. Additionally, since our polyglot source files can be viewed as Coq or C files at the same time, users willing to accept a bigger trusted code base can compile them with GCC.