This is a nice overview of what is feasible today: careful coding with strongly typed languages, manual vetting of dependencies, and background work on formally verifying small critical components. Very heartening to see!
yea, this is a great application of the quality spectrum. What’s interesting is, they don’t even mention unit testing. They start right at fuzzing and go all the way to formal verification.
wasm has a great story for formal reasoning. Fun fact: it has a full formal specification. It also has a full mechanized proof in a proof assistant (Isabelle). If memory serves me correctly, some people were also working on formalizing it in another proof assistant.
This makes it a very interesting choice of target for verification efforts.