Verified Regular Expression Matcher Environment Tested on "The Coq Proof Assistant, version 8.16.1 compiled with OCaml 4.14.0" Checking proofs $ make