While I love the trailblazing Tesla has done for EVs and smart cars, it's moments like these that make me cringe.

Obviously, we don't know right now if the driver was at fault or not - but I'm a capable coder and have some exposure to control theory as well as microcontrollers - and would be more than happy to audit Tesla's firmware.

Even more, I think there's a case to be made here for formal verification and high assurance languages such as SPARK.

It would be nice if you could pass the Tesla codebase to a formal solver and ask the solver "prove that pressing the brake never accelerates", and then have the resulting code and proof be made public.