Sudoku is a puzzle, typically on a 9x9 grid made up of nine 3x3 subgrids, where every row and column must contain every number between 1 and 9, exactly once, and every 3x3 subgrid also contains every number exactly once. Some squares in the puzzle are already filled out, which act as constraints. The rest are blank, and need to be filled in through logical reasoning. The solution is unique.
Write a module and use formal verification to solve the "hardest Sudoku puzzle in the world".