diff --git a/Makefile b/Makefile
index c70d3c4..1b42bbf 100644
--- a/Makefile
+++ b/Makefile
@@ -4,6 +4,8 @@
 #   make MOD=synchronizer         compile rtl/ + that tb, run; a test FAIL exits nonzero
 #   make wave MOD=synchronizer    same, then open the waveform in surfer (opens even on FAIL)
 #   make formal MOD=uart_rx       run every SymbiYosys task in formal/$(MOD).sby; a FAIL exits nonzero
+#   make trace MOD=uart_rx        print a formal counterexample as text
+#   make view-formal MOD=uart_rx  open a formal waveform in surfer; error if .vcd missing
 #   make cocotb                   run the Python top-level testbench (tb/test_uart.py) on the UART core
 #   make clean                    delete build artifacts (build/, *.vcd)
 
@@ -30,6 +32,36 @@ formal:
 	@test -n "$(MOD)" || { echo "usage: make formal MOD=<module>  (e.g. MOD=uart_rx)"; exit 1; }
 	sby -f $(FORMAL)
 
+# Echoes MOD's run directory, prompting when the .sby split into several tasks
+define pick_run
+	test -n "$(MOD)" || { echo "usage: make $@ MOD=<module>  (e.g. MOD=uart_rx)" >&2; exit 1; }; \
+	runs=$$(for d in formal/$(MOD)/ formal/$(MOD)_*/; do [ -f "$$d/status" ] && echo "$${d%/}"; done); \
+	[ -n "$$runs" ] || { echo "No runs for $(MOD), try: make formal MOD=$(MOD)" >&2; exit 1; }; \
+	if [ $$(echo "$$runs" | wc -l) -eq 1 ]; then echo "$$runs"; else \
+	  i=0; for d in $$runs; do i=$$((i+1)); \
+	    printf '  %d) %-12s %-6s%s\n' $$i "$$(basename $$d | sed 's/^$(MOD)_//')" \
+	      "$$(cut -d' ' -f1 $$d/status)" \
+	      "$$(find $$d -name trace.yw 2>/dev/null | head -1 | sed 's/.*/counterexample/')" >&2; \
+	  done; \
+	  printf 'Select task: ' >&2; read n; \
+	  sel=$$(echo "$$runs" | sed -n "$${n}p" 2>/dev/null); \
+	  [ -d "$$sel" ] || { echo "No task $$n" >&2; exit 1; }; \
+	  echo "$$sel"; fi
+endef
+
+trace:
+	@dir=$$($(pick_run)); test -n "$$dir" || exit 1; \
+	yw=$$(find $$dir -name 'trace.yw' 2>/dev/null | head -1); \
+	test -n "$$yw" || { echo "Error: no trace.yw in $$dir/, that run has no counterexample"; exit 1; }; \
+	yosys-witness display $$yw
+
+view-formal:
+	@dir=$$($(pick_run)); test -n "$$dir" || exit 1; \
+	vcd=$$(find $$dir -name '*.vcd' 2>/dev/null | head -1); \
+	test -n "$$vcd" || { echo "Error: no .vcd found in $$dir/"; exit 1; }; \
+	echo "surfer $$vcd"; \
+	surfer $$vcd $$(test -f $$dir.ron && echo "-s $$dir.ron") &
+
 cocotb:
 	rm -rf sim_build results.xml
 	$(MAKE) -f cocotb.mk
@@ -38,4 +70,4 @@ clean:
 	rm -rf build *.vcd sim_build results.xml
 
 .DEFAULT_GOAL := run
-.PHONY: run wave formal cocotb clean
+.PHONY: run wave formal trace view-formal cocotb clean
diff --git a/README.md b/README.md
index 34f353e..225a697 100644
--- a/README.md
+++ b/README.md
@@ -43,6 +43,8 @@ Synthesized for the Xilinx Artix-7 XC7A35T through Yosys and nextpnr-xilinx.
 make MOD=uart_rx                    # run a module's testbench
 make wave MOD=uart_rx               # run the testbench and open the waveform in Surfer
 make formal MOD=uart_rx             # run the module's SymbiYosys proof
+make trace MOD=uart_rx              # print a formal counterexample as text
+make view-formal MOD=uart_rx        # open a formal waveform in Surfer
 make cocotb                         # run the top-level cocotb loopback test
 ./synth_stats.sh uart               # report a module's synthesis cost
 ./fmax.sh uart_tx tt_uart_tx clk    # fmax and utilization