Both the implementation and the proof are written in Lean. In the files I reference here https://github.com/schildep/verified-3d-mesh-intersection#mi... there are theorems about the function that does the mesh intersection computation. The implementation is in the CSG/Impl folder. The proof is in the CSG/Proof folder. They are imported and tied together in the human reviewed file. Lean checks that these theorems in the human reviewed file are proven via the proofs.