there is a culture of type safety which is a very watered down machine checked proof that the thing entering a function has affordances X,Y and Z. Its not the end to end functional verification you are talking about but its not nothing either.