Conventional unit tests are existentially quantified

which I am pretty sure are not proofs.

Is there a proof that has substance which starts off "there exists .." and doesn't end "for all .."?

As an exercise, look at a conventional unit test. Look at the inputs to a given assertion, let's say you test 1, 2, 5, 7. The proof would read "for all x in {1, 2, 5, 7}" - is that meaningful?

To try and make it more substantial, you could continue adding inputs. You would never reach universal quantification, because infinity is not a countable set.

Or, you could generalize your assertions until they are the strongest assertions that can be made for randomly generated inputs (the closest thing to universal quantification we can compute, or "for all" via "for an arbitrary")

Another argument for property tests, but maybe a new insight into a mapping from a conventional unit test to a property test.