Comment by joomy

Yes, we were careful not to call it that. I still don't mind calling our programs verified, since they are verified in Rocq and we do our best to preserve the semantics of them. Right now the only measure we have is testing a small set of programs and also carefully picking a subset of C++ that we trust. Our future plan is to generate random Rocq programs, extract them via Crane, and compare the output to the outputs of extraction to OCaml, and even CertiCoq, which is a verified compiler from Rocq to C, (mostly) proven correct with respect to CompCert semantics.