We present two formal semantics for the core miniKanren. First, we give denotational variant which corresponds to the minimal Herbrand model for definite logic programs. Second, we present operational semantics which models interleaving, and prove its soundness and completeness w.r.t. denotational semantics. Our development is supported by formal Coq specification, thus making it certified.