In software engineering, sometimes tests arent' enough. Tests are great! They help us know that our footguns shoot straight - but how can we know we're aiming in the right direction? That would mean "debugging" our design with formal methods, and not the implementation of it with tests.

This post is a very brief introduction to the kind of tools that exist to help you figure out if your code can could even be correct without writing a single line of code, and where I think they can be most profitable in the Julia ecosystem.

Projects that I'll cover:

• JET.jl

• Decision tables and Part 2

• Z3

• Model checking and TLA+ and Alloy

• Fuzzing

• Coq/Lean formal verification

Courses: