You can get some of this without a proof tool, by arranging the code so that the bad state has no way in.
Statechart
Also called State machine, Finite state machine
A drawing of a system as the states it can be in and the moves between them. Anything not drawn isn't allowed, so a refunded order simply has no arrow to shipped. A statechart adds states inside states, and regions that run side by side.
Flags and if-statements are the easy thing to generate, and they allow combinations nobody meant. One status and a table of moves makes those impossible to enter. A chart also gives you something to check an agent's understanding against, without reading the code.
Say it to your agent
“Replace isPaid, isShipped and isRefunded in src/order.ts with one status field and a table of moves: pending to paid or failed, paid to shipped or refunded, shipped to delivered. Any other event returns an error and changes nothing. Draw the table as a Mermaid stateDiagram in docs/order.md, and test every event in every state.”