diff --git a/li.sby b/li.sby
new file mode 100644
index 0000000000000000000000000000000000000000..0e2d26263ec5c0751e6c849543d8b5e9a66143dd
--- /dev/null
+++ b/li.sby
@@ -0,0 +1,15 @@
+[options]
+mode live
+multiclock off
+
+[engines]
+aiger suprove
+
+[script]
+read -formal liveness_example.v
+prep -top top
+show -format dot -notitle
+
+
+[files]
+liveness_example.v
\ No newline at end of file
diff --git a/liveness_example.v b/liveness_example.v
new file mode 100644
index 0000000000000000000000000000000000000000..68edd1ffc83651823933f79cc2677413320318a7
--- /dev/null
+++ b/liveness_example.v
@@ -0,0 +1,41 @@
+`default_nettype none
+
+module top
+(
+    input wire clock,
+    output reg [3:0] egg,
+);
+    reg [3:0] counter = 1;
+    reg [7:0] bigcounter = 7'h3;
+    reg stop = 0;
+    always @ (posedge clock) begin
+
+
+        if (counter == 9)
+        begin
+            stop <= 1;
+        end
+        if (stop == 0)
+        begin
+            counter <= counter + 1;
+        end
+
+        egg <= counter;
+
+        //if (counter < 7) begin
+        assert property (s_eventually counter == 7);
+        //end
+
+
+        if (stop == 1) begin
+        bigcounter <= bigcounter - 1;
+        end
+
+        if (bigcounter == 0) begin
+        stop <= 0;
+        counter <= 0;
+        bigcounter <=7;
+        end
+
+    end // always @ (posedge clock)
+endmodule