Production solver operator here (kaisersolver, we run on Arbitrum and Base). I come at this from the opposite end, verifying settlements rather than solver code, but a few things we ran into might help you scope.
Settlement-level invariants are cheap to write down and they catch real problems. We check sixteen per settlement using only public data: the auction id in the calldata matches the competition record, the settling address is the auction winner and a registered solver, exactly the winning solution’s orders settled at the scored amounts, every trade respects the signed limit, delivery actually reached the recorded receiver, the deadline was met, and so on. The rule that made the tool trustworthy is that a check may only say VIOLATION when public data proves it. Anything else is UNCERTAIN.
The bugs we found in our own tool were boundary and serialization bugs, which is basically your list. A node answering null for a transaction receipt gave us a false “reverted” verdict on a perfectly valid settlement. A calldata decoder accepted a non-canonical auction-id tail (length 8 mod 32) that the reference implementation rejects. A truncated calldata read decoded as a zero limit price. All three are hermetic test cases now, and both our engines (a Python CLI and a browser JS port) agree across an 80-settlement corpus.
If you want a live differential target: the circuit-breaker validator repo has an open issue from a core team member where its score came out about 2.06e12 wei below the autopilot’s on a capped price, which was enough to deny-list a solver on mainnet. Two implementations of one formula disagreeing by rounding is exactly what a fuzzer finds in an afternoon.
Happy to share the invariant list and the fixtures if that’s useful.