diff --git a/collects/redex/private/keyword-macros-test.ss b/collects/redex/private/keyword-macros-test.ss
new file mode 100644
index 0000000000..fe39d4baaf
--- /dev/null
+++ b/collects/redex/private/keyword-macros-test.ss
@@ -0,0 +1,46 @@
+#lang scheme
+
+(require "keyword-macros.ss"
+         "test-util.ss")
+
+(reset-count)
+
+(let* ([formals `((#:b . ,#'1) (#:c . ,#'2))]
+       [parse 
+        (λ (actuals) 
+          (map syntax-e 
+               (parse-kw-args formals (cdr (syntax-e actuals)) actuals)))])
+  (let-syntax ([msg-src
+                (syntax-rules ()
+                  [(_ expr)
+                   (with-handlers ([exn:fail:syntax?
+                                    (λ (exn)
+                                      (values (exn-message exn)
+                                              (exn:fail:syntax-exprs exn)))])
+                     (begin expr (values 'no-msg 'no-src)))])])
+    (let ()
+      (test (parse #'(a #:c 3 #:b 4)) '(4 3))
+      (test (parse #'(a #:b 4 #:c 3)) '(4 3))
+      (test (parse #'(a #:c 3)) '(1 3))
+      (let*-values ([(kw) #'#:b]
+                    [(msg src) (msg-src (parse #`(a #,kw)))])
+        (test msg #rx"a: missing argument expression after keyword")
+        (test src (list kw)))
+      (let*-values ([(arg) #'1]
+                    [(msg src) (msg-src (parse #`(a #:b 1 #,arg)))])
+        (test msg #rx"a: expected a keyword")
+        (test src (list arg)))
+      (let*-values ([(kw) #'#:c]
+                    [(msg src) (msg-src (parse #`(a #:c 1 #:b 2 #,kw 3)))])
+        (test msg #rx"a: repeated keyword")
+        (test src (list kw)))
+      (let*-values ([(kw) #'#:c]
+                    [(msg src) (msg-src (parse #`(a #:b #,kw 3)))])
+        (test msg #rx"a: expected an argument expression")
+        (test src (list kw)))
+      (let*-values ([(kw) #'#:typo]
+                    [(msg src) (msg-src (parse #`(a #:b 3 #,kw 4)))])
+        (test msg #rx"a: invalid keyword")
+        (test src (list kw))))))
+
+(print-tests-passed 'keyword-macros-test.ss)
\ No newline at end of file
diff --git a/collects/redex/private/keyword-macros.ss b/collects/redex/private/keyword-macros.ss
new file mode 100644
index 0000000000..e5a0b42a03
--- /dev/null
+++ b/collects/redex/private/keyword-macros.ss
@@ -0,0 +1,28 @@
+#lang scheme
+
+(define (parse-kw-args formals actuals source)
+  (let loop ([current (for/hash ([arg formals]) (values (car arg) #f))]
+             [rest actuals])
+    (syntax-case rest ()
+      [() (map (λ (arg) (or (hash-ref current (car arg)) (cdr arg))) formals)]
+      [(kw . rest)
+       (not (keyword? (syntax-e (syntax kw))))
+       (raise-syntax-error #f "expected a keyword" source (syntax kw))]
+      [(kw arg . rest)
+       (keyword? (syntax-e (syntax arg)))
+       (raise-syntax-error #f "expected an argument expression" source (syntax arg))]
+      [(kw arg . rest)
+       (let ([none (gensym)])
+         (eq? none (hash-ref current (syntax-e (syntax kw)) none)))
+       (raise-syntax-error #f "invalid keyword" source (syntax kw))]
+      [(kw arg . rest)
+       (hash-ref current (syntax-e (syntax kw)))
+       (raise-syntax-error #f "repeated keyword" source (syntax kw))]
+      [(kw)
+       (raise-syntax-error #f "missing argument expression after keyword" source (syntax kw))]
+      [(kw arg . rest)
+       (loop (hash-set current (syntax-e (syntax kw)) (syntax arg))
+             (syntax rest))]
+      [else (raise-syntax-error #f "bad keyword argument syntax" source rest)])))
+
+(provide parse-kw-args)
\ No newline at end of file
diff --git a/collects/redex/private/rg-test.ss b/collects/redex/private/rg-test.ss
index 352b850ca1..103dec9f7c 100644
--- a/collects/redex/private/rg-test.ss
+++ b/collects/redex/private/rg-test.ss
@@ -5,6 +5,7 @@
          "matcher.ss"
          "term.ss"
          "rg.ss"
+         "keyword-macros.ss"
          "error.ss")
 
 (reset-count)
@@ -258,8 +259,8 @@
         null)
   (test (generate-term/decisions lang d 5 0 (decisions #:seq (list (λ (_) 2))))
         '(4 4 4 4 (4 4) (4 4)))
-  (test (raised-exn-msg exn:fail:redex? (generate-term lang e 5)) 
-        #rx"generate-term: unable to generate pattern e")
+  (test (raised-exn-msg exn:fail:redex? (generate-term lang e 5 #:retries 42)) 
+        #rx"generate-term: unable to generate pattern e in 42")
   (test (generate-term/decisions lang f 5 0 (decisions #:seq (list (λ (_) 0)))) null)
   (test (generate-term/decisions 
          lang ((0 ..._!_1) ... (1 ..._!_1) ...) 5 0
@@ -520,7 +521,7 @@
     ; followed by the choices that produce 'y on the first size 2 attempt.
     (decisions 
      #:nt (apply patterns 
-                 (append (build-list (* generation-retries proportion-at-size)
+                 (append (build-list (* default-retries proportion-at-size)
                                      (λ (_) first))
                          (list second second first)))))
    'e)
@@ -669,27 +670,17 @@
           #rx"x does not match n"))
   (test (raised-exn-msg
          exn:fail:redex?
-         (redex-check lang (side-condition any #f) #t #:attempts 1))
-        #rx"^redex-check: unable")
-  
-  (let ([stx-err (λ (stx)
-                   (with-handlers ([exn:fail:syntax? exn-message])
-                     (expand stx)
-                     'no-syntax-error))])
-    (parameterize ([current-namespace (make-base-namespace)])
-      (eval '(require "../reduction-semantics.ss"
-                      "rg.ss"))
-      (eval '(define-language empty))
-      (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 '(redex-check empty any #t #:attempts))
-            #rx"bad keyword syntax")
-      (test (stx-err '(redex-check empty any #t #:attempts 3 4))
-            #rx"bad keyword syntax")
-      (test (stx-err '(redex-check empty any #t #:source #:attempts))
-            #rx"bad keyword syntax"))))
+         (redex-check lang (side-condition any #f) #t #:retries 42 #:attempts 1))
+        #rx"^redex-check: unable .* in 42")
+  (test (raised-exn-msg
+         exn:fail:redex?
+         (redex-check lang any #t 
+                      #:source (reduction-relation 
+                                lang
+                                (--> (side-condition any #f) any))
+                      #:retries 42
+                      #:attempts 1))
+        #rx"^redex-check: unable .* in 42"))
 
 ;; check-metafunction-contract
 (let ()
@@ -744,8 +735,8 @@
   ;; Unable to generate domain
   (test (raised-exn-msg
          exn:fail:redex?
-         (check-metafunction-contract j #:attempts 1))
-        #rx"^check-metafunction-contract: unable"))
+         (check-metafunction-contract j #:attempts 1 #:retries 42))
+        #rx"^check-metafunction-contract: unable .* in 42"))
 
 ;; check-reduction-relation
 (let ()
@@ -827,8 +818,8 @@
         #rx"check-metafunction: expected")
   (test (raised-exn-msg
          exn:fail:redex?
-         (check-metafunction n (λ (_) #t)))
-        #rx"check-metafunction: unable"))
+         (check-metafunction n (λ (_) #t) #:retries 42))
+        #rx"check-metafunction: unable .* in 42"))
 
 ;; parse/unparse-pattern
 (let-syntax ([test-match (syntax-rules () [(_ p x) (test (match x [p #t] [_ #f]) #t)])])
diff --git a/collects/redex/private/rg.ss b/collects/redex/private/rg.ss
index 2244f7c137..0fa360b0d6 100644
--- a/collects/redex/private/rg.ss
+++ b/collects/redex/private/rg.ss
@@ -24,6 +24,7 @@ To do a better job of not generating programs with free variables,
          (for-syntax "rewrite-side-conditions.ss")
          (for-syntax "term-fn.ss")
          (for-syntax "reduction-semantics.ss")
+         (for-syntax "keyword-macros.ss")
          mrlib/tex-table)
 
 (define (allow-free-var? [random random]) (= 0 (random 30)))
@@ -133,7 +134,7 @@ To do a better job of not generating programs with free variables,
 (define real-threshold 1000)
 (define complex-threshold 2000)
 
-(define generation-retries 100)
+(define default-retries 100)
 (define retry-threshold (max chinese-chars-threshold complex-threshold))
 (define proportion-before-threshold 9/10)
 (define proportion-at-size 1/10)
@@ -179,7 +180,7 @@ To do a better job of not generating programs with free variables,
   (let ([lits (map symbol->string (compiled-lang-literals lang))])
     (make-rg-lang (parse-language lang) lits (unique-chars lits) (find-base-cases lang))))
 
-(define (generate lang decisions@ what)
+(define (generate lang decisions@ retries what)
   (define-values/invoke-unit decisions@
     (import) (export decisions^))
   
@@ -230,21 +231,21 @@ To do a better job of not generating programs with free variables,
     (let ([pre-threshold-incr 
            (ceiling
             (/ (- retry-threshold init-att)
-               (* proportion-before-threshold generation-retries)))]
+               (* proportion-before-threshold retries)))]
           [incr-size? 
            (λ (remain)
              (zero? 
               (modulo (sub1 remain) 
                       (ceiling (* proportion-at-size 
-                                  generation-retries)))))])
-      (let retry ([remaining generation-retries]
+                                  retries)))))])
+      (let retry ([remaining retries]
                   [size init-sz]
                   [attempt init-att])
         (if (zero? remaining)
             (redex-error what "unable to generate pattern ~s in ~a attempt~a" 
                          name 
-                         generation-retries
-                         (if (= generation-retries 1) "" "s"))
+                         retries
+                         (if (= retries 1) "" "s"))
             (let-values ([(term state) (gen size attempt)])
               (if (pred term (state-env state))
                   (values term state)
@@ -681,23 +682,25 @@ To do a better job of not generating programs with free variables,
   (unless (and (integer? x) (>= x 0))
     (raise-type-error name "natural number" x)))
 
-(define-for-syntax (term-generator lang pat decisions@ what)
+(define-for-syntax (term-generator lang pat decisions@ retries what)
   (with-syntax ([pattern 
                  (rewrite-side-conditions/check-errs 
                   (language-id-nts lang what)
-                  what #t pat)]
-                [lang lang]
-                [decisions@ decisions@]
-                [what what])
-    (syntax ((generate lang decisions@ 'what) `pattern))))
+                  what #t pat)])
+    #`((generate #,lang #,decisions@ #,retries '#,what) `pattern)))
 
 (define-syntax (generate-term stx)
   (syntax-case stx ()
-    [(_ lang pat size #:attempt attempt)
-     (with-syntax ([generate (term-generator #'lang #'pat #'(generation-decisions) 'generate-term)])
-       (syntax/loc stx
-         (let-values ([(term _) (generate size attempt)])
-           term)))]
+    [(_ lang pat size . kw-args)
+     (with-syntax ([(attempt retries)
+                    (parse-kw-args `((#:attempt . 1)
+                                     (#:retries . ,#'default-retries))
+                                   (syntax kw-args)
+                                   stx)])
+       (with-syntax ([generate (term-generator #'lang #'pat #'(generation-decisions) #'retries 'generate-term)])
+         (syntax/loc stx
+           (let-values ([(term _) (generate size attempt)])
+             term))))]
     [(_ lang pat size)
      (syntax/loc stx (generate-term lang pat size #:attempt 1))]))
 
@@ -707,29 +710,26 @@ To do a better job of not generating programs with free variables,
      (let-values ([(names names/ellipses) 
                    (extract-names (language-id-nts #'lang 'redex-check)
                                   'redex-check #t #'pat)]
-                  [(attempts-stx source-stx)
-                   (let loop ([args (syntax kw-args)]
-                              [attempts #f]
-                              [source #f])
-                     (syntax-case args ()
-                       [() (values attempts source)]
-                       [(#:attempts a . rest)
-                        (not (or attempts (keyword? (syntax-e #'a))))
-                        (loop #'rest #'a source)]
-                       [(#:source s . rest)
-                        (not (or source (keyword? (syntax-e #'s))))
-                        (loop #'rest attempts #'s)]
-                       [else (raise-syntax-error #f "bad keyword syntax" stx args)]))])
+                  [(attempts-stx source-stx retries-stx)
+                   (apply values
+                          (parse-kw-args `((#:attempts . ,#'default-check-attempts)
+                                           (#:source . #f)
+                                           (#:retries . ,#'default-retries))
+                                         (syntax kw-args)
+                                         stx))])
        (with-syntax ([(name ...) names]
                      [(name/ellipses ...) names/ellipses]
-                     [attempts (or attempts-stx #'default-check-attempts)])
+                     [attempts attempts-stx]
+                     [retries retries-stx])
          (with-syntax ([property (syntax
                                   (λ (_ bindings)
                                     (term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
                                               property)))])
            (quasisyntax/loc stx
-             (let ([att attempts])
+             (let ([att attempts]
+                   [ret retries])
                (assert-nat 'redex-check att)
+               (assert-nat 'redex-check ret)
                (unsyntax
                 (if source-stx
                     #`(let-values
@@ -748,12 +748,12 @@ To do a better job of not generating programs with free variables,
                                           (reduction-relation-srcs r)
                                           (reduction-relation-lang r)))])])
                         (check-property-many 
-                         lang pats srcs property random-decisions@ (max 1 (floor (/ att (length pats))))
+                         lang pats srcs property random-decisions@ (max 1 (floor (/ att (length pats)))) ret
                          'redex-check
                          (test-match lang pat)
                          (λ (generated) (redex-error 'redex-check "~s does not match ~s" generated 'pat))))
                     #`(check-property
-                       #,(term-generator #'lang #'pat #'random-decisions@ 'redex-check)
+                       #,(term-generator #'lang #'pat #'random-decisions@ #'ret 'redex-check)
                        property att)))
                (void))))))]))
 
@@ -789,12 +789,14 @@ To do a better job of not generating programs with free variables,
 
 (define-syntax (check-metafunction-contract stx)
   (syntax-case stx ()
-    [(_ name)
-     (syntax/loc stx 
-       (check-metafunction-contract name #:attempts default-check-attempts))]
-    [(_ name #:attempts attempts)
+    [(_ name . kw-args)
      (identifier? #'name)
-     (with-syntax ([m (metafunc/err #'name stx)])
+     (with-syntax ([m (metafunc/err #'name stx)]
+                   [(attempts retries)
+                    (parse-kw-args `((#:attempts . ,#'default-check-attempts)
+                                     (#:retries . ,#'default-retries))
+                                   (syntax kw-args)
+                                   stx)])
        (syntax/loc stx 
         (let ([lang (metafunc-proc-lang m)]
               [dom (metafunc-proc-dom-pat m)]
@@ -802,7 +804,7 @@ To do a better job of not generating programs with free variables,
               [att attempts])
           (assert-nat 'check-metafunction-contract att)
           (check-property 
-           ((generate lang decisions@ 'check-metafunction-contract)
+           ((generate lang decisions@ retries 'check-metafunction-contract)
             (if dom dom '(any (... ...))))
            (λ (t _) 
              (with-handlers ([exn:fail:redex? (λ (_) #f)])
@@ -810,8 +812,8 @@ To do a better job of not generating programs with free variables,
            att)
           (void))))]))
 
-(define (check-property-many lang pats srcs prop decisions@ attempts what [match #f] [match-fail #f])
-  (let ([lang-gen (generate lang decisions@ what)])
+(define (check-property-many lang pats srcs prop decisions@ attempts retries what [match #f] [match-fail #f])
+  (let ([lang-gen (generate lang decisions@ retries what)])
     (for/and ([pat pats] [src srcs])
       (check-property
        (lang-gen pat)
@@ -830,10 +832,16 @@ To do a better job of not generating programs with free variables,
   (syntax-case stx ()
     [(_ name property)
      (syntax/loc stx (check-metafunction name property #:attempts default-check-attempts))]
-    [(_ name property #:attempts attempts)
-     (with-syntax ([m (metafunc/err #'name stx)])
+    [(_ name property . kw-args)
+     (with-syntax ([m (metafunc/err #'name stx)]
+                   [(attempts retries)
+                    (parse-kw-args `((#:attempts . , #'default-check-attempts)
+                                     (#:retries . ,#'default-retries))
+                                   (syntax kw-args)
+                                   stx)])
        (syntax/loc stx
-         (let ([att attempts])
+         (let ([att attempts]
+               [ret retries])
            (assert-nat 'check-metafunction att)
            (check-property-many 
             (metafunc-proc-lang m)
@@ -842,6 +850,7 @@ To do a better job of not generating programs with free variables,
             (λ (term _) (property term))
             (generation-decisions)
             att
+            ret
             'check-metafunction))))]))
 
 (define (reduction-relation-srcs r)
@@ -851,7 +860,8 @@ To do a better job of not generating programs with free variables,
 (define (check-reduction-relation 
          relation property 
          #:decisions [decisions@ random-decisions@]
-         #:attempts [attempts default-check-attempts])
+         #:attempts [attempts default-check-attempts]
+         #:retries [retries default-retries])
   (check-property-many
    (reduction-relation-lang relation)
    (map rewrite-proc-lhs (reduction-relation-make-procs relation))
@@ -859,6 +869,7 @@ To do a better job of not generating programs with free variables,
    (λ (term _) (property term))
    decisions@
    attempts
+   retries
    'check-reduction-relation))
 
 (define-signature decisions^
@@ -891,7 +902,7 @@ To do a better job of not generating programs with free variables,
          pick-number parse-language check-reduction-relation 
          preferred-production-threshold check-metafunction
          generation-decisions pick-preferred-productions
-         generation-retries proportion-at-size retry-threshold 
+         default-retries proportion-at-size retry-threshold 
          proportion-before-threshold post-threshold-incr)
 
 (provide/contract
diff --git a/collects/redex/private/run-tests.ss b/collects/redex/private/run-tests.ss
index 68c134e5e6..10dc8f5382 100644
--- a/collects/redex/private/run-tests.ss
+++ b/collects/redex/private/run-tests.ss
@@ -9,6 +9,7 @@
     "tl-test.ss" 
     "term-test.ss" 
     "rg-test.ss" 
+    "keyword-macros-test.ss"
     "core-layout-test.ss" 
     "bitmap-test.ss" 
     "pict-test.ss"))
diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl
index 022696be4a..0f51e935f1 100644
--- a/collects/redex/redex.scrbl
+++ b/collects/redex/redex.scrbl
@@ -1029,10 +1029,12 @@ an association list mapping names to application counts.}
            (apply-reduction-relation* equals (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])]{
+@defform/subs[(generate-term language #, @|ttpattern| size-exp kw-args ...)
+              ([kw-args (code:line #:attempts attempts-expr)
+                        (code:line #:retries retries-expr)])
+              #:contracts ([size-expr natural-number/c]
+                           [attempt-num-expr natural-number/c]
+                           [retries-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
@@ -1041,16 +1043,28 @@ 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]).}
+decisions made during generation. For example, the expected length of 
+@pattech[pattern-sequence]s increases with @scheme[attempt-num-expr].
+
+The random generation process does not actively consider the constraints
+imposed by @pattech[side-condition] or @tt{_!_} @|pattern|s when 
+constructing a term; instead, it tests the satisfaction of
+such constraints after it freely generates the relevant portion of the 
+sub-term---regenerating the sub-term if necessary. The optional keyword 
+argument @scheme[retries-expr] (default @scheme[100]) bounds the number of times that 
+@scheme[generate-term] retries the generation of any sub-term. If 
+@scheme[generate-term] is unable to produce a satisfying term after 
+@scheme[retries-expr] attempts, it raises an error}
 
 @defform/subs[(redex-check language #, @|ttpattern| property-expr kw-arg ...)
               ([kw-arg (code:line #:attempts attempts-expr)
                        (code:line #:source metafunction)
-                       (code:line #:source relation-expr)])
+                       (code:line #:source relation-expr)
+                       (code:line #:retries retries-expr)])
               #:contracts ([property-expr any/c]
                            [attempts-expr natural-number/c]
-                           [relation-expr reduction-relation?])]{
+                           [relation-expr reduction-relation?]
+                           [retries-expr natural-number/c])]{
 Searches for a counterexample to @scheme[property-expr], interpreted
 as a predicate universally quantified over its free
 @pattech[term]-variables. @scheme[redex-check] chooses substitutions for 
@@ -1058,7 +1072,7 @@ 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[redex-check] generates at most @scheme[attempts-expr] (default @scheme[100])
+@scheme[redex-check] generates at most @scheme[attempts-expr] (default @scheme[1000])
 random terms in its search. The size and complexity of terms it generates
 gradually increases with each failed attempt.
 
@@ -1110,7 +1124,8 @@ term that does not match @scheme[pattern].}
 @defproc[(check-reduction-relation 
           [relation reduction-relation?]
           [property (-> any/c any/c)]
-          [#:attempts attempts natural-number/c 100])
+          [#:attempts attempts natural-number/c 1000]
+          [#:retries retries natural-number/c])
          void?]{
 Tests @scheme[relation] as follows: for each case of @scheme[relation],
 @scheme[check-reduction-relation] generates @scheme[attempts] random
@@ -1123,10 +1138,12 @@ This function provides a more convenient notation for
                           #:source relation)]
 when @scheme[relation] is a relation on @scheme[L] and has @scheme[n] rules.}
 
-@defform*[[(check-metafunction metafunction property)
-           (check-metafunction metafunction property #:attempts attempts)]
-          #:contracts ([property (-> any/c any/c)]
-                       [attempts natural-number/c])]{
+@defform/subs[(check-metafunction metafunction property kw-args ...)
+              ([kw-arg (code:line #:attempts attempts-expr)
+                       (code:line #:retries retries-expr)])
+              #:contracts ([property (-> any/c any/c)]
+                           [attempts-expr natural-number/c]
+                           [retries-expr natural-number/c])]{
 Like @scheme[check-reduction-relation] but for metafunctions.}
 
 @deftech{Debugging PLT Redex Programs}
diff --git a/collects/redex/reduction-semantics.ss b/collects/redex/reduction-semantics.ss
index d4e0271841..641b7cc567 100644
--- a/collects/redex/reduction-semantics.ss
+++ b/collects/redex/reduction-semantics.ss
@@ -66,7 +66,8 @@
  [variable-not-in (any/c symbol? . -> . symbol?)]
  [variables-not-in (any/c (listof symbol?) . -> . (listof symbol?))]
  [check-reduction-relation (->* (reduction-relation? (-> any/c any/c))
-                                (#:attempts natural-number/c)
+                                (#:attempts natural-number/c
+                                 #:retries natural-number/c)
                                 (one-of/c #t (void)))]
  [relation-coverage (parameter/c (or/c false/c coverage?))]
  [make-coverage (-> reduction-relation? coverage?)]