diff --git a/README.md b/README.md
index 1709c93..f67fcb5 100644
--- a/README.md
+++ b/README.md
@@ -16,7 +16,7 @@ The next two lists will grow during furter development
 * implication operator
 * next operator
 * next[i] operator
-* next_event operator
+* next_event() operator
 
 ## PSL features currently unsupported by GHDL:
 
diff --git a/formal/Makefile b/formal/Makefile
new file mode 100644
index 0000000..d3ac780
--- /dev/null
+++ b/formal/Makefile
@@ -0,0 +1,15 @@
+include tests.mk
+
+
+.PHONY: all clean
+
+all: ${psl_tests}
+
+
+%: ../src/%.vhd ../src/pkg.vhd ../src/sequencer.vhd ../src/hex_sequencer.vhd %.sby
+	mkdir -p work
+	-sby --yosys "yosys -m ghdl" -f -d work/$@ $@.sby prove
+
+
+clean:
+	rm -rf work
diff --git a/formal/psl_always.sby b/formal/psl_always.sby
new file mode 100644
index 0000000..c2f063a
--- /dev/null
+++ b/formal/psl_always.sby
@@ -0,0 +1,18 @@
+[tasks]
+prove
+
+[options]
+depth 25
+prove: mode bmc
+
+[engines]
+prove: smtbmc z3
+
+[script]
+prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_always.vhd -e psl_always
+prep -top psl_always
+
+[files]
+../src/pkg.vhd
+../src/sequencer.vhd
+../src/psl_always.vhd
diff --git a/formal/psl_never.sby b/formal/psl_never.sby
new file mode 100644
index 0000000..76b6483
--- /dev/null
+++ b/formal/psl_never.sby
@@ -0,0 +1,18 @@
+[tasks]
+prove
+
+[options]
+depth 25
+prove: mode bmc
+
+[engines]
+prove: smtbmc z3
+
+[script]
+prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_never.vhd -e psl_never
+prep -top psl_never
+
+[files]
+../src/pkg.vhd
+../src/sequencer.vhd
+../src/psl_never.vhd
diff --git a/formal/psl_next.sby b/formal/psl_next.sby
new file mode 100644
index 0000000..4c51115
--- /dev/null
+++ b/formal/psl_next.sby
@@ -0,0 +1,18 @@
+[tasks]
+prove
+
+[options]
+depth 25
+prove: mode bmc
+
+[engines]
+prove: smtbmc z3
+
+[script]
+prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_next.vhd -e psl_next
+prep -top psl_next
+
+[files]
+../src/pkg.vhd
+../src/sequencer.vhd
+../src/psl_next.vhd
diff --git a/formal/psl_next_3.sby b/formal/psl_next_3.sby
new file mode 100644
index 0000000..07eab26
--- /dev/null
+++ b/formal/psl_next_3.sby
@@ -0,0 +1,18 @@
+[tasks]
+prove
+
+[options]
+depth 25
+prove: mode bmc
+
+[engines]
+prove: smtbmc z3
+
+[script]
+prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_next_3.vhd -e psl_next_3
+prep -top psl_next_3
+
+[files]
+../src/pkg.vhd
+../src/sequencer.vhd
+../src/psl_next_3.vhd
diff --git a/formal/psl_next_event.sby b/formal/psl_next_event.sby
new file mode 100644
index 0000000..cd5a419
--- /dev/null
+++ b/formal/psl_next_event.sby
@@ -0,0 +1,18 @@
+[tasks]
+prove
+
+[options]
+depth 25
+prove: mode bmc
+
+[engines]
+prove: smtbmc z3
+
+[script]
+prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_next_event.vhd -e psl_next_event
+prep -top psl_next_event
+
+[files]
+../src/pkg.vhd
+../src/sequencer.vhd
+../src/psl_next_event.vhd
diff --git a/formal/tests.mk b/formal/tests.mk
new file mode 100644
index 0000000..7f24230
--- /dev/null
+++ b/formal/tests.mk
@@ -0,0 +1,6 @@
+psl_tests := \
+psl_always \
+psl_never \
+psl_next \
+psl_next_3 \
+psl_next_event
diff --git a/src/psl_always.vhd b/src/psl_always.vhd
index 1d0dff4..edeb5c6 100644
--- a/src/psl_always.vhd
+++ b/src/psl_always.vhd
@@ -18,16 +18,17 @@ architecture psl of psl_always is
 begin
 
 
