diff --git a/fsm/Makefile b/fsm/Makefile
index d9d3aac..eb87b90 100644
--- a/fsm/Makefile
+++ b/fsm/Makefile
@@ -6,6 +6,7 @@ YOSYS = yosys
 PNR = nextpnr-ice40
 IPACK = icepack
 BURN = iceFUNprog
+SBY = sby
 
 VERILATOR=verilator
 VERILATOR_ROOT ?= $(shell bash -c 'verilator -V|grep VERILATOR_ROOT | head -1 | sed -e "s/^.*=\s*//"')
@@ -13,9 +14,11 @@ VINC := $(VERILATOR_ROOT)/include
 
 RTL_SRC := $(wildcard rtl/*.v)
 SIM_SRC := $(wildcard sim/*.cc)
+FV_SRC := sim/top.sby
+
 BUILD_DIR := ./build
 
-.PHONY: all burn
+.PHONY: all burn fv clean
 all: $(SIM_TARGET)  $(BIN_TARGET)
 
 # -GWIDTH=5 allows passing parameter to verilog module
@@ -51,6 +54,8 @@ $(BIN_TARGET): $(BUILD_DIR)/top.json $(PCF) $(TIMING)
 burn: $(BIN_TARGET)
 	@$(BURN) $<
 
-.PHONY: clean
+fv:
+	@$(SBY) -f $(FV_SRC) -d $(BUILD_DIR)/fv
+
 clean:
 	rm -rf $(BUILD_DIR)
diff --git a/fsm/rtl/top.v b/fsm/rtl/top.v
index fe786af..35daa14 100644
--- a/fsm/rtl/top.v
+++ b/fsm/rtl/top.v
@@ -56,6 +56,44 @@ module top(i_clk, o_led, lcol1);
       endcase
    end
 
+`ifdef	FORMAL
+   // led_index should never go beyond 13
+	always @(*)
+		assert(led_index <= 4'hd);
+
+	// I prefix all of the registers (or wires) I use in formal
+	// verification with f_, to distinguish them from the rest of the
+	// project.
+	reg	f_valid_output;
+   always @(*)
+   begin
+      // Determining if the output is valid or not is a rather
+      // complex task--unusual for a typical assertion.  Here, we'll
+      // use f_valid_output and a series of _blocking_ statements
+      // to determine if the output is one of our valid outputs.
+      f_valid_output = 0;
+
+      case(obuf)
+         8'h01: f_valid_output = 1'b1;
+         8'h02: f_valid_output = 1'b1;
+         8'h04: f_valid_output = 1'b1;
+         8'h08: f_valid_output = 1'b1;
+         8'h10: f_valid_output = 1'b1;
+         8'h20: f_valid_output = 1'b1;
+         8'h40: f_valid_output = 1'b1;
+         8'h80: f_valid_output = 1'b1;
+      endcase
+
+      assert(f_valid_output);
+
+      // SV supports a $onehot function which we could've also used
+      // depending upon your version of Yosys.  This function will
+      // be true if one, and only one, bit in the argument is true.
+      // Hence we might have said
+      // assert($onehot(o_led));
+      // and avoided this case statement entirely.
+   end
+`endif
    /* shift reg
    // shifting bit
    always @(posedge clk_12MHz)
diff --git a/fsm/sim/top.sby b/fsm/sim/top.sby
new file mode 100644
index 0000000..3d0b7f6
--- /dev/null
+++ b/fsm/sim/top.sby
@@ -0,0 +1,13 @@
+[options]
+mode prove
+
+[engines]
+smtbmc
+
+[script]
+read -formal *.v
+prep -top top
+
+[files]
+rtl/top.v
+rtl/clk_gen.v