diff --git a/collects/meta/props b/collects/meta/props
index 64affe8755..85593e675a 100755
--- a/collects/meta/props
+++ b/collects/meta/props
@@ -1201,6 +1201,8 @@ path/s is either such a string or a list of them.
 "collects/redex/examples/r6rs/r6rs-tests.rkt" drdr:command-line (mzc *)
 "collects/redex/examples/r6rs/racket-vs-redex.rkt" drdr:timeout 180
 "collects/redex/examples/r6rs/show-examples.rkt" drdr:command-line (mzc *)
+"collects/redex/examples/racket-machine/examples.rkt" drdr:command-line (gracket * "--no-pop-ups")
+"collects/redex/examples/racket-machine/randomized-tests.rkt" drdr:command-line (racket "-t" * "-m") drdr:timeout 300
 "collects/redex/examples/racket-machine/reduction-test.rkt" drdr:command-line (mzc *)
 "collects/redex/examples/racket-machine/verification-test.rkt" drdr:command-line (mzc *)
 "collects/redex/examples/semaphores.rkt" drdr:command-line (mzc *)
diff --git a/collects/redex/examples/racket-machine/examples.rkt b/collects/redex/examples/racket-machine/examples.rkt
new file mode 100644
index 0000000000..54ee5ecf79
--- /dev/null
+++ b/collects/redex/examples/racket-machine/examples.rkt
@@ -0,0 +1,93 @@
+#lang racket
+
+(require (only-in "reduction.rkt" -> load)
+         (only-in "verification.rkt" bytecode-ok?)
+         (only-in "model-impl.rkt" compile-bytecode impl->model)
+         redex
+         rackunit)
+
+;; eval: e ((x e) ...) -> (listof result)
+;; Evaluates a bytecode program.
+;; result ::= v | closure | stuck
+(define (eval expr [cycles '()])
+  (map (match-lambda
+         [`((clos ,_) ,_ ,_ ,_ ()) (closure)]
+         [`(,v ,_ ,_ ,_ ()) v]
+         [`(,_ ,_ ,_ ,_ (,_ ,_ ...)) (stuck)]
+         ['error (error)])
+       (let ([seen (make-hash)]
+             [finals '()])
+         (let loop ([state (program expr cycles)])
+           (unless (hash-ref seen state #f)
+             (hash-set! seen state #t)
+             (let ([succs (apply-reduction-relation -> state)])
+               (if (null? succs)
+                   (set! finals (cons state finals))
+                   (map loop succs)))))
+         finals)))
+
+(define (program expr cycles)
+  (term (load ,expr ,cycles)))
+
+(struct closure () #:transparent)
+(struct stuck () #:transparent)
+(struct error () #:transparent)
+
+(check-equal? (eval '(application (proc-const (val) (loc 0)) 'y))
+              '('y))
+(check-equal? (eval '(application (indirect x) 'y) '((x (proc-const (val) (loc 0)))))
+              '('y))
+(check-equal? (eval '(proc-const (val) (loc 0)))
+              (list (closure)))
+(check-equal? (eval '(application (proc-const (val) (loc 0))))
+              (list (error)))
+(define bug-#3
+  '(let-one (proc-const (val) (loc 0)) 
+            (application 
+             (loc-noclr 1) 
+             (install-value 1 (proc-const (val) 'x) 
+                            'y))))
+(let ([sorted (λ (xs) (sort xs string<=? #:key (curry format "~s")))])
+  (check-pred (negate bytecode-ok?) bug-#3)
+  (check-equal? (sorted (eval bug-#3)) '('x 'y)))
+
+(define (trace expr [cycles '()])
+  (traces -> (program expr cycles)))
+(define (step expr [cycles '()])
+  (stepper -> (program expr cycles)))
+
+(when (let ([pop-ups? #t])
+        (command-line
+         #:once-any
+         ["--no-pop-ups"
+          "Avoid opening the `traces' and `stepper' windows"
+          (set! pop-ups? #f)])
+        pop-ups?)
+  (trace bug-#3)
+  (step bug-#3))
+
+;; racket->bytecode: syntax -> (e ((x e) ...))
+;; Compiles a Racket expression into bytecode.
+(define racket->bytecode
+  (compose impl->model compile-bytecode))
+
+(define a-racket-program
+  #'(let ([cons (λ (x y) (λ (s) (s x y)))]
+          [car (λ (p) (p (λ (x y) x)))]
+          [cdr (λ (p) (p (λ (x y) y)))]
+          [null #f]
+          [null? (λ (x) (if x #f #t))])
+      (letrec ([find (lambda (it? xs)
+                       (if (null? xs)
+                           #f
+                           (let ([x (car xs)])
+                             (if (it? x)
+                                 x
+                                 (find it? (cdr xs))))))])
+        (find (λ (x) x) (cons #f (cons #f (cons 1 (cons 2 null))))))))
+
+;; If this test fails, it's probably because the compiler has changed
+;; and no longer maps this program into the subset supported in the
+;; model. Try the version bundled with Redex (see the README).
+(match-let ([(cons expr cycles) (racket->bytecode a-racket-program)])
+  (check-equal? (eval expr cycles) '(1)))
\ No newline at end of file
diff --git a/collects/redex/examples/racket-machine/impl-eval.rkt b/collects/redex/examples/racket-machine/impl-eval.rkt
new file mode 100644
index 0000000000..5538ed9fd5
--- /dev/null
+++ b/collects/redex/examples/racket-machine/impl-eval.rkt
@@ -0,0 +1,51 @@
+#lang racket
+
+(require racket/serialize
+         racket/runtime-path
+         compiler/zo-marshal)
+
+(provide (all-defined-out))
+
+(serializable-struct impl-timeout ())
+(serializable-struct impl-rejected ())
+(serializable-struct impl-exception (value))
+(serializable-struct impl-answer (value))
+(serializable-struct impl-clos-val ())
+(serializable-struct impl-undefined-val ())
+
+(define (eval-impl expr timeout)
+  (let* ([p (zo-marshal expr)]
+         [c (make-channel)]
+         [t (thread
+             (λ ()
+               (parameterize ([read-accept-compiled #t])
+                 (channel-put c (with-handlers ([exn:fail? values])
+                                  (let ([val (eval (read (open-input-bytes p)))])
+                                    (impl-answer
+                                     (cond [(procedure? val) (impl-clos-val)]
+                                           [(eq? (letrec ([x x]) x) val) (impl-undefined-val)]
+                                           [else val]))))))))])
+    
+    (match (sync/timeout timeout c)
+      [(and (? exn:fail?) (exn (regexp #rx"ill-formed code") _))
+       (impl-rejected)]
+      [(exn msg _) (impl-exception msg)]
+      [#f (begin (kill-thread t) (impl-timeout))]
+      [x x])))
+
+(define-runtime-path impl-exec-path "impl-exec.rkt")
+
+(define (eval-impl-external expr timeout)
+  (let-values ([(in-in in-out) (make-pipe)]
+               [(out-in out-out) (make-pipe)])
+    (parameterize ([current-input-port in-in]
+                   [current-output-port out-out])
+      (write timeout in-out)
+      (write (serialize expr) in-out)
+      (if (system (format "racket -X ~a ~a"
+                          (find-executable-path 
+                           (find-system-path 'exec-file)
+                           (find-system-path 'collects-dir))
+                          impl-exec-path))
+          (deserialize (read out-in))
+          (error 'eval-impl-external "failed to evaluate ~a" expr)))))
diff --git a/collects/redex/examples/racket-machine/impl-exec.rkt b/collects/redex/examples/racket-machine/impl-exec.rkt
new file mode 100644
index 0000000000..006cd4d1fb
--- /dev/null
+++ b/collects/redex/examples/racket-machine/impl-exec.rkt
@@ -0,0 +1,9 @@
+#lang racket
+
+(require racket/serialize
+         "impl-eval.rkt")
+
+(define timeout (read))
+(define bytecode (deserialize (read)))
+
+(write (serialize (eval-impl bytecode timeout)))
diff --git a/collects/redex/examples/racket-machine/model-impl.rkt b/collects/redex/examples/racket-machine/model-impl.rkt
new file mode 100644
index 0000000000..0c74b52be2
--- /dev/null
+++ b/collects/redex/examples/racket-machine/model-impl.rkt
@@ -0,0 +1,211 @@
+#lang racket
+
+(require compiler/zo-parse
+         compiler/zo-marshal
+         "impl-eval.rkt")
+
+(provide (all-defined-out)
+         (all-from-out "impl-eval.rkt"))
+
+(define (compile-bytecode expr)
+  (let ([tmp (make-temporary-file)])
+    (call-with-output-file tmp #:exists 'truncate
+      (λ (p) 
+        (parameterize ([current-namespace (make-base-namespace)])
+          (write (compile expr) p))))
+    (begin0
+      (call-with-input-file tmp zo-parse)
+      (delete-file tmp))))
+
+(define (impl->model expr)
+  (define cycled (cycle-points expr))
+  (define text-addr (make-hasheq))
+  (define next-loc
+    (let ([suffix 0])
+      (λ ()
+        (set! suffix (add1 suffix))
+        (string->symbol (format "x~s" suffix)))))
+  (define text-seg '())
+  (cons 
+   (let recur ([e expr])
+     (match e
+       [(compilation-top _ _ e)
+        (recur e)]
+       [(localref #f n #f #t #f)
+        `(loc ,n)]
+       [(localref #f n #t _ #f)
+        `(loc-clr ,n)]
+       [(localref #f n #f #f #f)
+        `(loc-noclr ,n)]
+       [(localref #t n #f #t #f)
+        `(loc-box ,n)]
+       [(localref #t n #t _ #f)
+        `(loc-box-clr ,n)]
+       [(localref #t n #f #f #f)
+        `(loc-box-noclr ,n)]
+       [(let-one r b #f #f)
+        `(let-one ,(recur r) ,(recur b))]
+       [(let-void n #f b)
+        `(let-void ,n ,(recur b))]
+       [(let-void n #t b)
+        `(let-void-box ,n ,(recur b))]
+       [(install-value 1 n #f r b)
+        `(install-value ,n ,(recur r) ,(recur b))]
+       [(install-value 1 n #t r b)
+        `(install-value-box ,n ,(recur r) ,(recur b))]
+       [(boxenv n b)
+        `(boxenv ,n ,(recur b))]
+       [(application f as)
+        `(application ,(recur f) ,@(map recur as))]
+       [(seq es)
+        `(seq ,@(map recur es))]
+       [(branch c t e)
+        `(branch ,(recur c) ,(recur t) ,(recur e))]
+       [(let-rec rs b)
+        `(let-rec ,(map recur rs) ,(recur b))]
+       [(lam _ _ _ τs #f ns `(val/ref ...) _ b)
+        `(lam ,τs ,(vector->list ns) ,(recur b))]
+       [(closure l _)
+        (define (model-rep)
+          (match-let ([`(lam ,τs () ,b) (recur l)])
+            `(proc-const ,τs ,b)))
+        (if (hash-ref cycled e #f)
+            `(indirect ,(let ([x (hash-ref text-addr e #f)])
+                          (or x
+                              (let ([x (next-loc)])
+                                (hash-set! text-addr e x)
+                                (set! text-seg (cons (list x (model-rep)) text-seg))
+                                x))))
+            (model-rep))]
+       [(case-lam _ ls)
+        `(case-lam ,@(map recur ls))]
+       [(? void?) 'void]
+       [(? number?) e]
+       [(? boolean?) e]
+       [(? symbol?) `',e]
+       [_ (error 'impl->model "unrecognized form ~s" e)]))
+   text-seg))
+
+(define (cycle-points expr)
+  (define seen (make-hasheq))
+  (let recur ([e expr])
+    (when (zo? e) ; i.e., not a literal
+      (if (hash-ref seen e #f)
+          (unless (closure? e)
+            (error 'cycle-refs "illegal cycle through ~s" e))
+          (begin
+            (hash-set! seen e #t)
+            (match e
+              [(compilation-top _ _ e)
+               (recur e)]
+              [(localref _ _ _ _ _)
+               (void)]
+              [(let-one r b _ _)
+               (recur r)
+               (recur b)]
+              [(let-void _ _ b)
+               (recur b)]
+              [(install-value _ _ _ r b)
+               (recur r)
+               (recur b)]
+              [(boxenv _ b)
+               (recur b)]
+              [(application f as)
+               (recur f) 
+               (for-each recur as)]
+              [(seq es)
+               (for-each recur es)]
+              [(branch c t e)
+               (recur c)
+               (recur t)
+               (recur e)]
+              [(let-rec rs b)
+               (for-each recur rs) 
+               (recur b)]
+              [(lam _ _ _ _ _ _ _ _ b)
+               (recur b)]
+              [(closure l _)
+               (recur l)]
+              [(case-lam _ ls)
+               (for-each recur ls)]
+              [_ (void)])))))
+  seen)
+
+(define (model->impl expr [cycles '()])
+  (let ([cycle-places (make-immutable-hash
+                       (map (match-lambda
+                              [(cons x _) 
+                               (cons x (make-placeholder #f))])
+                            cycles))])
+    (letrec ([recur (λ (e)
+                      (match e
+                        [`(loc ,n) (cons (localref #f n #f #t #f) 0)]
+                        [`(loc-clr ,n) (cons (localref #f n #t #t #f) 0)]
+                        [`(loc-noclr ,n) (cons (localref #f n #f #f #f) 0)]
+                        [`(loc-box ,n) (cons (localref #t n #f #t #f) 0)]
+                        [`(loc-box-clr ,n) (cons (localref #t n #t #t #f) 0)]
+                        [`(loc-box-noclr ,n) (cons (localref #t n #f #f #f) 0)]
+                        [`(let-one ,r ,b)
+                         (match-let ([(cons rr dr) (recur r)]
+                                     [(cons rb db) (recur b)])
+                           (cons (let-one rr rb #f #f)
+                                 (add1 (max dr db))))]
+                        [`(,(and (or 'let-void 'let-void-box) i) ,n ,b)
+                         (match-let ([(cons rb db) (recur b)])
+                           (let ([b? (match i ['let-void #f] ['let-void-box #t])])
+                             (cons (let-void n b? rb) 
+                                   (+ n db))))]
+                        [`(,(and (or 'install-value 'install-value-box) i) ,n ,r ,b)
+                         (match-let ([(cons rr dr) (recur r)]
+                                     [(cons rb db) (recur b)])
+                           (let ([b? (match i ['install-value #f] ['install-value-box #t])])
+                             (cons (install-value 1 n b? rr rb)
+                                   (max dr db))))]
+                        [`(boxenv ,n ,e)
+                         (match-let ([(cons re de) (recur e)])
+                           (cons (boxenv n re) de))]
+                        [`(application ,f . ,as)
+                         (match-let ([`((,rf . ,df) (,ras . ,das) ...)
+                                      (map recur (cons f as))])
+                           (cons (application rf ras)
+                                 (+ (length as) (apply max df das))))]
+                        [`(seq ,e ,es ...)
+                         (match-let ([`((,re . ,de) (,res . ,des) ...)
+                                      (map recur (cons e es))])
+                           (cons (seq (cons re res))
+                                 (apply max de des)))]
+                        [`(branch ,c ,t ,f)
+                         (match-let ([(cons rc dc) (recur c)]
+                                     [(cons rt dt) (recur t)]
+                                     [(cons rf df) (recur f)])
+                           (cons (branch rc rt rf)
+                                 (max dc dt df)))]
+                        [`(let-rec (,rs ...) ,b)
+                         (match-let ([`((,rrs . 0) ...) (map recur rs)]
+                                     [(cons rb db) (recur b)])
+                           (cons (let-rec rrs rb) db))]
+                        [`(lam (,τs ...) (,ns ...) ,b)
+                         (match-let ([(cons rb db) (recur b)])
+                           (cons (lam (gensym) '()
+                                      (length τs) τs #f
+                                      (list->vector ns) (for/list ([_ ns]) 'val/ref)
+                                      (+ (length τs) (length ns) db) rb)
+                                 0))]
+                        [`(proc-const (,τs ...) ,b)
+                         (match-let ([(cons re 0) (recur `(lam ,τs () ,b))])
+                           (cons (closure re (gensym)) 0))]
+                        [`(case-lam ,cs ...)
+                         (match-let ([`((,rcs . 0) ...) (map recur cs)])
+                           (cons (case-lam (gensym) rcs) 0))]
+                        [`(indirect ,x)
+                         (cons (hash-ref cycle-places x) 0)]
+                        ['void (cons (void) 0)]
+                        [else (cons e 0)]))])
+      (match-let ([(cons rep-expr dep-expr) (recur expr)])
+        (for-each
+         (match-lambda
+           [(list x e)
+            (placeholder-set! (hash-ref cycle-places x) (car (recur e)))])
+         cycles)
+        (make-reader-graph
+         (compilation-top dep-expr (prefix 0 '() '()) rep-expr))))))
\ No newline at end of file
diff --git a/collects/redex/examples/racket-machine/randomized-tests-test.rkt b/collects/redex/examples/racket-machine/randomized-tests-test.rkt
new file mode 100644
index 0000000000..254a58865f
--- /dev/null
+++ b/collects/redex/examples/racket-machine/randomized-tests-test.rkt
@@ -0,0 +1,44 @@
+#lang racket
+
+(require redex/reduction-semantics "randomized-tests.rkt")
+
+(let ([r (run (term (application (lam (val) () (loc-noclr 0)) 'x)) (term ()) 100)])
+  (test-equal
+   (and (answer? r)
+        (equal? (answer-value r) ''x))
+   #t))
+
+(test-predicate
+ cutoff?
+ (run (term (let-void 1 (let-rec ((lam () (0) (application (loc-noclr 0)))) (application (loc-noclr 0))))) (term ()) 100))
+
+(test-predicate
+ non-conf?
+ (run
+  (term
+   (let-one 
+    (lam (val) () (loc-noclr 0))
+    (application
+     (loc-noclr 1)
+     (install-value 1 'non-proc 'x))))
+  (term ())
+  100))
+
+(test-predicate
+ stuck?
+ (run
+  (term
+   (let-one 
+    'x
+    (let-void 
+     1
+     (let-rec
+      ((lam () (0 1) 
+            (branch (loc-noclr 1)
+                    (boxenv 1 (application (loc-noclr 0)))
+                    'y)))
+      (application (loc-noclr 0))))))
+  (term ())
+  100))
+
+(test-results)
diff --git a/collects/redex/examples/racket-machine/randomized-tests.rkt b/collects/redex/examples/racket-machine/randomized-tests.rkt
new file mode 100644
index 0000000000..4c4cd93112
--- /dev/null
+++ b/collects/redex/examples/racket-machine/randomized-tests.rkt
@@ -0,0 +1,342 @@
+#lang racket
+
+(require redex/reduction-semantics
+         (only-in "grammar.rkt" bytecode)
+         (only-in "reduction.rkt" -> load runtime)
+         (only-in "verification.rkt" bytecode-ok?)
+         "model-impl.rkt"
+         compiler/zo-parse compiler/zo-marshal)
+
+(provide (all-defined-out))
+
+;; Test the internal properties (verifier totality, safety, and confluence)
+;; on acyclic expressions. The verifier's totality is tested implicitly by
+;; treating a "no clauses matched" exception as a test failure.
+(define (test-internal-properties 
+         #:verifier [verified? bytecode-ok?]
+         #:reduction [-> ->]
+         #:prepare [prepare fix]
+         #:steps [steps 100]
+         #:attempts [attempts 5000])
+  (redex-check
+   bytecode e (safe-and-confluent? (term e) (term ()) verified? -> steps)
+   #:prepare prepare
+   #:attempts attempts))
+
+;; Tests the internal properties on cyclic expressions.
+(define (test-internal-properties/cycles
+         #:steps [steps 100]
+         #:attempts [attempts 5000]
+         #:print? [print? #t])
+  (redex-check
+   bytecode (side-condition (e (x_0 (name e_0 (proc-const (τ ...) e_0*))) ...)
+                            (equal? (term (x_0 ...))
+                                    (remove-duplicates (term (x_0 ...)))))
+   (safe-and-confluent? (term e) (term ((x_0 e_0) ...)) bytecode-ok? -> steps)
+   #:attempts attempts
+   #:prepare fix-cyclic
+   #:print? print?))
+
+;; Tests the external properties (the model and implementation agree on
+;; verification and evaluation questions).
+(define (test-external-properties
+         #:prepare [prepare (compose optimize fix)]
+         #:model-verifier [model-verified? bytecode-ok?]
+         #:steps [steps 100]
+         #:timeout [timeout 10]
+         #:attempts [attempts 5000]
+         #:print? [print? #t])
+  (redex-check
+   bytecode e
+   (model-impl-consistent? (term e) '() steps timeout model-verified?)
+   #:prepare prepare
+   #:attempts attempts
+   #:print? print?))
+
+; result = answer | stuck | cutoff | non-conf
+(define-struct cutoff ())
+(define-struct stuck (state))
+(define-struct answer (value))
+(define-struct non-conf (values))
+
+; run: e ((x e) ...) nat -> result
+(define (run e cycles cutoff #:reduction [-> ->])
+  (let ([cache (make-hash)])
+    (let loop ([s (term (load ,e ,cycles))]
+               [c cutoff])
+      (let ([r (hash-ref cache s #f)])
+        (if (and r (>= (car r) c))
+            (cdr r)
+            (begin
+              ; If we see this state again while it's marked pending, 
+              ; it will be with a lesser cutoff, and it will indicate a 
+              ; cycle in the reduction graph. Without pruning, a cycle
+              ; the reduction graph produces a cutoff result; with it
+              ; a cylce produces a pending, which is treated identically.
+              (hash-set! cache s (cons c 'pending))
+              (let ([r (cond [(term (halted? ,s)) 
+                            (make-answer 
+                             (if (eq? s 'error)
+                                 'error
+                                 (car s)))]
+                           [(zero? c) (make-cutoff)]
+                           [else
+                            (let ([nexts (map (curryr loop (sub1 c)) (apply-reduction-relation -> s))])
+                              (if (null? nexts)
+                                  (make-stuck s)
+                                  (or (findf non-conf? nexts)
+                                      (findf stuck? nexts)
+                                      (let ([answers (filter answer? nexts)])
+                                        (if (null? answers)
+                                            (make-cutoff)
+                                            (let cmp ([others (cdr answers)])
+                                              (if (null? others)
+                                                  (car answers)
+                                                  (if (equal? (answer-value (car answers))
+                                                              (answer-value (car others)))
+                                                      (cmp (cdr others))
+                                                      (make-non-conf 
+                                                       (list (answer-value (car answers))
+                                                             (answer-value (car others))))))))))))])])
+              (begin
+                (hash-set! cache s (cons c r))
+                r))))))))
+
+(define (verified/cycles? expr cycles verified?)
+  (and (verified? expr)
+       (andmap (match-lambda [`(,_ ,e) (verified? e)])
+               cycles)))
+
+(define (safe-and-confluent? expr cycles verified? -> steps)
+  (with-handlers ([exn:fail? (λ (_) #f)])
+    (or (not (verified/cycles? expr cycles verified?))
+        (match (run expr cycles steps #:reduction ->)
+          [(cutoff) #t]
+          [(answer _) #t]
+          [(stuck _) #f]
+          [(non-conf _) #f]))))
+
+(define (model-impl-consistent? expr cycles steps timeout model-verified?)
+  (define (equiv-results? m i)
+    (match m
+      ['uninit #f]
+      [`(box ,_) #f]
+      ['undefined (impl-undefined-val? i)]
+      [`(clos ,_) (impl-clos-val? i)]
+      ['void (void? i)]
+      [else (equal? m i)]))
+  (with-handlers ([exn:fail? (λ (_) #f)])
+    (let ([model-verified? (verified/cycles? expr cycles model-verified?)]
+          [impl-result (eval-impl-external (model->impl expr cycles) timeout)])
+      (and 
+       (if model-verified? 
+           (not (impl-rejected? impl-result))
+           (impl-rejected? impl-result))
+       (or (not model-verified?)
+           (match (run expr cycles steps)
+             [(cutoff) #t]
+             [(stuck _) #f]
+             [(non-conf _) #f]
+             [(answer a) (equiv-results?
+                          a
+                          (match impl-result
+                            [(impl-answer v) v]
+                            [(impl-exception _) 'error]))]))))))
+
+;; A reimplementation of the optimizations in the implementation's
+;; bytecode reader
+(define (optimize expr)
+  (define value?
+    (let ([v? (redex-match bytecode v)])
+      (λ (e)
+        (or (v? e)
+            (match e
+              [`(proc-const ,_ ,_) #t]
+              [`(lam ,_ ,_ ,_) #t]
+              [`(case-lam ,_ ...) #t]
+              [else #f])))))
+  (define omittable?
+    (match-lambda
+      [`(loc ,_) #t]
+      [`(loc-noclr ,_) #t]
+      [`(loc-box ,_) #t]
+      [`(loc-box-noclr ,_) #t]
+      [`(proc-const ,_ ,_) #t]
+      [`(lam ,_ ,_ ,_) #t]
+      [`(case-lam ,_ ...) #t]
+      [(? (redex-match bytecode v)) #t]
+      [`(branch ,c ,t ,e)
+       (and (omittable? c)
+            (omittable? t)
+            (omittable? e))]
+      [`(let-one ,r ,b)
+       (and (omittable? r)
+            (omittable? b))]
+      [`(,(or 'let-void 'let-void-box) 
+         ,_ 
+         (,(or 'install-value 'install-value-box) 0 ,r ,b))
+       (and (omittable? r)
+            (omittable? b))]
+      [`(,(or 'let-void 'let-void-box) ,_ ,b)
+       (omittable? b)]
+      [`(let-rec ,_ ,b)
+       (omittable? b)]
+      [`(application void ,es ...)
+       (andmap omittable? es)]
+      [else #f]))
+  (let recur ([e expr])
+    (match e
+      [`(branch ,c ,t ,e)
+       (let ([c* (recur c)])
+         (if (value? c*)
+             (if c* (recur t) (recur e))
+             `(branch ,c* ,(recur t) ,(recur e))))]
+      [`(seq ,es ...)
+       (letrec ([flatten (λ (es)
+                           (foldr (λ (e a)
+                                    (match e
+                                      [`(seq ,es ...)
+                                       (append es a)]
+                                      [else (cons e a)]))
+                                  '() es))]
+                ; preserves tail position
+                [omit (λ (es kept?)
+                        (if (null? es)
+                            '()
+                            (if (and (omittable? (car es))
+                                     (not (null? (cdr es))))
+                                (omit (cdr es) kept?)
+                                (cons (car es) (omit (cdr es) #t)))))])
+         (match (omit (map recur (flatten es)) #f)
+           ['() 'void]
+           [`(,e) e]
+           [es `(seq ,@es)]))]
+      [(? list?) (map recur e)]
+      [else e])))
+
+;; Performs a write-read round trip to see the optimizations performed
+;; by the implementation's bytecode reader
+(define (write-read expr)
+  (let-values ([(in out) (make-pipe)]
+               [(tmp) (make-temporary-file)])
+    (zo-marshal-to expr out)
+    (let ([optimized (parameterize ([read-accept-compiled #t])
+                       (read in))])
+      (call-with-output-file tmp #:exists 'truncate
+        (λ (p) (write optimized p))))
+    (begin0
+      (call-with-input-file tmp zo-parse)
+      (delete-file tmp))))
+
+(define-metafunction runtime
+  halted? : p -> b
+  [(halted? (V S H T ())) #t]
+  [(halted? error) #t]
+  [(halted? (V S H T (i_0 i_1 ...))) #f])
+
+(define random-expr
+  (let ([generator (generate-term bytecode e)])
+    (λ (attempt) 
+      (generator (inexact->exact (round (/ (log attempt) (log 5))))))))
+(define random-value
+  (let ([generator (generate-term bytecode v)])
+    (λ () (generator 3))))
+(define-syntax-rule (ref-or-else n e e*)
+  (if (zero? n) e* e))
+
+(define cycle-targets (make-parameter '()))
+
+;; Makes three classes of corrections:
+;; 1. replaces out-of-bounds stack offsets with random in-bounds 
+;;    ones (without checking that the new target contains an
+;;    appropriate value),
+;; 2. replaces `ref' argument annotations with `val' annotations
+;;    when the procedure appears in a context that does not allow
+;;    `ref' arguments (but does not alter the procedure's body), and
+;; 3. replaces `indirect' targets with ones in the `cycle-targets'
+;;    parameter (and replaces the entire `indirect' expression
+;;    with a random value if `cycle-targets' is empty).
+(define (fix expr)
+  (define (localref? i)
+    (memq i '(loc loc-noclr loc-clr loc-box loc-box-noclr loc-box-clr)))
+  (let recur ([depth 0] [refs? #f] [expr expr])
+    (match expr
+      [`(,(? localref? i) ,n) 
+       (ref-or-else depth `(,i ,(modulo n depth)) (random-value))]
+      
+      [`(let-one ,e1 ,e2)
+       `(let-one ,(recur (add1 depth) #f e1)
+                 ,(recur (add1 depth) #f e2))]
+      [`(,(and (or 'let-void 'let-void-box) i) ,n ,e)
+       `(,i ,n ,(recur (+ depth n) #f e))]
+      
+      [`(boxenv ,n ,e)
+       (let ([e* (recur depth #f e)])
+         (ref-or-else depth `(boxenv ,(modulo n depth) ,e*) e*))]
+      [`(,(and (or 'install-value 'install-value-box) i) ,n ,e1 ,e2)
+       (let ([e1* (recur depth #f e1)]
+             [e2* (recur depth #f e2)])
+         (ref-or-else depth `(,i ,(modulo n depth) ,e1* ,e2*) `(seq ,e1* ,e2*)))]
+      
+      [`(application ,e ,es ...)
+       (let ([m (length es)])
+         `(application
+           ,(recur depth #t e)
+           ,@(map (curry recur (+ depth m) #f) es)))]
+      [`(,(and (or 'branch 'seq) i) ,es ...)
+       `(,i ,@(map (curry recur depth #f) es))]
+      [`(let-rec (,ls ...) ,e)
+       (let ([n (min depth (length ls))]
+             [ls* (map (curry recur depth #f) ls)])
+         `(let-rec ,(map (curry recur depth #f) (take ls* n))
+                   ,(recur depth #f e)))]
+      [`(indirect ,c) 
+       (cond [(memq c (cycle-targets))
+              `(indirect ,c)]
+             [(not (null? (cycle-targets))) 
+              `(indirect ,(list-ref (cycle-targets) (random (length (cycle-targets)))))]
+             [else
+              (random-value)])]
+      [`(proc-const (,τs ...) ,e)
+       (let ([n (length τs)])
+         `(proc-const ,(if refs? τs (build-list n (λ (_) 'val)))
+                      ,(recur n #f e)))]
+      [`(case-lam ,ls ...)
+       `(case-lam ,@(map (curry recur depth #f) ls))]
+      [`(lam (,τs ...) (,ns ...) ,e)
+       (let ([m (length τs)])
+         `(lam ,(if refs? τs (build-list m (λ (_) 'val)))
+               ,(if (zero? depth) 
+                    '()
+                    (map (curryr modulo depth) ns))
+               ,(recur (+ m (if (zero? depth) 0 (length ns))) #f e)))]
+      [(? number?) expr]
+      ['void expr]
+      [`(quote ,_) expr]
+      [(? boolean?) expr])))
+
+(define fix-cyclic
+  (match-lambda
+    [`(,e (,xs ,es) ...)
+     (parameterize ([cycle-targets xs])
+       (cons (fix e) 
+             (map (λ (x e) (list x (fix e)))
+                  xs es)))]))
+
+;; Replaces all `indirect' expressions with random values
+(define no-indirects
+  (match-lambda
+    [`(indirect ,_) (random-value)]
+    [(? list? l) (map no-indirects l)]
+    [e e]))
+
+(define (main)
+  (define-syntax-rule (test t k)
+    (match t
+      [#t k]
+      [(counterexample p)
+       (pretty-print p)
+       (exit 1)]))
+  (test (time (test-internal-properties/cycles #:attempts 4000 #:print? #f))
+        (test (time (test-external-properties #:attempts 250 #:print? #f))
+              (void))))
\ No newline at end of file