> "Formally verified software" means that some portion of the software's expected behavior has been rendered as a proposition, and that proposition has been proven correct using some kind of proof assistant or theorem-proving software that we assume correctly validates the proof of the proposition.

All programs that don't contain undefined behavior satisfy this (in an annoying tautological way) because all programs are proofs of themselves. So the thing you're getting paid for, if you are, is to ask the right questions of your theorem prover (which may be a Python interpreter).