It is neither common nor easy but actually provably impossible. Please read this piece carefully: https://pron.github.io/posts/correctness-and-complexity
You must be misunderstanding the work if you believe that what is being done routinely is impossible.
Quite possibly I don't understand what you mean by "work". If by "work" you mean creating provably correct software then no, it is not done routinely.
People create wholly deterministic state machines all the damn time.
What do you mean by "wholly deterministic"?
You can buy an 8-bit adder/accumulator from a catalog.
It is neither common nor easy but actually provably impossible. Please read this piece carefully: https://pron.github.io/posts/correctness-and-complexity