-  SEQ : sequencer generic map ("_-_-_") port map (clk, a);
+  --                            012345
+  SEQ : sequencer generic map ("--____") port map (clk, a);
 
 
   -- All is sensitive to rising edge of clk
   default clock is rising_edge(clk);
 
-  -- Signal a has to be low at cycle 0 only
+  -- This assertion holds
   WITHOUT_ALWAYS_a : assert a;
 
-  -- Signal a has to be low forever
+  -- This assertion doesn't hold at cycle 2
   WITH_ALWAYS_a : assert always a;
 
 
diff --git a/src/psl_never.vhd b/src/psl_never.vhd
index 1e0af4c..9b938fc 100644
--- a/src/psl_never.vhd
+++ b/src/psl_never.vhd
@@ -13,22 +13,28 @@ end entity psl_never;
 
 architecture psl of psl_never is
 
-  signal a : std_logic;
+  signal a, b : std_logic;
 
 begin
 
 
-  SEQ : sequencer generic map ("_-_-_") port map (clk, a);
+  --                              0123
+  SEQ_A : sequencer generic map ("____") port map (clk, a);
+  SEQ_B : sequencer generic map ("__-_") port map (clk, b);
 
 
   -- All is sensitive to rising edge of clk
   default clock is rising_edge(clk);
 
-  -- Signal a has to be low forever
-  NEVER_a : assert never a;
+  -- This assertion holds
+  NEVER_0_a : assert never a;
 
   -- Equivalent assert with always and negation
+  -- This assertion holds
   ALWAYS_a : assert always not a;
 
+  -- This assertion doesn't hold at cycle 2
+  NEVER_1_a : assert never b;
+
 
 end architecture psl;
diff --git a/src/psl_next.vhd b/src/psl_next.vhd
index 517fac1..ba51693 100644
--- a/src/psl_next.vhd
+++ b/src/psl_next.vhd
@@ -19,9 +19,11 @@ architecture psl of psl_next is
 begin
 
 
+  --                              012345678901
   SEQ_A : sequencer generic map ("_-__--__-__") port map (clk, a);
   SEQ_B : sequencer generic map ("_--__--__--") port map (clk, b);
 
+  --                              012345678901
   SEQ_C : sequencer generic map ("_-__--__-__") port map (clk, c);
   SEQ_D : sequencer generic map ("_--__-___--") port map (clk, d);
 
diff --git a/src/psl_next_3.vhd b/src/psl_next_3.vhd
index 29ea1ee..ae94265 100644
--- a/src/psl_next_3.vhd
+++ b/src/psl_next_3.vhd
@@ -20,12 +20,15 @@ architecture psl of psl_next_3 is
 begin
 
 
+  --                              01234567890
   SEQ_A : sequencer generic map ("__-_-______") port map (clk, a);
   SEQ_B : sequencer generic map ("_____-_-___") port map (clk, b);
 
+  --                              01234567890
   SEQ_C : sequencer generic map ("__-_-______") port map (clk, c);
   SEQ_D : sequencer generic map ("_____-_____") port map (clk, d);
 
+  --                              01234567890
   SEQ_E : sequencer generic map ("__-_-______") port map (clk, e);
   SEQ_F : sequencer generic map ("_____-----_") port map (clk, f);
 
@@ -36,7 +39,7 @@ begin
   -- This assertion holds
   NEXT_0_a : assert always (a -> next[3] (b));
 
-  -- This assertion doesn't hold at cycle 8
+  -- This assertion doesn't hold at cycle 7
   NEXT_1_a : assert always (c -> next[3] (d));
 
   -- This assertion holds
diff --git a/src/sequencer.vhd b/src/sequencer.vhd
index 4ef80cf..f6c3ccf 100644
--- a/src/sequencer.vhd
+++ b/src/sequencer.vhd
@@ -21,7 +21,7 @@ end entity sequencer;
 
 architecture rtl of sequencer is
 
-  signal cycle : natural := 0;
+  signal index : natural := seq'low;
   signal ch    : character;
 
 begin
@@ -30,13 +30,13 @@ begin
   process (clk) is
   begin
     if rising_edge(clk) then
-      if (cycle < seq'length) then
-        cycle <= cycle + 1;
+      if (index < seq'high) then
+        index <= index + 1;
       end if;
     end if;
   end process;
 
-  ch <= seq(cycle+1);
+  ch <= seq(index);
 
   data <= to_bit(ch);