> My next "big" project will be a data visualization system that's probably going to need some Python, JavaScript, and some simple bash piping between the pytho

> My next "big" project will be a data visualization system that's probably going to need some Python, JavaScript, and some simple bash piping between the python scripts. Unfortunately, there aren't great deductive verification tools for either Python or JavaScript. Perhaps more importantly, there's also not a particularly good understanding of how to formally verify front-end code. The most important property of a visualization system is something like "the visualization accurately represents the data being visualized", but in a problem domain like this, formalizing the high-level intent is probably harder than actually proving that this intent is achieved. Additionally, the cost of throwing an exception at runtime are presumably pretty low (unlike in a control system, for example). So once you've formalized your spec, you can just check your specs at run time throw an exception/report a bug instead of or in addition to generating the possibly faulty visualization. Are there key components of the visualization pipeline that could threaten its correctness? E.g. data reduction, interpolation, fancy graphics code, etc.? If so, I'd focus on those and come up with a good set of formal, checkable-at-runtime contracts that capture your high-level informal specification. Alternatively, is it possible to do some computation on your output to check that it matches the input data? E.g. you could imagine counting pixels of certain colors on a heat map or pie chart and comparing that to the original data. That way you don't have to verify (or trust) all of the graphics generation code, thus significantly reducing your trusted computing base. Saying "we have a formal mathematical description of what it means for this portion of the visualization system to be correct, and a way of checking input/output matches that description" is probably a more significant contribution than actually churning through a static verification effort. > it'll be nice to flash and say "I used formal methods to prove this implementation" as it is going to be for an academic's project. Are you sure this is the case? Most academics, even within CS, don't care much about formal methods. If you're just looking to learn formal methods, then I guess it's whatever. But if you're looking to stand out, you might want to figure out what's important to your stake holders and focus on that. I'd be pleasantly surprised if the answer to that question is formal methods.