Writing correct lock-free and distributed stateful systems in Rust, with TLA+

"Again, I don't know what you mean by "best". SPARK is a"

The OP is about TLA+ and Rust. Using Rust says they want something imperative, low-level, safe and fast. They also want easier verification. That eliminates all complicated tools (esp proof assistants) plus most of full verification. The parent of my first comment wanted to connect properties proven in TLA+ to the code itself. Maintaining low effort, that narrows it down to Frama-C, Java/JML, and SPARK. If they're a C expert, Frama-C is compelling due to all the other tools that can help them. Java/JML has a similar argument but complex runtime & patent suit-loving vendor (i.e. Oracle). SPARK has high automation, knocks out most of C's problems automatically, has tool support, and a non-malicious vendor. So, solution for this proposal is to try to encode correctness conditions from TLA+ or another analysis in SPARK.

"You can ensure memory and concurrency safety with or without language support, and it's unclear what you mean by "partial verification". For example, you could say that guarantees for memory safety and no race conditions are a good sweet spot."

Full verification is verification of all properties of an algorithm. Partial verification is verifying some of them. You don't really rank the two so much as you prioritize which properties to verify in a partial verification since you lacked time, budget, etc for full verification. Far as memory-safety and race freedom, OP chose Rust which already has that. So, it's a high priority to meet the safety standard OP already desires and has with TLA+ w/ Rust. It's really the OP's preference for easy, specific forms of safety, and efficient imperative language that are dictating my requirements here.

"For a very special kind of "can". seL4 is a 10KLOC C program that has been drastically dumbed down, and still took 20 man years! "

You keep leaving off two things when you mention that. One is that these projects have a habit of reinventing the wheel in tooling using their own languages, runtimes, extensions, new logics, etc. Reuse happens but CompSci likes building new stuff. They usually list around 70% or whatever high number of their effort goes into building new tools/theories. Reusing would drop that down a lot which is where the 5 years comes from. Strictly building on what we have would make that the median or max for a similar project with time coming down further as reusable components are developed. One can see that in ACL2, Isabelle/HOL and Coq ecosystems for projects that actually use what's already there. Or even in CompCert work where new CompSci just keeps adding new components to it to save time/effort.

The other thing is that seL4 targeted C language. That language wasn't designed for verification. By its history, it was barely designed at all starting with BCPL. This was also on shittiest, most-evolution-driven ISA in existence. They also built lots of new tools on top of some of the hardest ones. This thing was set up to be one of the hardest verifications in existence. Proven tools with languages designed to utilize them would reduce the hardness and increase iteration speed. We can see this with Myreen et al's work on CakeML vs CompCert. So much more has happened in less time since they started with a building block (a LISP verified to ASM), built another (a partial SML verified to ASM), and so on to get the big project (decent SML w/ optimizations verified to ASM). Their work was even used in seL4 to verify its assembly. That let it bypass building or needing a certified, optimizing compiler. Likewise, untrusted optimizations + verified, equivalence check let hardware and software verification cheat past a ton of difficulty w/ production cost being sequentially or concurrently running the checker over and over. Lots of potential cheats when designing for easy work w/ lots of reuse. Still hard but not seL4 hard for everything.

"Clearly, when you write a database and want to ensure serializability or no loss of data on failure, those are the most important properties by far. "

Such properties are to be done in another tool then broken down into properties to test on local, code modules. I imagine they'd need at least one specialist for that kind of verification. A database is hard enough that they'd probably be able to hire one. In any case, the OP is using TLA+ to check properties Rust can't. This would be using TLA+ or some other tool to check properties SPARK can't. Similar territory. Also, recall the COGENT work where the key components of an ext2 filesystem was done with half the code in C without painful analysis of mutable state that seL4 had to do. Easier proofs with C code coming out that preserves those properties.

"As there is no research -- as far as I know -- that tries to classify what constitutes a "reasonable program","

There has been under LANGSEC and prior in Abstract, State Machines. They verified them sequentially then their interactions in composition. The thing many keep rediscovering is the model for expressing them has to keep a certain amount of sequential and simple operation. Past as certain point, it becomes impossible to analyze automatically with existing methods. I'm not sure how much work has been done outside the ASM or LANGSEC research on that. We get it incidentally at least during the formal verification efforts: every attempt tells us what can be expressed, proven, etc. Really ad hoc, though.

"There is something interesting you could try, though: You could express global correctness properties in TLA+, and show (in TLA+) that they are preserved if some simple low-level properties are preserved, and then express and verify those in JML/SPARK. This is very interesting, and I'd love to hear about such an experience (or even try it myself), but my gut feeling is that that it would still be too costly. If someone does do that, however, that's something certainly publication-worthy."

That might have been how E-SPARK connected Event-B and SPARK. TLA+ is easier to use than Evdnt-B and often in similar domains. Ill try to remember this option.

Absolutely. Anyway this gap is worth mentioning for deeper understanding of a verification problem.