I work on space craft flight software and exactly none of it is formally verified. As far as I know, it's not practical to do so. If we could do it (without ballooning cost and schedule 10x), we would.
A large portion of Microsoft's in house developed device drivers for windows are formally verified.
Boeing together with DARPA built an autonomous helicopter on top of the formally verified Sel4 microkernel https://ts.data61.csiro.au/projects/TS/SMACCM/
Another one:
Wireguard uses formally verified implementations of ed25519 https://github.com/project-everest/hacl-star
Never saw any crash happen there.
You should think of these systems like you think of garbage collection. They lower (sometimes eliminate) one particular kind of problem, and that's it. It does not prove the code works, doesn't OOM, doesn't segfault, doesn't dos itself, doesn't enter infinite loop, etc.
Honest question (I obviously don't have a ton of experience in this area), what does "model-checked in TLA+ though the applications themselves are not written in TLA+" mean (in terms of the guarantees you're getting)? If you're not verifying the actual code, then how do you prevent bugs creeping during whatever happens between verification and actually writing the application code?
The HACL* project looks interesting. I would definitely accept that as an affirmative answer to my original question.
Code review! So, SO much code review. Also testing and type systems and linters and code review.
(There's also some work on automatic synthesis, like PGo, but that's all very, very far from being production-ready.)
The main benefit of using TLA+ is that it lets you hammer out issues in the high-level design. Less "oops this has a buffer overrun" and more "oops if this service stalls out for too long our recovery mechanism will violate a core safety guarantee." Turns out that lots of the nastiest bugs are in the design, not the implementation, so using TLA+ saves a lot of time and money. But you still need to code review!
Yeah, but we already have processes to manage the latter. It's the (potential) buffer overruns that keep me up at night!
>Turns out that lots of the nastiest bugs are in the design, not the implementation
I'm not saying it never happens (does TLA plus make sure everyone's assuming SI units?), but that hasn't been my experience at all.
I'd _hope_ you'd have those processes, working on space flight and all :P. Good processes > good tools. It's easier to start using a good tool than overhaul your process. So for people who don't have that kind of discipline or heavyweight process, TLA+ gives a lot of benefits for really cheap. AWS, for example, found it really easy to slot into their workflow.
Re buffer overruns, I just remembered OpenComRTOS, which used TLA+ to verify low-level properties of their code.[1] They found it super helpful.
> I'm not saying it never happens (does TLA plus make sure everyone's assuming SI units?), but that hasn't been my experience at all.
'Fraid it probably can't help you with the SI units. I'm thinking about "design bugs" more like this:
> 1. Suppose we have a document with version 57
> 2. A bulk of delete and reindex will remove the index-v57, increase the version to 58 (for the delete operation), then put a new doc with version 59. While the engine places the index-59 into the version map, the safe-access flag is flipped over (due to a concurrent fresh), the engine won't put that index entry into the version map, but also leave the delete-58 tombstone in the version map. The delete-58 tombstone is stale because the latest version of that document is index-59.
> 3. Another bulk of delete and reindex will increase the version to 59 (for a delete) but won't remove docs from Lucene because of the existing (stale) delete-58 tombstone. The index operation will append document (version 60) to Lucene (instead of overwriting). At this point, we will have two documents with the same id.
Which was a bug TLA+ found in ElasticSearch.[2]
[1]: https://dl.acm.org/doi/10.5555/1779934.1779955 [2]: https://github.com/elastic/elasticsearch/issues/31976#issuec...
In Ada you can do Design-by-contract but in the SPARK subset you can actually formally prove the implementation's correctness.
SPARK is used to my knowledge in rail signalling system, air traffic control systems, Class III medical devices, and now also NVDIA plans to use it for sections of their ADAS platform.
I think the cost aspect is overblown. The biggest issue is that anything related to Ada is not really that well known and often what is known is based on stereotypes from the 80's. Also for most people they would not see it as career growth move to switch to an Ada based technology stack.
I suspect there'd be a lot of stuff using either SPARK or Event-B, but Tokeneer[3] is the only thing I found with five minutes of Googling.
[1]: https://www.microsoft.com/en-us/research/publication/ironfle...
[2]: https://www.cs.purdue.edu/homes/pfonseca//papers/eurosys2017...
Logical problems (and problems in C extensions) are of course always possible, therefore you have Stateflow and other methods. Other formal methods cannot guarantee that neither.