Formal proof of correctness of Levenshtein distance
As pointed out in a comment above, the answer is yes, in Lean.  See the paper and the code as linked into comments.
I was rather hoping Agda or Idris... but perhaps the Lean formalization is actually constructive.