> Is it just simpler/easier to read than the code is, so they're easier to spot? Kind of. You basically annotate your program with pre/post-conditions, then yo

> Is it just simpler/easier to read than the code is, so they're easier to spot? Kind of. You basically annotate your program with pre/post-conditions, then you run the program through a theorem prover, which attempts to prove all of your conditions are true in all cases. The basic guarantee is that if you pass the theorem prover, your code will be free of array out-of-bounds accesses, null pointer dereferences, integer overflow, divide by zero, and other runtime errors. These are useful security properties to prove always hold, and you don’t have to explicitly write specifications for them (just conditions to help the prover along). If you want to go further (prove functional correctness of your program), you can add more specifications. A lot of times you just want to prove some basic sanity checks hold 100% of the time (e.g. always return a sorted array). These can be pretty easy to specify correctly.