This demo introduces static program verification for JavaScript and shows how interactive development tools can support the programmer with understanding and resolving verification issues. No prior experience with formal verification is assumed.

In general, program verification relies on source code annotations such as pre-, postconditions and invariants in order to check the program for correctness for all possible inputs. By specifying the expected behavior in terms of logical propositions, program verifiers can support dynamically-typed languages such as JavaScript (including dynamic programming idioms and higher-order functions). However, the verification process can become complex, so simple error messages may not be sufficient to explain verification problems. In this demo, I will present an integrated development and verification environment based on the JavaScript program verifier. In particular, I will use a series of small examples to illustrate how counterexamples, an interactive verification inspector and an integrated step-by-step debugger can be used to understand and debug verification issues.