Well yes, you _can_ verify ML-based systems (and I discuss briefly how in the linked article). It is just that this is much harder with such systems than with HW or SW systems for which "you have the source code".

What I meant by "Because ML systems are opaque, you cannot really reason about what they do" (perhaps I was not being clear) was this: You can indeed _observe_ what they do, but being able to actually inspect the source makes verification much easier and more reliable: You know what parts of the logic you have covered, you can think of "danger areas" (and direct testing to them), and you can simply check whether all the cases you can think about have been covered in the source.

With opaque systems, you have no idea whether e.g. your ML-based autonomous vehicle will recognize people-painted-on-a-bus as people-on-the-road, until you actually test for that. And then you have to test people-painted-on-a-truck.

What I meant regarding "modular verification" is that you can check sub-modules according to some spec (or at least according to informal comments). This is quite different from what you can do when analyzing NN layers.

I suspect you are right in claiming (in your last paragraph) that one will always have to choose between "more understandable" and "more accurate". But I think we can do various things (the DARPA suggestion being one of them) to make the "more accurate" solution more verifiable.