[unexpectedtrap]

Correctness of the kernel and consistency of the theory implemented in it are different things. Gödel’s theorems prevent you from proving the latter, but not the former.

[codebje]

Interesting - what is correctness of the kernel here? That it faithfully implements the model?