The formal, mechanized, verification of computer programs is a particularly difficult task in fast-evolving and complex development environments, as it typically is a slow process. To speed this effort up, verification efforts often target abstract models of these programs, and many implementation details are often left unverified in critical code. In this work, we propose to bridge the verification gap between a mechanized model and its implementation by leveraging property-based testing. Concretely, we present a light-weight automated tool for extracting F* specifications as OCaml predicates for its execution as a QCheck tests.