For automotive software the ISO 26262 is the equivalent to RTCA DO-178 in avionics. ISO 26262 highly recommends that ASIL C and D-classified systems utilize semiformal and formal verification among other techniques to verify software unit design and implementation.
That is because the formal method supplement of the DO-178C is RTCA DO-333. There you have about a hundred pages concerned with the application of formal methods.
And what the OPAL functional language [1] did since the mid 80s. Though the concept there is expanded from simple reference counting by additional static analysis during compile time (making use of the functional semantics of the language) to avoid reference counting when for example the compiler can find/prove sequential increment/decrement counts, then the reference counting code is eliminated.
No, a domain-consistent all-different propagator such as the one desccribed in [1] is sufficient to determine a valuation domain for a Sudoku puzzle without any search.
Of course that does not hold in general, but in the special case of Sudokus and problem modelling by a domain-consistent all-different propagator, no search is required for a solution.
[1] A filtering algorithm for constraints of difference in CSPs, J-C. Régin, 1994
Yes, but even better there is the global constraint geost [1] which is specifically for this purpose in k-dimensions; see also [2] for a more detailed presentation.
Unfortunately, Gecode does not provide it (and you would have to express it in form of other, more lower level constraints which gets quickly complicated), and neither does Google's OR-tools which have a nice Python interface.
There is JaCoP which provides the geost global constraint and makes it available via the declarative MiniZinc problem description language so one needs not to use the Java API.