diff --git a/contrib/formal/fifo_formal.sby b/contrib/formal/fifo_formal.sby
index 4070122c2..f7d7e969c 100644
--- a/contrib/formal/fifo_formal.sby
+++ b/contrib/formal/fifo_formal.sby
@@ -17,7 +17,7 @@ smtbmc z3
 
 [script]
 read_verilog -formal -sv -DSIMULATION fifo.v
-read_verilog fifo_formal_props.v
+read_verilog -formal fifo_formal_props.v
 prep -top fifo_formal_props
 
 [files]
diff --git a/contrib/formal/mac_formal.sby b/contrib/formal/mac_formal.sby
index 0687dfb84..7ea01f2a1 100644
--- a/contrib/formal/mac_formal.sby
+++ b/contrib/formal/mac_formal.sby
@@ -17,7 +17,7 @@ smtbmc z3
 
 [script]
 read_verilog -formal -sv -DSIMULATION mac.v
-read_verilog mac_formal_props.v
+read_verilog -formal mac_formal_props.v
 prep -top mac_formal_props
 
 [files]
diff --git a/contrib/formal/uart_formal.sby.blocked b/contrib/formal/uart_formal.sby.blocked
index ceb3cbfb1..fb97e2aa6 100644
--- a/contrib/formal/uart_formal.sby.blocked
+++ b/contrib/formal/uart_formal.sby.blocked
@@ -15,7 +15,7 @@ smtbmc z3
 
 [script]
 read_verilog -formal -sv -DSIMULATION uart.v
-read_verilog uart_formal_props.v
+read_verilog -formal uart_formal_props.v
 prep -top uart_formal_props
 
 [files]
diff --git a/docs/NOW.md b/docs/NOW.md
index 850383360..953027e7b 100644
--- a/docs/NOW.md
+++ b/docs/NOW.md
@@ -1,3 +1,14 @@
+# NOW -- the props read with -formal too (2026-08-20)
+
+Last updated: 2026-08-20
+
+## ci(formal): -formal on the props read line (Closes #2271)
+
+- The layer-5 flag fix covered only the DUT line; CI yosys read the props
+  plain and resolved 'assert' as a task name (rc=16) while the local proof
+  had flagged both reads. Reproduced the exact CI error locally without the
+  flag; with it the chain proves Status PASSED. One line per .sby
+
 # NOW -- the first real formal verdicts: fifo and mac PROVE (2026-08-20)
 
 Last updated: 2026-08-20