I kinda want to learn formal verification, but there are too many questions about actually implementing it in software. This implementation gap is one of them. Posting them here in case anyone has...
I kinda want to learn formal verification, but there are too many questions about actually implementing it in software. This implementation gap is one of them.
Posting them here in case anyone has answers:
How do you ensure that implementation matches the specification. I tried TLA+ modeling in a project, it caught a bug, which I read as sound and fixed it. That fix caused production outage, turns out I was modeling the concurrency wrong in TLA+ (because it is really hard to model it correctly and in performant way - if I coded to my specs the software would be serving a single user at a time instead of thousands).
From my recent search the best approaches would be:
Rocq of Rust (formerly Coq of Rust) from the Cryptocurrency world do this by converting your actual Rust code into Rocq code, then you write your proof in Rocq itself
Lean 4 is an actual programming language. I heard the Lean 4 compiler is self hosting, but I don't know how performant Lean 4 program could be and the ecosystem. Would you want to write an entire microservice in Lean? or does Lean has a good FFI so that critical sections can be written in Lean and wrapped in other languages (similar to how the Python community use Cython or PyO3)
What do you even prove for in a normal web application? For example, what proofs do you write to ensure that Tildes is bug-free?
What classes of software testing could Formal Verification can replaces? For example, assuming that the code 100% matches specification, do I still need unit testing if I can express all the test cases as theorem?
I'll try to answer your questions as best as I can. Just keep in mind it's only a subjet I'm interested in (and had a class 10+ years ago), but I'm not a professional in the field. Also, I have a...
I'll try to answer your questions as best as I can. Just keep in mind it's only a subjet I'm interested in (and had a class 10+ years ago), but I'm not a professional in the field. Also, I have a more software engineer point of view of formal verification, rather than a mathematician one. I have written a lot of code that IMHO would benefit tremendously from having some properties formally verified, but I haven't really designed anything where you have specs complex enough (and critical enough) that formal verification for the specs would make sense.
If you have separate specs and implementation, you can't really ensure that they match, unless you program the implementation in a language that has built-in formal verification (like Lean) and can be certain you mirrored the specs correctly. But at that point, it might be simpler and safer to just do everything in the language you're using. In some cases, it can still be useful to prove the specs without being certain the implementation matches. It really depends on how certain you want to be that your program is "bug-free".
You can prove a lot of useful stuff, even for a web app. Typically, you might have some parts of the app that require stuff that cannot be modeled by the type system (or at least, bot efficiently). Pre-conditions of functions/methods are stuff that are often up to programmers to ensure, but you would prevent a lot of bugs if you could ensure they are never violated. Ensuring your vector/array has at least n elements when accessing the nth, or not dereferencing a null pointer are examples of such pre-conditions. On a larger scale you might also want to ensure that you never leave your database in a "bad state" (e.g. with invariants violated) as a result of a request or transaction. However, I don't think you can ever prove that a program is "bug-free", as you can't really formalize what a "bug" is. At best, you can ensure your program is free of some classes of bugs (like buffer overflows) and has some specific properties.
In theory, you could replace all software testing with formal verification. If you prove that your test will pass, there is no need for running it. In practice, running the test might be a while lot faster than checking that the proof is correct. There are also cases where you juge that the guarantees you get from formal verification are not worth the effort.
Point 3 seems impossible even in theory. A proof models the environment that the code runs in. How do you check that your model matches the environment without testing it? For example, if the OS...
Point 3 seems impossible even in theory. A proof models the environment that the code runs in. How do you check that your model matches the environment without testing it? For example, if the OS has a bug, your model isn't going to include that bug. Similarly for a hardware bug or anything your modelled software communicates with that's outside the system boundary.
You need testing to discover what to model.
There are special proof languages where you can write code without running it, but that's because they're about proving mathematical theories.
That's a totally fair point. While the OS or even some aspects of the hardware could be part of the thing you prove, there is pretty much always something outside of that boundary that can still...
That's a totally fair point. While the OS or even some aspects of the hardware could be part of the thing you prove, there is pretty much always something outside of that boundary that can still mess things up (a cosmic ray flipping some bits, a grid voltage fluctuation causing unpredictable stuff to hapen in the CPU, undesirable quantum stuff, etc).
The original comment mentioned unit testing, and it's supposed to test code in isolation. So one could argue that proving that the code will pass the test fulfills the point of unit testing. But I don't think any sane person will fully isolate the piece of code being tested (for example, when you run it, you still rely on the OS doing proper memory management, if you call sort(), you're not going to mock that, erc...). And in my experience, it can be more useful for the "unit test" to include as many things in the test as possible as long as it doesn't make the test too slow or too complex, because that provides more testing for the other parts if the system.
Yes, I also avoid testing against mocks when testing against a real implementation is practical. (Databases and browsers come to mind.) On the other hand, testing in a real environment won't tell...
Yes, I also avoid testing against mocks when testing against a real implementation is practical. (Databases and browsers come to mind.)
On the other hand, testing in a real environment won't tell you whether your code is portable or conforms to a standard. Testing against multiple implementations is good for comparison. Maybe you could test against real browsers and also a theoretically ideal, abstract browser? That's where a proof might be useful, so you tell when your implementation is theoretically correct, but reality is letting you down.
Despite the paper’s famously accessible style, we’ve found bugs in every Raft implementation we’ve tested, including HashiCorp Raft, Aeron Cluster, OpenRaft, and MicroRaft — despite the investment in formal methods, careful code review, unit testing, and years of testing in production. The bugs we found manifest as violations of Raft’s main invariant (called state machine safety in the paper, commonly referred to elsewhere as total order delivery). If you’re using a Raft implementation, you might want to check it for bugs.
We’ve sent bug reports upstream. This isn’t intended as a critique of Raft, its authors, its implementers, or any particular implementation. Raft implementations, even with a formal specification and a detailed implementation guide, are not easy to write.
Rather, this is a story about correctness in distributed systems — the inevitability of bugs, the inadequacy of any single approach, and the high cost of learned helplessness.
[...]
In all cases, network partitions and turbulence were sufficient to surface examples of divergence (i.e. no node kill/restart required, or disk corruption, or other faults)
[...]
If there is a single lesson to be learned here, it’s that formal methods alone cannot ensure that software works, because the formal specification still needs to be implemented, and even if you have mechanized verification, you’re verifying the model and not the implementation itself.
We believe formal methods are useful and necessary — they can confirm the basic soundness of a design, and provide a map that saves engineers from many of the errors that can arise in the implementation of a complex system.
But as these bugs show, errors continue to arise when translating the formal specification to production code. In the course of our work with various Raft implementations, we identified a number of assumptions in the Raft paper that remain implicit. An implementer who misses any of these details is likely to run into trouble.
I kinda want to learn formal verification, but there are too many questions about actually implementing it in software. This implementation gap is one of them.
Posting them here in case anyone has answers:
I'll try to answer your questions as best as I can. Just keep in mind it's only a subjet I'm interested in (and had a class 10+ years ago), but I'm not a professional in the field. Also, I have a more software engineer point of view of formal verification, rather than a mathematician one. I have written a lot of code that IMHO would benefit tremendously from having some properties formally verified, but I haven't really designed anything where you have specs complex enough (and critical enough) that formal verification for the specs would make sense.
If you have separate specs and implementation, you can't really ensure that they match, unless you program the implementation in a language that has built-in formal verification (like Lean) and can be certain you mirrored the specs correctly. But at that point, it might be simpler and safer to just do everything in the language you're using. In some cases, it can still be useful to prove the specs without being certain the implementation matches. It really depends on how certain you want to be that your program is "bug-free".
You can prove a lot of useful stuff, even for a web app. Typically, you might have some parts of the app that require stuff that cannot be modeled by the type system (or at least, bot efficiently). Pre-conditions of functions/methods are stuff that are often up to programmers to ensure, but you would prevent a lot of bugs if you could ensure they are never violated. Ensuring your vector/array has at least n elements when accessing the nth, or not dereferencing a null pointer are examples of such pre-conditions. On a larger scale you might also want to ensure that you never leave your database in a "bad state" (e.g. with invariants violated) as a result of a request or transaction. However, I don't think you can ever prove that a program is "bug-free", as you can't really formalize what a "bug" is. At best, you can ensure your program is free of some classes of bugs (like buffer overflows) and has some specific properties.
In theory, you could replace all software testing with formal verification. If you prove that your test will pass, there is no need for running it. In practice, running the test might be a while lot faster than checking that the proof is correct. There are also cases where you juge that the guarantees you get from formal verification are not worth the effort.
Point 3 seems impossible even in theory. A proof models the environment that the code runs in. How do you check that your model matches the environment without testing it? For example, if the OS has a bug, your model isn't going to include that bug. Similarly for a hardware bug or anything your modelled software communicates with that's outside the system boundary.
You need testing to discover what to model.
There are special proof languages where you can write code without running it, but that's because they're about proving mathematical theories.
That's a totally fair point. While the OS or even some aspects of the hardware could be part of the thing you prove, there is pretty much always something outside of that boundary that can still mess things up (a cosmic ray flipping some bits, a grid voltage fluctuation causing unpredictable stuff to hapen in the CPU, undesirable quantum stuff, etc).
The original comment mentioned unit testing, and it's supposed to test code in isolation. So one could argue that proving that the code will pass the test fulfills the point of unit testing. But I don't think any sane person will fully isolate the piece of code being tested (for example, when you run it, you still rely on the OS doing proper memory management, if you call sort(), you're not going to mock that, erc...). And in my experience, it can be more useful for the "unit test" to include as many things in the test as possible as long as it doesn't make the test too slow or too complex, because that provides more testing for the other parts if the system.
Yes, I also avoid testing against mocks when testing against a real implementation is practical. (Databases and browsers come to mind.)
On the other hand, testing in a real environment won't tell you whether your code is portable or conforms to a standard. Testing against multiple implementations is good for comparison. Maybe you could test against real browsers and also a theoretically ideal, abstract browser? That's where a proof might be useful, so you tell when your implementation is theoretically correct, but reality is letting you down.
From the article:
[...]
[...]