What I've Learned About Formal Methods in Half a Year

As someone who was working on this decades ago [1][2], here's a useful recap.

- Back then, CPU power for the prover was a big problem. That's been fixed. We were too early in the days of a 1 MIPS VAX.

- Prover theory is much better. We were using the Oppen-Nelson prover, the original SAT system. Now that's routine technology.

- Loose languages are a problem. You have to nail down all "undefined behavior", and either detect it and forbid it, or give it precise semantics.

- Integrate the verification annotation into the programming language. Not as comments. It should be at least syntax and type checked when the program is compiled, and it should use essentially the same syntax as the language to which it is attached. Otherwise the annotations get out of date and nobody uses them.

- Break big assertions into lots of little assertions. Don't AND them. This improves the diagnostics.

- Debug the verification in the source language, by adding asserts. The verification system usually treats asserts as a proof goal, and assumes they are true for the code that follows. You narrow down the problem into a small area in that way. If you need to prove something hard, get to the point where you have "assert(a); assert(b);", and need to prove that A implies B. Then you use an offline prover. Don't work on the code problems in a prover directly.

- You're not done until you get 100%. If you write "assert(false);", there is only one error but the verification is totally meaningless.

- Don't get carried away with the formalism. Verification systems tend to be built by people who think formalism is cool. That is a negative for getting work done.

- Undecidability and the halting problem are not issues. If your program is anywhere near undecidable, it's broken. Microsoft took the position with their Static Driver Verifier that if the verifier can't decide termination easily, it doesn't get to be a signed kernel driver.

- Some things are hard to specify, and some things aren't. A database is an example of a complicated system that's not too hard to specify. The specification is a full table search of giant arrays. The implementation doesn't do it that way, but it's supposed to behave as if it does. The other extreme would be a GUI program.

[1] http://www.animats.com/papers/verifier/verifiermanual.pdf

[2] https://github.com/John-Nagle/pasv

No, you can just type `\nat` and the Lean extension in VScode will turn it into `ℕ`. Similarly, you can type many LaTeX macros, and the will render in unicode. Examples: `\times` becomes `×` and `\to` becomes `→`, etc...

> This is why you can unplug Pratt and Whitney engines from an airplane and plug in Rolls-Royce engines.

Wait wut? Are you talking about their embedded software or the hardware itself? Because if you're talking about the hardware, I'm about to be dumbfounded that there are formal verifications of hardware, my mind is about to be blown.

You could think of many of the formal tools outside of dependently typed programming as design by contract plus a thingy that complains if the contract doesn't work.

Not at apple: The following is about 10 years out of date, would be interesting to know what's changed:

10 years ago formal had just started to be viable in run of the mill semiconductor verification (as opposed to throwing a bunch of specialist PhD grads at the problem); Jasper Gold was the first tool I heard of that worked well enough. pre-formal, the approach was to write a bunch of tests with input stimulators and validity checkers and/or assertions, and then work on the stimulators until you reached 100%coverage (signing off the cases that couldn't happen). That's not just line coverage, but each branch of an if, each component of a boolean expression must toggle, each bit of a signal must toggle, etc.

Reaching 100% coverage was a tedious exercise so the first use of formal was as a sumplement, to find the last,most difficult test cases that completed your coverage (or prove that the cases were impossible). The next use was to try and prove directly that assertions or test failures could not occur, or provide a counterexample. this is all based on the tool being able to read low level verilog or systemC code.

What it couldn't do at the time, which would be interesting to know if it can now, is as follows: Often, you actually have a higher level model of the behavior of your system. The RTL code is written to have the same behavior (manually, because it takes expertise to choose RTL code that will work efficiently). Ideally, provers would simply prove that your RTL has the same behavior.