diff --git a/collects/redex/private/rg-test.ss b/collects/redex/private/rg-test.ss
index a46e922206..08393a1a2d 100644
--- a/collects/redex/private/rg-test.ss
+++ b/collects/redex/private/rg-test.ss
@@ -504,62 +504,62 @@
       (get-output-string p)
       (close-output-port p))))
 
-;; check
+;; redex-check
 (let ()
   (define-language lang
     (d 5)
     (e e 4)
     (n number))
-  (test (current-output (λ () (check lang d #f))) 
+  (test (current-output (λ () (redex-check lang d #f))) 
         "counterexample found after 1 attempts:\n5\n")
-  (test (check lang d #t) #t)
-  (test (check lang (d e) (and (eq? (term d) 5) (eq? (term e) 4)) #:attempts 2) #t)
-  (test (check lang (d ...) (zero? (modulo (foldl + 0 (term (d ...))) 5)) #:attempts 2) #t)
-  (test (current-output (λ () (check lang (d e) #f)))
+  (test (redex-check lang d #t) #t)
+  (test (redex-check lang (d e) (and (eq? (term d) 5) (eq? (term e) 4)) #:attempts 2) #t)
+  (test (redex-check lang (d ...) (zero? (modulo (foldl + 0 (term (d ...))) 5)) #:attempts 2) #t)
+  (test (current-output (λ () (redex-check lang (d e) #f)))
         "counterexample found after 1 attempts:\n(5 4)\n")
-  (test (current-output (λ () (check lang d (error 'pred-raised))))
+  (test (current-output (λ () (redex-check lang d (error 'pred-raised))))
         "counterexample found after 1 attempts:\n5\n")
   (test (parameterize ([check-randomness (make-random 0 0)])
-          (check lang n (eq? 42 (term n)) 
-                 #:attempts 1
-                 #:source (reduction-relation lang (--> 42 x))))
+          (redex-check lang n (eq? 42 (term n)) 
+                       #:attempts 1
+                       #:source (reduction-relation lang (--> 42 x))))
         #t)
   (test (current-output
          (λ ()
            (parameterize ([check-randomness (make-random 0 0)])
-             (check lang n (eq? 42 (term n)) 
-                    #:attempts 1
-                    #:source (reduction-relation lang (--> 0 x z))))))
+             (redex-check lang n (eq? 42 (term n)) 
+                          #:attempts 1
+                          #:source (reduction-relation lang (--> 0 x z))))))
         "counterexample found (z) after 1 attempts:\n0\n")
   (test (current-output
          (λ ()
            (parameterize ([check-randomness (make-random 1)])
-             (check lang d (eq? 42 (term n)) 
-                    #:attempts 1
-                    #:source (reduction-relation lang (--> 0 x z))))))
+             (redex-check lang d (eq? 42 (term n)) 
+                          #:attempts 1
+                          #:source (reduction-relation lang (--> 0 x z))))))
         "counterexample found after 1 attempts:\n5\n")
   (test (let ([r (reduction-relation lang (--> 0 x z))])
-          (check lang n (number? (term n)) 
-                 #:attempts 10
-                 #:source r))
+          (redex-check lang n (number? (term n)) 
+                       #:attempts 10
+                       #:source r))
         #t)
   (let ()
     (define-metafunction lang
       [(mf 0) 0]
       [(mf 42) 0])
     (test (parameterize ([check-randomness (make-random 0 1)])
-            (check lang (n) (eq? 42 (term n)) 
-                   #:attempts 1
-                   #:source mf))
+            (redex-check lang (n) (eq? 42 (term n)) 
+                         #:attempts 1
+                         #:source mf))
           #t))
   (let ()
     (define-language L)
     (test (with-handlers ([exn:fail? exn-message])
-            (check lang any #t #:source (reduction-relation L (--> 1 1))))
+            (redex-check lang any #t #:source (reduction-relation L (--> 1 1))))
           #rx"language for secondary source"))
   (let ()
     (test (with-handlers ([exn:fail? exn-message])
-            (check lang n #t #:source (reduction-relation lang (--> x 1))))
+            (redex-check lang n #t #:source (reduction-relation lang (--> x 1))))
           #rx"x does not match n"))
   
   (let ([stx-err (λ (stx)
@@ -570,15 +570,15 @@
       (eval '(require "../reduction-semantics.ss"
                       "rg.ss"))
       (eval '(define-language empty))
-      (test (stx-err '(check empty any #t #:typo 3))
-            #rx"check: bad keyword syntax")
-      (test (stx-err '(check empty any #t #:attempts 3 #:attempts 4))
+      (test (stx-err '(redex-check empty any #t #:typo 3))
+            #rx"redex-check: bad keyword syntax")
+      (test (stx-err '(redex-check empty any #t #:attempts 3 #:attempts 4))
             #rx"bad keyword syntax")
-      (test (stx-err '(check empty any #t #:attempts))
+      (test (stx-err '(redex-check empty any #t #:attempts))
             #rx"bad keyword syntax")
-      (test (stx-err '(check empty any #t #:attempts 3 4))
+      (test (stx-err '(redex-check empty any #t #:attempts 3 4))
             #rx"bad keyword syntax")
-      (test (stx-err '(check empty any #t #:source #:attempts))
+      (test (stx-err '(redex-check empty any #t #:source #:attempts))
             #rx"bad keyword syntax"))))
 
 ;; check-metafunction-contract
diff --git a/collects/redex/private/rg.ss b/collects/redex/private/rg.ss
index 6174f0ac82..3b700c2424 100644
--- a/collects/redex/private/rg.ss
+++ b/collects/redex/private/rg.ss
@@ -655,11 +655,12 @@ To do a better job of not generating programs with free variables,
 
 (define check-randomness (make-parameter random))
 
-(define-syntax (check stx)
+(define-syntax (redex-check stx)
   (syntax-case stx ()
     [(_ lang pat property . kw-args)
      (let-values ([(names names/ellipses) 
-                   (extract-names (language-id-nts #'lang 'check) 'check #t #'pat)]
+                   (extract-names (language-id-nts #'lang 'redex-check)
+                                  'redex-check #t #'pat)]
                   [(attempts-stx source-stx)
                    (let loop ([args (syntax kw-args)]
                               [attempts #f]
@@ -678,9 +679,9 @@ To do a better job of not generating programs with free variables,
                      [attempts (or attempts-stx #'default-check-attempts)])
          (quasisyntax/loc stx
            (let ([att attempts])
-             (assert-nat 'check att)
+             (assert-nat 'redex-check att)
              (or (check-property 
-                  (cons (list #,(term-generator #'lang #'pat #'random-decisions 'check) #f)
+                  (cons (list #,(term-generator #'lang #'pat #'random-decisions 'redex-check) #f)
                         (let ([lang-gen (generate lang (random-decisions lang))])
                           #,(if (not source-stx)
                                 #'null
@@ -694,16 +695,16 @@ To do a better job of not generating programs with free variables,
                                                 [else
                                                  #`(let ([r #,source-stx])
                                                      (unless (reduction-relation? r)
-                                                       (raise-type-error 'check "reduction-relation" r))
+                                                       (raise-type-error 'redex-check "reduction-relation" r))
                                                      (values
                                                       (map rewrite-proc-lhs (reduction-relation-make-procs r))
                                                       (reduction-relation-srcs r)
                                                       (reduction-relation-lang r)))])])
                                     (unless (eq? src-lang lang)
-                                      (error 'check "language for secondary source must match primary pattern's language"))
+                                      (error 'redex-check "language for secondary source must match primary pattern's language"))
                                     (zip (map lang-gen pats) srcs)))))
                   #,(and source-stx #'(test-match lang pat))
-                  (λ (generated) (error 'check "~s does not match ~s" generated 'pat))
+                  (λ (generated) (error 'redex-check "~s does not match ~s" generated 'pat))
                   (λ (_ bindings)
                     (term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
                               property))
@@ -842,7 +843,7 @@ To do a better job of not generating programs with free variables,
 (define generation-decisions (make-parameter random-decisions))
 
 (provide pick-from-list pick-var min-prods decisions^ pick-sequence-length
-         is-nt? pick-char random-string pick-string check nt-by-name
+         is-nt? pick-char random-string pick-string redex-check nt-by-name
          pick-nt unique-chars pick-any sexp generate-term parse-pattern
          class-reassignments reassign-classes unparse-pattern
          (struct-out ellipsis) (struct-out mismatch) (struct-out class)
diff --git a/collects/redex/private/tl-test.ss b/collects/redex/private/tl-test.ss
index a8c52a7afd..78aae31d07 100644
--- a/collects/redex/private/tl-test.ss
+++ b/collects/redex/private/tl-test.ss
@@ -1,7 +1,5 @@
 (module tl-test mzscheme
   (require "../reduction-semantics.ss"
-           (only "reduction-semantics.ss" 
-                 relation-coverage make-coverage covered-cases)
            "test-util.ss"
            (only "matcher.ss" make-bindings make-bind)
            scheme/match
diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl
index 0335ffc8cd..1d9f533dde 100644
--- a/collects/redex/redex.scrbl
+++ b/collects/redex/redex.scrbl
@@ -47,9 +47,12 @@
      #'((tech "term") args ...)]
     [x (identifier? #'x) #'(tech "term")]))
 
+@(define redex-eval (make-base-eval))
+@(interaction-eval #:eval redex-eval (require redex/reduction-semantics))
+
 @title{@bold{Redex}: Debugging Operational Semantics}
 
-@author["Robert Bruce Findler"]
+@author["Robert Bruce Findler" "Casey Klein"]
 
 PLT Redex consists of a domain-specific language for specifying
 reduction semantics, plus a suite of tools for working with the
@@ -982,6 +985,103 @@ counters so that next time this function is called, it
 prints the test results for the next round of tests.
 }
 
+@defproc[(make-coverage [r reduction-relation?]) coverage?]{
+Constructs a structure to contain the per-case test coverage of
+the relation @scheme[r]. Use with @scheme[relation-coverage]
+and @scheme[covered-cases].
+}
+
+@defproc[(coverage? [v any/c]) boolean?]{
+Returns @scheme[#t] for a value produced by @scheme[make-coverage]
+and @scheme[#f] for any other.}
+
+@defparam[relation-coverage c (or/c false/c coverage?)]{
+When @scheme[c] is a @scheme[coverage] structure, rather than 
+@scheme[#f] (the default), procedures such as
+@scheme[apply-reduction-relation], @scheme[traces], etc. count 
+the number applications of each case of the
+@scheme[reduction-relation], storing the results in @scheme[c].
+}
+
+@defproc[(covered-cases 
+          [c coverage?])
+         (listof (cons/c string? natural-number/c))]{
+Extracts the coverage information recorded in @scheme[c], producing
+an association list mapping names to application counts.}
+
+@examples[
+#:eval redex-eval
+       (define-language addition
+         (e (+ number ...)))
+       (define reduce
+         (reduction-relation 
+          addition
+          (--> (+) 0 "zero")
+          (--> (+ number) number)
+          (--> (+ number_1 number_2 number ...)
+               (+ ,(+ (term number_1) (term number_2))
+                  number ...)
+               "add")))
+       (let ([coverage (make-coverage reduce)])
+         (parameterize ([relation-coverage coverage])
+           (apply-reduction-relation* reduce (term (+ 1 2 3)))
+           (covered-cases coverage)))]
+
+@defform*[[(generate-term language #, @|ttpattern| size-exp)
+           (generate-term language #, @|ttpattern| size-exp #:attempt attempt-num-expr)]
+          #:contracts ([size-expr natural-number/c]
+                       [attempt-num-expr natural-number/c])]{
+Generates a random term matching @scheme[pattern] (in the given language).
+
+The argument @scheme[size-expr] bounds the height of the generated term
+(measured as the height of the derivation tree used to produce
+the term). 
+         
+The optional keyword argument @scheme[attempt-num-expr] 
+(default @scheme[1]) provides coarse grained control over the random
+decisions made during generation (e.g., the expected length of 
+@pattech[pattern-sequence]s increases with @scheme[attempt-num-expr]).}
+
+@defform/subs[(check language #, @|ttpattern| property-expr kw-arg ...)
+              ([kw-arg (code:line #:attempts attempts-expr)
+                       (code:line #:source metafunction)
+                       (code:line #:source relation-expr)])
+              #:contracts ([property-expr any/c]
+                           [attempts-expr natural-number/c]
+                           [relation-expr reduction-relation?])]{
+Searches for a counterexample to @scheme[property-expr], interpreted
+as a predicate universally quantified over its free
+@pattech[term]-variables. @scheme[check] chooses substitutions for 
+these free @pattech[term]-variables by generating random terms matching
+@scheme[pattern] and extracting the sub-terms bound by the
+@pattech[names] and non-terminals in @scheme[pattern].
+
+@scheme[check] generates at most @scheme[attempts-expr] (default @scheme[100])
+random terms in its search. The size and complexity of terms it generates
+gradually increases with each failed attempt.
+
+When the optional @scheme[#:source] argument is present, @scheme[check] 
+generates @math{10%} of its terms by randomly choosing a pattern from the
+left-hand sides the definition of the supplied metafunction or relation.
+@scheme[check] raises an exception if a term generated from an alternate
+pattern does not match the @scheme[pattern].}
+
+@defproc[(check-reduction-relation 
+          [relation reduction-relation?]
+          [property (-> any/c any/c)]
+          [#:attempts attempts natural-number/c 100])
+         (or/c true/c void?)]{
+Tests a @scheme[relation] as follows: for each case of @scheme[relation],
+@scheme[check-reduction-relation] generates @scheme[attempts] random
+terms that match that case's left-hand side and applies @scheme[property] 
+to each random term.}
+
+@defform*[[(check-metafunction metafunction property)
+           (check-metafunction metafunction property #:attempts attempts)]
+          #:contracts ([property (-> any/c any/c)]
+                       [attempts natural-number/c])]{
+Like @scheme[check-reduction-relation] but for metafunctions.}
+
 @deftech{Debugging PLT Redex Programs}
 
 It is easy to write grammars and reduction rules that are
diff --git a/collects/redex/reduction-semantics.ss b/collects/redex/reduction-semantics.ss
index dfbd96b498..68c4c14a93 100644
--- a/collects/redex/reduction-semantics.ss
+++ b/collects/redex/reduction-semantics.ss
@@ -7,8 +7,6 @@
          "private/rg.ss"
          "private/error.ss")
 
-#;(provide (all-from-out "private/rg.ss"))
-
 (provide exn:fail:redex?) ;; from error.ss
 
 (provide reduction-relation 
@@ -43,6 +41,11 @@
          test-predicate
          test-results)
 
+(provide redex-check
+         generate-term
+         check-metafunction
+         check-metafunction-contract)
+
 (provide/contract
  [current-traced-metafunctions (parameter/c (or/c 'all (listof symbol?)))]
  [reduction-relation->rule-names (-> reduction-relation? (listof symbol?))]
@@ -61,4 +64,10 @@
                   (-> bindings? symbol? any)
                   (-> bindings? symbol? (-> any) any))]
  [variable-not-in (any/c symbol? . -> . symbol?)]
- [variables-not-in (any/c (listof symbol?) . -> . (listof symbol?))])
+ [variables-not-in (any/c (listof symbol?) . -> . (listof symbol?))]
+ [check-reduction-relation (->* (reduction-relation? (-> any/c any/c))
+                                (#:attempts natural-number/c)
+                                (one-of/c #t (void)))]
+ [relation-coverage (parameter/c (or/c false/c coverage?))]
+ [make-coverage (-> reduction-relation? coverage?)]
+ [covered-cases (-> coverage? (listof (cons/c string? natural-number/c)))])
\ No newline at end of file