A checker of Lean builds: proof holes, project axioms, native proofs, axioms outside a profile, unsafe and partial declarations, Lean's loop constructs, constants whose compiled code is replaced, constants whose value mentions a panic form, and a closed language checked before anything is compiled.