1. 24

Hi,

I’d like to move my career towards formal methods and software verification. Almost every job posting understandably requires either an advanced degree or extensive prior work. I’m curious to hear from anyone who’s landed a job in this area with minimal previous experience in this specialization.

Do you recommend going back to school full time? Getting a job in an adjacent role at a company that’s willing to train? Or perhaps going to night school while at a such a company? Any tips on companies that are particularly friendly to training or self-learning and recruiting internally for such roles? Perhaps the “learn and blog about it” approach would work well?

I suppose this isn’t too different from other specialties though I would love to hear from anyone with experience in this particular area - especially about any companies friendly to formal methods newbies.

Thanks & happy Friday, everyone.

  1.  

  2. 7

    I recommend looking for a University that does it to learn or work on one of their projects. I suspect it’s very helpful to have experienced people to help you through your first year or two of verifying anything significant.

    In any case, here’s a write-up from one of best in field with advice and one book reference. The other books people mention are Certified Programming with Dependent Types by Chlipala and Software Foundations. If picking based on tooling, Coq and HOL (esp Isabelle) are used on best projects in software with ACL2 being used most for hardware.

    It also helps to see what lightweight verification is like if you need some motivation, a fallback, or just tell you something aint worth proving. Alloy (see site) or TLA+ (learntla.com) are best for that imho.

    1. 2

      Thanks Nick. I suspect it would be helpful to have experienced mentorship as well. It’s certainly a challenging - and large - area. Working with a University sounds like a great idea.

      Thanks for the link! I suppose it’s time to get back to writing algorithms and proving things ;)

      1. 4

        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.

        1. 2

          Thanks for the list. Programming languages are interesting to me and partly what drives my interest here, especially tools like Disel.

          I’m guessing #7, automation, will be increasingly interesting the further along I get here.

        2. 4

          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.

          1. 1

            I may have to dig with this. I find having practical examples to chew on while learning quite valuable. Your work looks great, congrats on your success!

        3. 2

          “I recommend looking for a University that does it to learn or work on one of their projects. I suspect it’s very helpful to have experienced people to help you through your first year or two of verifying anything significant.”

          True, you can found some of the courses and lectures in a list.

        4. 4

          What kind of industrial jobs have you found that are centered on formal methods?

          I was under the impression that that it would be a small part of any software development job.

          For example, I read the article about Amazon using TLA+. I’m pretty sure they didn’t hire a bunch of people with formal methods experience. It sounds more like the senior engineers tried it, decided it was a good idea, and then taught/spread formal methods within the existing dev team.

          Does anyone here use formal methods in their day job? If I had to guess, I would probably guess that less than 1% or even zero people reading this have applied formal methods to a piece of code that ships (I certainly haven’t). It seems like it’s more in the research phase, whereas you are talking about getting an “adjacent role at a company”. I could be wrong though.

          http://lamport.azurewebsites.net/tla/amazon.html

          1. 5

            I have! It was a really powerful tool in shipping code, but just that- a tool. It definitely wasn’t what I was hired to do, and in fact it wasn’t even expected at all: I just wedged it in and found it worked.

            To my understanding, most of the people whose job is specifically “use formal methods” are mostly in either hardware or academia.

            1. 7

              To my understanding, most of the people whose job is specifically “use formal methods” are mostly in either hardware or academia.

              That’s probably most of them, especially hardware if you want an industry job. Besides hardware companies using formal methods, there’s a little ecosystem of middleware companies selling the formal-methods tools, mainly to hardware companies. I’ve run across a handful elsewhere though. Financial companies occasionally advertise specifically formal-methods jobs (example). I’ve also seen ads on occasion from aerospace companies (no link handy). There’s Microsoft Research as well, which might even employ more people working on formal methods full-time than any single university does, but MSR is kind of an honorary member of academia.

              1. 3

                There’s Microsoft Research as well, which might even employ more people working on formal methods full-time than any single university does

                Maaaaaaaaaaaybe MIT is comparable, but that’s the only candidate I can think of. Outside of academia you also have INRIA, which is a French national research agency that produces a lot of stuff in formal methods too. Coincidentally enough, MSR and INRIA run a joint lab, which IIRC is where all the work in TLA+ happens.

                1. 5

                  Calling INRIA outside academia is… at least, a slight bit misleading, while technically true. People get PhDs at INRIA (technically they are issued by some other university, but their advisor and research is done at INRIA), and people who are at INRIA sometimes lecture at regular universities (I’m not actually sure how common this is, but talked to someone just a few months ago who was talking about doing this).

                  1. 1

                    Did not know this. Thanks for the correction!

              2. 1

                Awesome! How did you learn about formal methods – through school or self-taught?

                This kind of confirms what I was thinking. If you want to use formal methods at a software company, it’s unlikely you’ll be “hired in” for that. It’s more like you’re already a developer on a team, and you have to take the initiative to use it and teach your coworkers it and sell management on its utility.

              3. 4

                Data61 down here in Australia are often hiring Proof Engineers:

                https://ts.data61.csiro.au/jobs/proof-engineers2015

                1. 4

                  In industry I have have used Agda to prove code correct instead of testing it, because the tooling made it quicker to do than using property tests in Haskell.

                  1. 4

                    Whaaaaat!? You may be first person I’ve seen say it was quicker to prove code correct than use testing approaches. Makes me wonder if the code you were working on was a lot of straight-forward math in a functional style or something. You did mention Haskell. In any case, that sounds like it’s worth a write-up and submission to Lobsters for being practical, efficient, and about Agda in industry.

                2. 3

                  What kind of industrial jobs have you found that are centered on formal methods?… It seems like it’s more in the research phase, whereas you are talking about getting an “adjacent role at a company”.

                  As you suggest, not many :). Mostly hardware companies as others have pointed out. I was including industrial research without being explicit, so Microsoft Research and some other places, e.g. Galois count in my book. I think, in addition to the other suggestions here, I will start going through conference and journal publications to find some more leads.

                  1. 2

                    One easy trick is just going through the formal methods submissions in the publications looking at their University or corporate affiliation. I’ve also submitted quite a few tagged with formal methods here that you can just use Lobsters search for. You can also look for tool vendors such as company doing Atlier-B to see who their customers are. ProB is another with Z and TLA+ support. For instance, ProofPower led me to QinetiQ. AbsInt owns CompCert. Rosu’s group is doing Runtime Verification Inc. Smartcard vendors like Infineon or Gemalto use them a lot for higher-security stuff. Kesterel Institute is an old one that many outsourced to.

                    Just looking at the tools, papers, and reference sections takes you a lot of places. Helps to know the jargon that pops up a lot, too. Examples are Common Criteria EAL7 or DO-178B (recently DO-178C) since they often sold as a tool to aid certification. Or “formal methods industry.”

                3. 3

                  Don’t have experience with formal verification specifically, but some general advice:

                  1. Adjacent roles is good. Companies with more obscure technologies are often more willing to train, since they have no choice. And small startups will hire for much broader positions than the actual job posting, e.g. I was hired for backend skills but in practice I’m learning image processing as applied to gene sequencing.
                  2. Learn and blog is a fine thing too… if you have the time. I don’t, so tend to go for adjacent jobs if I’m interested in particular skillset (in this case, I wanted to learn scientific computing).

                  If you don’t have skills upfront, you also want resume that stresses your ability to learn quickly.

                  (Longer writeup here: https://codewithoutrules.com/2018/01/23/job-with-technology-you-dont-know/)

                  1. 1

                    Thanks! The tip for resumes is a good one. Sounds like you’re having fun learning in your new role.