There's a model checker that can directly verify Rust code, Kani https://model-checking.github.io/kani/ - I wonder if Servo could use it in this case?

Or maybe https://github.com/tokio-rs/loom

The problem with most of these tools is the same as when we got the UML driven development craziness, most of them don't map to the actuall source code being written, and most often than not, mistakes get introduced as the actual implementation doesn't match the model.

What the industry is missing is more adoption of Design by Contract, formal verification clauses (SPARK and Frama-C style), Type Driven Development, across mainstream languages, alongside more love for stuff like Dafny, F* and such.

If you haven't seen those already, you might also want to check out:

  - Apalache: a symbolic model checker for TLA+ backed by Z3 (https://apalache-mc.org)
  - Quint: a modern and executable specification language with TLA+-like semantics, that integrates with Apalache (https://quint-lang.org)

I also didn't expect to find it, partially because I've had basically no exposure to it... I've heard about these formal verification tools but I never really grasped them or felt like they applied to any of the problem domains I work in.

But WOW did the example here really drove home how it could be a very useful tool for me. I can think of a few projects I've worked on or reviewed in the last year where I'd have considered using this, and still am.