Can someone explain how this works from a 7/10 technical perspective? I hate reading articles that talk to you like youre five when trying to explain advanced concepts. I just want to know how it works in 1 paragraph and thats it.
Here was a lengthier diatribe of mine on a former Quanta article: https://news.ycombinator.com/item?id=22549988
Long version: Formal verification is a broad topic with a lot of different facets. But hopefully this sheds some light on some of the more useful ones:
Model-checkers like TLA+. You can specify an algorithm, say something simple like a bank account transfer where a sender's account is debited, and a receiver's account is credited. You can then set constraints, such that the sender's account must have enough to cover the transfer, etc. TLA+ will then run through all the scenarios in your algorithm to find corner-cases when the constraints aren't met. It's useful for modeling distributed systems, and you can try simulating an algorithm in parallel to see error conditions in multi-threaded code.
The downside to TLA+ is that you produce a specification, but still have to reproduce the specification in compilable/runnable code. I understand Amazon has had a lot of success using TLA+ to wring out potential bugs in systems before implementing them, and Leslie Lamport (author of TLA+ and creator of LaTeX, too) has some great (and entertaining) videos on his website explaining how they work: https://lamport.azurewebsites.net/tla/tla.html
There are formally-verifiable dialects of programming languages like the SPARK dialect of Ada, and Frama-C, which let you specify pre and post-conditions for functions, and then it will perform model-checking with flow analysis and SMT solvers to ensure those conditions are met in a way that's mathematically sound. Some conditions, like lack of buffer or integer overflows, are always checked. This way, code which has passed the proof stage can truly be said to be free of run-time errors, and whatever extra contracts you've added in your code will be met as well. Since all of this is checked at compile/proof-time, there's no run-time penalty for the extra assurance.
I came up with this simple example of SPARK code that proves if I have a function that doubles every element in an array, then the result satisfies a contract where every element in the output is even: https://pastebin.com/BtkaEDQ5
There are also proof assistants and theorem proving tools/languages like HOL, Isabelle, Coq, LEAN, and others which IMO fall under the umbrella of formal verification, but more on the computer science side than software engineering. In contrast, TLA+ and SPARK are very useful and practical for developing high-integrity software. Still, they're programming languages, and you can write executable code in them that can be said to be mathematically sound. A good resource is the Software Foundations course: https://softwarefoundations.cis.upenn.edu/
Some dependently-typed programming languages like Idris, F*, Dafny, and (I think) Liquid Haskell provide different mixes of these capabilities, but are geared towards producing usable software.
So you mentioned that it can handle things like overflows. Does this include all the things a fuzzer might find?
This article says "hacker-proof." Is that hyperbole (which implies 100% certainty in my mind) or is there a margin of error in this type of system. I'm just imagining things how large codebases with lots of maintainers still have bugs found every day from fuzzing. I would imagine if its near 100% that assumes the system that checks it is also free of bugs... quite fun to think about.
Getting started with SPARK, you'll see messages like "Can't prove that this variable won't overflow" (usually with corner cases like "when x = 4,294,967,295 and y = -1"). So it kind of makes you realize how error-prone code can be.
A statement like "x++" has the assumption baked into it that x isn't going to be INT_MAX. Fuzzers work by manipulating your control flow such that x _will_ be INT_MAX and cause an overflow or other bad stuff. Formal verification exposes all those assumptions and when people complain about slow development, it's because you're basically making the code "fuzzer-proof".
"Hacker-proof" is hyperbole, but not as much as some might have you believe. People have pointed out that the specification has to be correct. My code in the pastebin proves every element in the output array is even, but if the code is supposed to produce an array of odd numbers, then obviously that's still a bug, even though it's been "formally verified".
I wouldn't use the term "hacker-proof", but I would say "hacker-resistant". FV _can_ eliminate whole classes of vulnerabilities that attackers could otherwise use. A common trope is "well there's still hardware bugs or the spec could be wrong, so why bother?" I mean, sure, a hacker could cut the power to the datacenter, too, but IMO that's not a reason to ignore tools that can make the software we write much more robust.
One issue that can crop up is that you can't always prove what you're trying to specify. The state space can grow too big and the solver can't figure it out in a timely fashion, so you have to make assumptions and hope your tests give you enough confidence to deploy the system. This is basically the halting problem - it doesn't say that it's impossible to prove termination (or any other property) of some code, it just says that you can't _always_ prove them.
nVidia recently began using SPARK in some of their work, the video does a good job explaining some of the bugs that FV eliminates: https://www.youtube.com/watch?v=DZSSyWlsb28
Fuzzing still helps a lot in those cases! Especially if you focus on those kinds of problems.
In Coq you may define a set in terms of constructors of that set, for instance the set of natural numbers is:
Inductive nat : Set :=
| O : nat
| S : nat -> nat
The language is dependently typed, which means that expressions may be used as types. If you'd like to construct an "int" in C you may give an example such as "4". If you'd like to construct a value with "x < y" type in Coq, you must provide an example, either building it through theorems. As a programmer, it's a process similar to looking through an API manual, you know you have an object of one type and you know the type of the object you need, and you're trying to find the path that gets you one from the other. Often times the function you need won't already exist and you'll have to define a new function in code, then use that function in your proof.
For flavour, here's what that looks like in Coq. This is my attempt at defining natural numbers as Church Numerals, then defining multiplication on them:
Definition nat := ∀ X : Type, (X → X) → X → X.
Definition mult (n m : nat) : natIf you can build up value 'z' whose type is "x < y" then it's important that when you use it, it still be true that x is less than y later. For this reason, Coq is a functional programming language without mutability.
Dependent types have implications across the language. For instance you could have a record (like a C struct) whose three members are a numerator, a denominator, and a proof that the denominator != 0. Another cool thing is that it lets you write more expressive APIs such as a "pop()" function on a queue. In most languages your options are to make it undefined behaviour to pop an empty queue, or return a result type that may contain an error, or use exceptions if your language supports them. In Coq, you may define pop() as a function which takes a parameter whose type is a proof that the queue is not empty when called. (Due to Coq being pure functional, pop() also returns the whole post-pop queue.)
When proving, you have the goal to prove some statement, and some hypotheses that are known true in your current state. You may apply any theorems previously proven to transform your goal or hypothesis. Generally this means breaking the problem down into stages, such as splitting on 'and' and 'or', or performing induction on a variable. This proofing language is different from the programming language.
The best tutorial I've found online is for Lean prover, not Coq, but the concept is the same. (Indeed, other than lean using "rw" where Coq uses "rewrite", I can't recall any differences at all): https://news.ycombinator.com/item?id=22801607
The main problem I have with Coq is its lack of automation. If I understand the history, that's a bit of an ironic statement because Coq's main feature was its automation. The statements to "rewrite based on this theorem" or "split on 'and' and form two goals" are tactics, and Coq allows you to write your own tactics. There's no need for tactics to be proven correct, they can be full of bugs, either they show a path to produce a value with the right type in which case you have a proof, or they do not. My problem is that the Coq developers seem to share an opinion that the user is a mathematician who has considered the problem, developed a proof, attempted to formalize the proof on their own paper, and is as a last step entering their formalized proof into Coq. As a non-mathematician, I have done none of those things. I understand that they avoid doing things that may consume CPU time like trying every combination for a variable, but the "auto" tactic won't try 'true' and 'false' for a single boolean variable.
The one last step is that you can "extract" running code from Coq proofs. I've never done this myself, so I can't speak to it, but the idea is that you want to remove the concern that the code you've proven isn't the code you actually run. Coq can emit OCaml or Haskell.