Well, it might also help to read them to see what tools you even want to use. As always, I suggest something you will enjoy in a category with practical applications immediately or down the line. There’s more practical stuff now than ever. Formal methods still ain’t at Github’s level, though. Still more to do. :)

Here’s a few areas of research to consider for what to verify:

1. Obviously, a formal semantics, compiler, or optimization for a specific language worth the time. Rust and Nim come to mind. People also keep building important stuff in C++ which was only partly done. Haskell had one, formal semantics done but no verified compiler. Maybe a useful Scheme like Racket or Chicken.

2. Tooling for automated proof of safety, termination, and so on for programs in a language like above with minimal specs a la SPARK or Frama-C. Optionally working on SAT/SMT solvers to get such languages closer to 100% on more problems with less schemes like ghost code. There’s lots of potential there.

3. Verifying models used in actual languages for safe/effective concurrency (eg Eiffel SCOOP) and/or parallelism (eg Cray Chapel or Taft’s ParaSail). Possibly a mockup in existing language with macros of such features with verified translator to regular code.

4. Verifying client-server or peer-to-peer protocols that have a lot of uptake for various properties. Optionally, making something like Verdi that already does it easier to use for non-experts or increased automation.

5. Verifying important data structures and sequential algorithms for correctness. Just make sure there’s a C implementation with x86 and ARM7-9 compatibility. If it performs well, people can wrap it in any language with C FFI.

6. GUI’s and graphics stacks. That occasionally gets work but not much of it. Graphics drivers are notorious for crashing. Just automated verification of them for safety like Microsoft’s SLAM and no race conditions might be helpful. Fully verification of an OpenGL stack or something might also be interesting. For GUI’s, something like Nitpicker would be easy whereas for GUI programming a DSL compiling to major toolkit would be the route. Maybe an OpenCL model. Who knows.

7. Increasing usability, automation, and performance of any tool people have used to do anything on that the lists above. There’s already lots of people increasing their assurance. Cost of verification is a more important problem right now, though. The lightweight methods need more power. The heavyweight methods need more automation. I did speculate about and find a HOL-to-FOL translator used to do the latter once. That, the use of model-checkers to filter before proving, and results of SAT/SMT tooling in general suggest there’s lots of potential here.

So, there’s you some ideas that might have immediate or long-term impact on problems that matter. There should also be something in that list you find fun. Maybe also something you know a lot about already. That can help. Either should have potential for projects worth spending a lot of time on.

If you’d like to practice on a juicy target, I invite you to join an effort to eradicate bugs in a database I’m working on in my free time, sled! It has a simple interface, but lots of optimizations that really need to be reliable. Nobody wants to use a database that very quickly deletes their data :P

I’ve been working extensively with property testing and a few tricks for shaking out interesting thread interleavings, and these approaches have yielded enough bugs to keep me busy for the last 6 months, but it’s time to really ramp up the rigor.

These are the approaches I believe will lead to the discovery of interesting bugs:

• formally specify the lock-free algorithms in use for the IO buffer and tree using TLA+, alloy, spin, iris etc… with the goal of identifying concerns that have not been considered in the implementation
• reproduce the functionality of quviq’s erlang PULSE scheduler using either ptrace or SCHED_FIFO/SCHED_RR in a test harness for performing parallel property testing as a rust library. Bring some of the awesome features of quviq’s quickcheck into the rust world.
• implement a concurrency testing library for rust that utilizes ptrace and z3 to get a nice user-friendly practical implementation of Maximal Causality Reduction to identify a minimal set of relevant interleaving schedules, and then use ptrace to schedule the threads according to the generated schedules to suss out crashes or violations of specified invariants.

Future directions include:

• building a versioned transactional store on top of sled
• building a horizontally scalable linearizable kv store on top of sled
• building a location-agnostic (phones, multi-dc, PoP’s) store powered by OT & CRDT’s on top of sled

The future focus on distributed systems will involve lots of interesting simulation, as well as an attempt to unify concurrency testing and distributed systems simulation. This is sort of a holy grail for me, and I hope to create tooling that lets people build significantly more reliable distributed systems, even more than the databases themselves.

Let me know if any of these directions sound like things you would be interested in collaborating on! You can find my email on github if so. Having this stuff on my github has resulted in a bunch of interesting people reaching out about jobs, and I haven’t been asked to do a single technical interview after referring companies to the project to see my output. This is a 100% non-commercial endeavor at this point, but I see it as earning interesting future job opportunities at the very least. I can’t tell you if commercial formal methods people will appreciate your work on these systems or not, but this is a real system that fills a real pain point (existing embedded db’s either have crappy read perf or crappy write perf, are generally confusing for people to configure, and often have poor consistency guarantees), and applying advanced testing techniques to this should actually save people from facing huge issues.

I’m a fan of the video course too, but having said that it will not actually teach you TLA+. For that you really need to study the book and the sample specs in the toolkit, but after the first 2 short (and delightful) videos you will have an understanding of what TLA+ is and what it (might) be useful for. The next 2 videos give you a deeper look.