I always wondered why aren't smart contracts developed strictly; proving them with Coq or some proof assistant, or making a formal TLA+ struct to define them before coding. As the siblings say, it smells like contractors that don't take it as seriously as (imo) they should.