Leah Neukirchen @ GPN24 on Nostr: pretty sure it does: "Passes a completed proof term to Coq's kernel to check that the ...

pretty sure it does: "Passes a completed proof term to Coq's kernel to check that the proof term is well-typed and to verify that its type matches the theorem statement."