diff --git a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
index bce3e13868..4e9efdebe2 100644
--- a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
+++ b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
@@ -1106,9 +1106,12 @@ reduce it further).
                ...)
              ([metafunction-contract (code:line) 
                                      (code:line id : @#,ttpattern-sequence ... -> range
-                                                maybe-pre-condition)]
+                                                maybe-pre-condition
+                                                maybe-post-condition)]
               [maybe-pre-condition (code:line #:pre @#,tttterm)
                                    (code:line)]
+              [maybe-post-condition (code:line #:post @#,tttterm)
+                                    (code:line)]
               [range @#,ttpattern
                      (code:line @#,ttpattern or range)
                      (code:line @#,ttpattern ∨ range)
@@ -1133,7 +1136,10 @@ If present, the term inside the @racket[maybe-pre-condition] is evaluated
 after a successful match to the input pattern in the contract (with
 any variables from the input contract bound). If
 it returns @racket[#f], then the input contract is considered to not
-have matched and an error is also raised.
+have matched and an error is also raised. When a metafunction
+returns, the expression in the @racket[maybe-post-condition] is
+evaluated (if present), with any variables from the input or output 
+contract bound.
 
 The @racket[side-condition], @racket[hidden-side-condition],
 @racket[where], and @racket[where/hidden] clauses behave as
@@ -1213,6 +1219,8 @@ ensures that there is a unique match for that case. Without
 it, @racket[(term (- (x x) x))] would lead to an ambiguous
 match.
 
+@history[#:changed "1.4" @list{Added @racket[#:post] conditions.}]
+
 }
 
 @defform[(define-metafunction/extension f language 
diff --git a/pkgs/redex-pkgs/redex-lib/info.rkt b/pkgs/redex-pkgs/redex-lib/info.rkt
index 4fb1c7e5eb..c70f0fde7b 100644
--- a/pkgs/redex-pkgs/redex-lib/info.rkt
+++ b/pkgs/redex-pkgs/redex-lib/info.rkt
@@ -18,4 +18,4 @@
 
 (define pkg-authors '(robby bfetscher))
 
-(define version "1.3")
+(define version "1.4")
diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt
index e970edb787..8267794661 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt
@@ -407,7 +407,7 @@
      (begin
        (unless (identifier? #'lang)
          (raise-syntax-error #f "expected an identifier in the language position" stx #'lang))
-       (define-values (contract-name dom-ctcs pre-condition codom-contracts pats)
+       (define-values (contract-name dom-ctcs pre-condition codom-contracts post-condition pats)
          (split-out-contract stx (syntax-e #'def-form-id) #'body #t))
        (with-syntax* ([((name trms ...) rest ...) (car pats)]
                       [(mode-stx ...) #`(#:mode (name I))]
@@ -425,7 +425,7 @@
   ;; initial test determines if a contract is specified or not
   (cond
     [(pair? (syntax-e (car (syntax->list rest))))
-     (values #f #f #f (list #'any) (check-clauses stx syn-error-name (syntax->list rest) relation?))]
+     (values #f #f #f (list #'any) #f (check-clauses stx syn-error-name (syntax->list rest) relation?))]
     [else
      (syntax-case rest ()
        [(id separator more ...)
@@ -438,7 +438,7 @@
                (raise-syntax-error syn-error-name 
                                    "expected clause definitions to follow domain contract"
                                    stx))
-             (values #'id contract #f (list #'any) (check-clauses stx syn-error-name clauses #t)))]
+             (values #'id contract #f (list #'any) #f (check-clauses stx syn-error-name clauses #t)))]
           [else
            (unless (eq? ': (syntax-e #'separator))
              (raise-syntax-error syn-error-name "expected a colon to follow the meta-function's name" stx #'separator))
@@ -448,18 +448,19 @@
                [(null? more)
                 (raise-syntax-error syn-error-name "expected an ->" stx)]
                [(eq? (syntax-e (car more)) '->)
-                (define-values (raw-clauses rev-codomains pre-condition)
+                (define-values (raw-clauses rev-codomains pre-condition post-condition)
                   (let loop ([prev (car more)]
                              [more (cdr more)]
                              [codomains '()])
                     (cond
                       [(null? more)
-                       (raise-syntax-error syn-error-name "expected a range contract to follow" stx prev)]
+                       (raise-syntax-error syn-error-name
+                                           "expected a range contract to follow" stx prev)]
                       [else
                        (define after-this-one (cdr more))
                        (cond
                          [(null? after-this-one)
-                          (values null (cons (car more) codomains) #t)]
+                          (values null (cons (car more) codomains) #t #t)]
                          [else
                           (define kwd (cadr more))
                           (cond
@@ -467,17 +468,41 @@
                              (loop kwd 
                                    (cddr more)
                                    (cons (car more) codomains))]
-                            [(and (not relation?) (equal? (syntax-e kwd) '#:pre))
+                            [(and (not relation?) 
+                                  (or (equal? (syntax-e kwd) '#:pre)
+                                      (equal? (syntax-e kwd) '#:post)))
                              (when (null? (cddr more)) 
-                               (raise-syntax-error 'define-metafunction 
-                                                   "expected an expression to follow #:pre keyword"
-                                                   kwd))
-                             (values (cdddr more)
+                               (raise-syntax-error 
+                                'define-metafunction 
+                                (format "expected an expression to follow ~a keyword"
+                                        (syntax-e kwd))
+                                kwd))
+                             (define pre #t)
+                             (define post #t)
+                             (define remainder (cdddr more))
+                             (cond
+                               [(equal? (syntax-e kwd) '#:pre)
+                                (set! pre (caddr more))
+                                (define without-pre (cdddr more))
+                                (when (and (pair? without-pre)
+                                           (equal? (syntax-e (car without-pre)) '#:post))
+                                  (when (null? (cddr without-pre)) 
+                                    (raise-syntax-error 
+                                     'define-metafunction 
+                                     "expected an expression to follow #:post keyword"
+                                     kwd))
+                                  (set! remainder (cddr without-pre))
+                                  (set! post (cadr without-pre)))]
+                               [(equal? (syntax-e kwd) '#:post)
+                                (set! post (caddr more))])
+                             (values remainder
                                      (cons (car more) codomains)
-                                     (caddr more))]
+                                     pre 
+                                     post)]
                             [else
                              (values (cdr more)
                                      (cons (car more) codomains)
+                                     #t
                                      #t)])])])))
                 (let ([doms (reverse dom-pats)]
                       [clauses (check-clauses stx syn-error-name raw-clauses relation?)])
@@ -485,6 +510,7 @@
                           doms
                           (if relation? #f pre-condition)
                           (reverse rev-codomains)
+                          (if relation? #f post-condition)
                           clauses))]
                [else
                 (loop (cdr more) (cons (car more) dom-pats))]))])]
diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt
index 67b754d656..598e6721d5 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt
@@ -1186,8 +1186,10 @@
          (syntax-local-value 
           prev-metafunction
           (λ ()
-            (raise-syntax-error syn-error-name "expected a previously defined metafunction" orig-stx prev-metafunction))))
-       (let*-values ([(contract-name dom-ctcs pre-condition codom-contracts pats)
+            (raise-syntax-error 
+             syn-error-name 
+             "expected a previously defined metafunction" orig-stx prev-metafunction))))
+       (let*-values ([(contract-name dom-ctcs pre-condition codom-contracts post-condition pats)
                       (split-out-contract orig-stx syn-error-name #'rest #f)]
                      [(name _) (defined-name (list contract-name) pats orig-stx)])
          (when (and prev-metafunction (eq? (syntax-e #'name) (syntax-e prev-metafunction)))
@@ -1208,8 +1210,13 @@
                                                               name
                                                               name-predicate
                                                               #,dom-ctcs
-                                                              #,pre-condition
+                                                              #,(if pre-condition
+                                                                    (list pre-condition)
+                                                                    #f)
                                                               #,codom-contracts
+                                                              #,(if post-condition
+                                                                    (list post-condition)
+                                                                    #f)
                                                               #,pats
                                                               #,syn-error-name))
                                      (term-define-fn name name2))])
@@ -1252,16 +1259,26 @@
 
 (define-syntax (generate-metafunction stx)
   (syntax-case stx ()
-    [(_ orig-stx lang prev-metafunction 
+    [(_ orig-stx lang prev-metafunction-stx
         name name-predicate
-        dom-ctcs pre-condition
-        codom-contracts pats syn-error-name)
-     (let ([prev-metafunction (and (syntax-e #'prev-metafunction) #'prev-metafunction)]
-           [dom-ctcs (syntax-e #'dom-ctcs)]
-           [pre-condition (syntax-e #'pre-condition)]
-           [codom-contracts (syntax-e #'codom-contracts)]
-           [pats (syntax-e #'pats)]
-           [syn-error-name (syntax-e #'syn-error-name)])
+        dom-ctcs-stx pre-condition-stx
+        codom-contracts-stx post-condition-stx
+        pats-stx syn-error-name)
+     (let ()
+       (define (condition-or-false s)
+         (define info (syntax-e s))
+         (cond
+           [info
+            (unless (pair? info) (error 'condition-or-false "~s" s))
+            (car info)]
+           [else #f]))
+       (define prev-metafunction (and (syntax-e #'prev-metafunction-stx) #'prev-metafunction-stx))
+       (define dom-ctcs (syntax-e #'dom-ctcs-stx))
+       (define pre-condition (condition-or-false #'pre-condition-stx))
+       (define codom-contracts (syntax-e #'codom-contracts-stx))
+       (define post-condition (condition-or-false #'post-condition-stx))
+       (define pats (syntax-e #'pats-stx))
+       (define syn-error-name (syntax-e #'syn-error-name))
        (define lang-nts
          (definition-nts #'lang #'orig-stx syn-error-name))
        (with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats]
@@ -1322,21 +1339,29 @@
                                                (syntax-line lhs)
                                                (syntax-column lhs)))
                                      pats)]
-                               [(dom-syncheck-expr dom-side-conditions-rewritten dom-names dom-names/ellipses)
+                               [(dom-syncheck-expr dom-side-conditions-rewritten 
+                                                   (dom-names ...)
+                                                   dom-names/ellipses)
                                 (if dom-ctcs
                                     (rewrite-side-conditions/check-errs
                                      #'lang
                                      syn-error-name
                                      #f
-                                     #`(side-condition #,dom-ctcs (term #,pre-condition)))
+                                     dom-ctcs)
                                     #'((void) any () ()))]
-                               [((codom-syncheck-expr codom-side-conditions-rewritten codom-names codom-names/ellipses) ...)
+                               [((codom-syncheck-expr 
+                                  codom-side-conditions-rewritten
+                                  codom-names 
+                                  codom-names/ellipses) ...)
                                 (map (λ (codom-contract)
                                        (rewrite-side-conditions/check-errs
                                         #'lang
                                         syn-error-name
                                         #f
-                                        codom-contract))
+                                        (if post-condition
+                                            #`(side-condition (#,dom-ctcs #,codom-contract)
+                                                              (term #,post-condition))
+                                            codom-contract)))
                                      codom-contracts)]
                                [(rhs-fns ...)
                                 (map (λ (names names/ellipses rhs/where)
@@ -1415,7 +1440,13 @@
                                        (λ ()
                                          (add-mf-dqs #,(check-pats #'(list gen-clause ...)))))])))
                             #,(if dom-ctcs #'dsc #f)
+                            (λ (bindings) 
+                              #,(bind-pattern-names 'define-metafunction
+                                                    #'dom-names/ellipses
+                                                    #'((lookup-binding bindings 'dom-names) ...)
+                                                    #`(term #,pre-condition)))
                             `(codom-side-conditions-rewritten ...)
+                            #,(and post-condition #t)
                             'name))))
                     'disappeared-use
                     (map syntax-local-introduce 
@@ -1575,7 +1606,11 @@
    (syntax->list extras)))
 
 
-(define (build-metafunction lang cases parent-cases wrap dom-contract-pat codom-contract-pats name)
+(define (build-metafunction lang cases parent-cases 
+                            wrap
+                            dom-contract-pat pre-condition
+                            codom-contract-pats post-condition?
+                            name)
   (let* ([dom-compiled-pattern (and dom-contract-pat (compile-pattern lang dom-contract-pat #f))]
          [codom-compiled-patterns (map (λ (codom-contract-pat) (compile-pattern lang codom-contract-pat #f))
                                        codom-contract-pats)]
@@ -1610,8 +1645,17 @@
                   (let ([cache-ref (hash-ref cache exp not-in-cache)])
                     (cond
                       [(or (not (caching-enabled?)) (eq? cache-ref not-in-cache))
+                       (define dom-match-result 
+                         (if dom-compiled-pattern
+                             (match-pattern dom-compiled-pattern exp)
+                             '()))
                        (when dom-compiled-pattern
-                         (unless (match-pattern dom-compiled-pattern exp)
+                         (unless dom-match-result
+                           (redex-error name
+                                        "~s is not in my domain"
+                                        `(,name ,@exp)))
+                         (unless (for/and ([mtch (in-list dom-match-result)])
+                                   (pre-condition (mtch-bindings mtch)))
                            (redex-error name
                                         "~s is not in my domain"
                                         `(,name ,@exp))))
@@ -1623,45 +1667,49 @@
                            [(null? ids) 
                             (redex-error name "no clauses matched for ~s" `(,name . ,exp))]
                            [else
-                            (let ([pattern (car lhss)]
-                                  [rhs (car rhss)]
-                                  [id (car ids)]
-                                  [continue (λ () (loop (cdr ids) (cdr lhss) (cdr rhss) (+ num 1)))])
-                              (let ([mtchs (match-pattern pattern exp)])
-                                (cond
-                                  [(not mtchs) (continue)]
-                                  [else
-                                   (let ([anss (apply append
-                                                      (filter values
-                                                              (map (λ (mtch) (rhs traced-metafunc (mtch-bindings mtch)))
-                                                                   mtchs)))]
-                                         [ht (make-hash)])
-                                     (for-each (λ (ans) (hash-set! ht ans #t)) anss)
-                                     (cond
-                                       [(null? anss)
-                                        (continue)]
-                                       [(not (= 1 (hash-count ht)))
-                                        (redex-error name "~a matched ~s ~a returned different results" 
-                                                     (if (< num 0)
-                                                         "a clause from an extended metafunction"
-                                                         (format "clause #~a (counting from 0)" num))
-                                                     `(,name ,@exp)
-                                                     (if (= 1 (length mtchs))
-                                                         "but"
-                                                         (format "~a different ways and "
-                                                                 (length mtchs))))]
-                                       [else
-                                        (let ([ans (car anss)])
-                                          (unless (ormap (λ (codom-compiled-pattern)
-                                                           (match-pattern codom-compiled-pattern ans))
-                                                         codom-compiled-patterns)
-                                            (redex-error name
-                                                         "codomain test failed for ~s, call was ~s"
-                                                         ans 
-                                                         `(,name ,@exp)))
-                                          (cache-result exp ans id)
-                                          (log-coverage id)
-                                          ans)]))])))]))]
+                            (define pattern (car lhss))
+                            (define rhs (car rhss))
+                            (define id (car ids))
+                            (define (continue) (loop (cdr ids) (cdr lhss) (cdr rhss) (+ num 1)))
+                            (define mtchs (match-pattern pattern exp))
+                            (cond
+                              [(not mtchs) (continue)]
+                              [else
+                               (define anss
+                                 (apply append
+                                        (filter values
+                                                (map (λ (mtch) (rhs traced-metafunc (mtch-bindings mtch)))
+                                                     mtchs))))
+                               (define ht (make-hash))
+                               (for-each (λ (ans) (hash-set! ht ans #t)) anss)
+                               (cond
+                                 [(null? anss)
+                                  (continue)]
+                                 [(not (= 1 (hash-count ht)))
+                                  (redex-error name "~a matched ~s ~a returned different results" 
+                                               (if (< num 0)
+                                                   "a clause from an extended metafunction"
+                                                   (format "clause #~a (counting from 0)" num))
+                                               `(,name ,@exp)
+                                               (if (= 1 (length mtchs))
+                                                   "but"
+                                                   (format "~a different ways and "
+                                                           (length mtchs))))]
+                                 [else
+                                  (define ans (car anss))
+                                  (unless (for/or ([codom-compiled-pattern 
+                                                    (in-list codom-compiled-patterns)])
+                                            (match-pattern codom-compiled-pattern 
+                                                           (if post-condition?
+                                                               (list exp ans)
+                                                               ans)))
+                                    (redex-error name
+                                                 "codomain test failed for ~s, call was ~s"
+                                                 ans 
+                                                 `(,name ,@exp)))
+                                  (cache-result exp ans id)
+                                  (log-coverage id)
+                                  ans])])]))]
                       [else 
                        (log-coverage (cdr cache-ref))
                        (car cache-ref)])))]
diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt
index 399e615b0d..79351080a2 100644
--- a/pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt
+++ b/pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt
@@ -1197,7 +1197,37 @@
     (test (term (m 1 1)) 1)
     (test (with-handlers ((exn:fail:redex? exn-message))
             (term (m 1 2)))
-          #rx"is not in my domain"))
+          #rx"is not in my domain")
+    
+    (define-metafunction empty-language
+      is-nat : any -> boolean
+      [(is-nat natural) #t]
+      [(is-nat any) #f])
+
+    (define-metafunction empty-language
+      post-only : any_1 -> any_2
+      #:post (same any_1 any_2)
+      [(post-only any) 1])
+
+    (test (term (post-only 1)) 1)
+    (test (with-handlers ([exn:fail:redex? exn-message])
+            (term (post-only 2)))
+          #rx"codomain")
+
+    (define-metafunction empty-language
+      pre-and-post : any_1 -> any_2
+      #:pre (is-nat any_1)
+      #:post (same any_1 any_2)
+      [(pre-and-post any) 1])
+
+    (test (term (pre-and-post 1)) 1)
+    (test (with-handlers ([exn:fail:redex? exn-message])
+            (term (pre-and-post x)))
+          #rx"is not in my domain")
+    (test (with-handlers ([exn:fail:redex? exn-message])
+            (term (pre-and-post 2)))
+          #rx"codomain")
+    )
   
   (let ()
     (define-language L