Refinement reflection: complete verification with SMT | Publicación