It is possible to prove that a piece of code matches a given mathematical specification. That spec has to be good though, and there can still be hardware failures (e.g. bitflips), problems with the environment (if not proven correct as well), and more. It theoretically is possible though that way to at least 100% secure a not-too-complex piece of software by itself (without hardware).
