diff --git a/examples/wishbone/read_write.tx b/examples/wishbone/read_write.tx
index 3eaac591..c01e6d40 100644
--- a/examples/wishbone/read_write.tx
+++ b/examples/wishbone/read_write.tx
@@ -1,7 +1,9 @@
 trace {
     reset();
     write(0b1111, 0x4000000, 0x1111);
-    // reset();
+    reset();
     read(0b1111, 0x4000000, 0x1111);
-    //idle_no_cycle();
+    idle_no_cycle();
+    write(0b1111, 0x4000000, 0x1111);
+    reset();
 }
diff --git a/examples/wishbone/wishbone_fv.prot b/examples/wishbone/wishbone_fv.prot
new file mode 100644
index 00000000..00eec9aa
--- /dev/null
+++ b/examples/wishbone/wishbone_fv.prot
@@ -0,0 +1,564 @@
+// Wishbone pins for this project from the server (the one servicing requests) perspective
+interface Wishbone {
+    // high active RST pin (the wishbone spec requires all signals to be high active)
+    in i_reset: u1,
+    // acknowledge (from server)
+    out i_wb_ack: u1,
+    // address (from client)
+    in i_wb_addr: u32,
+    // cycle output, indicates bus cycle in progress (from client)
+    in i_wb_cyc: u1,
+    // read data from server
+    out i_wb_data: u32,
+    // write data from client
+    in i_wb_idata: u32,
+    // error from server
+    out i_wb_err: u1,
+    // mask for data in/out from client
+    in i_wb_sel: u4,
+    // indicates a valid transfer cycle from client
+    in i_wb_stb: u1,
+    // write enable (i.e. not read) from client
+    in i_wb_we: u1,
+    in BTE: u2,
+    in CTI: u3,
+}
+
+prot reset<self: Wishbone>() {
+    self.RST := 1'b1;
+    self.CYC := 1'b0;
+    self.STB := 1'b0;
+    step();
+}
+
+#[idle]
+prot idle_no_cycle<self: Wishbone>() {
+    self.RST := 1'b0;
+    self.CYC := 1'b0;
+    step();
+}
+
+prot idle_continue_cycle<self: Wishbone>() {
+    self.RST := 1'b0;
+    self.CYC := 1'b1;
+    self.STB := 1'b0;
+    step();
+}
+
+prot write<self: Wishbone>(mask: u4, addr: u32, data: u32) {
+    assert_eq(mask, 4'b1111); // TODO: support other masks
+    // no RST
+    self.RST := 1'b0;
+    // classic cycle (in which case bte is don't care)
+    self.CTI := 3'b0;
+    self.BTE := X;
+
+    // in our simple version, we always drive cyc and stb together
+    self.CYC := 1'b1;
+    self.STB := 1'b1;
+
+    // we are writing
+    self.WE := 1'b1;
+
+    // apply parameters
+    self.ADR := addr;
+    self.SEL := mask;
+    self.DAT_O := data;
+
+    // TODO: masking
+    // if !mask[0] { DAT_O[ 7: 0] := X; }
+    // if !mask[1] { DAT_O[15: 8] := X; }
+    // if !mask[2] { DAT_O[23:16] := X; }
+    // if !mask[3] { DAT_O[31:24] := X; }
+
+
+    while self.ACK == 1'b0 {
+        step();
+    }
+
+    // acknowledge is now true
+    step();
+}
+
+prot read<self: Wishbone>(mask: u4, addr: u32, data: u32) {
+    assert_eq(mask, 4'b1111); // TODO: support other masks
+
+    // no RST
+    self.RST := 1'b0;
+    // classic cycle (in which case bte is don't care)
+    self.CTI := 3'b0;
+    self.BTE := X;
+
+    // in our simple version, we always drive cyc and stb together
+    self.CYC := 1'b1;
+    self.STB := 1'b1;
+
+    // we are reading
+    self.WE := 1'b0;
+
+    // apply parameters
+    self.ADR := addr;
+    self.SEL := mask;
+    self.DAT_O := X;
+
+    while self.ACK == 1'b0 {
+        step();
+    }
+
+    // TODO: masking
+    // if mask[0] { assert_eq(self.DAT_I[ 7: 0], data[ 7: 0]); }
+    // if mask[1] { assert_eq(self.DAT_I[15: 8], data[15: 8]); }
+    // if mask[2] { assert_eq(self.DAT_I[23:16], data[23:16]); }
+    // if mask[3] { assert_eq(self.DAT_I[31:24], data[31:24]); }
+
+    assert_eq(self.DAT_I, data);
+    step();
+}
+
+// a burst with only a single item uses a special cti of 7
+prot write_burst_single<self: Wishbone>(mask: u4, addr: u32, data: u32) {
+    assert_eq(mask, 4'b1111); // TODO: support other masks
+
+    // no RST
+    self.RST := 1'b0;
+    // final burst item
+    self.CTI := 3'b111;
+    self.BTE := X;
+
+    // in our simple version, we always drive cyc and stb together
+    self.CYC := 1'b1;
+    self.STB := 1'b1;
+
+    // we are writing
+    self.WE := 1'b1;
+
+    // apply parameters
+    self.ADR := addr;
+    self.SEL := mask;
+    self.DAT_O := data;
+
+    // wait for ack
+    while self.ACK == 1'b0 {
+        step();
+    }
+
+    // acknowledge is now true for one cycle
+    step();
+}
+
+// a burst with only a single item uses a special cti of 7
+prot read_burst_single<self: Wishbone>(mask: u4, addr: u32, data: u32) {
+    assert_eq(mask, 4'b1111); // TODO: support other masks
+
+    // no RST
+    self.RST := 1'b0;
+    // final burst item
+    self.CTI := 3'b111;
+    self.BTE := X;
+
+    // in our simple version, we always drive cyc and stb together
+    self.CYC := 1'b1;
+    self.STB := 1'b1;
+
+    // we are reading
+    self.WE := 1'b0;
+
+    // apply parameters
+    self.ADR := addr;
+    self.SEL := mask;
+
+
+    // wait for ack
+    while self.ACK == 1'b0 {
+        step();
+    }
+
+    // acknowledge is now true for one cycle and we get the data
+    assert_eq(self.DAT_I, data); // TODO: take mask into account
+    step();
+}
+
+prot write_burst_const<self: Wishbone>(mask: u4, addr: u32, data: [u32]++) {
+    assert_eq(mask, 4'b1111); // TODO: support other masks
+
+    // no RST
+    self.RST := 1'b0;
+    // constant burst cycle (in which case bte is don't care)
+    self.CTI := 3'b001;
+    self.BTE := X;
+
+    // in our simple version, we always drive cyc and stb together
+    self.CYC := 1'b1;
+    self.STB := 1'b1;
+
+    // we are writing
+    self.WE := 1'b1;
+
+    // apply parameters
+    self.ADR := addr;
+    self.SEL := mask;
+
+    for d in data {
+        self.DAT_O := d;
+
+        // indicate end of cycle for last item
+        if is_last() {
+            self.CTI := 3'b111;
+        }
+
+        // wait for ack
+        while self.ACK == 1'b0 {
+            step();
+        }
+
+        // acknowledge is now true for one cycle
+        step();
+    }
+}
+
+prot read_burst_const<self: Wishbone>(mask: u4, addr: u32, data: [u32]++) {
+    assert_eq(mask, 4'b1111); // TODO: support other masks
+
+    // no RST
+    self.RST := 1'b0;
+    // constant burst cycle (in which case bte is don't care)
+    self.CTI := 3'b001;
+    self.BTE := X;
+
+    // in our simple version, we always drive cyc and stb together
+    self.CYC := 1'b1;
+    self.STB := 1'b1;
+
+    // we are reading
+    self.WE := 1'b0;
+
+    // apply parameters
+    self.ADR := addr;
+    self.SEL := mask;
+
+    for d in data {
+        // indicate end of cycle for last item
+        if is_last() {
+            self.CTI := 3'b111;
+        }
+
+        // wait for ack
+        while self.ACK == 1'b0 {
+            step();
+        }
+
+        // acknowledge is now true for one cycle and we get the data
+        assert_eq(self.DAT_I, d); // TODO: take mask into account
+        step();
+    }
+}
+
+prot write_burst_increment_linear<self: Wishbone>(mask: u4, start_addr: u32, data: [u32]++) {
+    assert_eq(mask, 4'b1111); // TODO: support other masks
+
+    // no RST
+    self.RST := 1'b0;
+    // incremental linear burst
+    self.CTI := 3'b010;
+    self.BTE := 2'b00;
+
+    // in our simple version, we always drive cyc and stb together
+    self.CYC := 1'b1;
+    self.STB := 1'b1;
+
+    // we are writing
+    self.WE := 1'b1;
+
+    // apply parameters
+    self.SEL := mask;
+
+    for d in data {
+        self.ADR := start_addr + (iter_count::<u30>() ## 2'b00);
+        self.DAT_O := d;
+
+        // indicate end of cycle for last item
+        if is_last() {
+            self.CTI := 3'b111;
+        }
+
+        // wait for ack
+        while self.ACK == 1'b0 {
+            step();
+        }
+
+        // acknowledge is now true for one cycle
+        step();
+    }
+}
+
+prot read_burst_increment_linear<self: Wishbone>(mask: u4, start_addr: u32, data: [u32]++) {
+    assert_eq(mask, 4'b1111); // TODO: support other masks
+
+    // no RST
+    self.RST := 1'b0;
+    // incremental linear burst
+    self.CTI := 3'b010;
+    self.BTE := 2'b00;
+
+    // in our simple version, we always drive cyc and stb together
+    self.CYC := 1'b1;
+    self.STB := 1'b1;
+
+    // we are reading
+    self.WE := 1'b0;
+
+    // apply parameters
+    self.SEL := mask;
+
+    for d in data {
+        self.ADR := start_addr + (iter_count::<u30>() ## 2'b00);
+
+        // indicate end of cycle for last item
+        if is_last() {
+            self.CTI := 3'b111;
+        }
+
+        // wait for ack
+        while self.ACK == 1'b0 {
+            step();
+        }
+
+        // acknowledge is now true for one cycle and we get the data
+        assert_eq(self.DAT_I, d); // TODO: take mask into account
+        step();
+    }
+}
+
+
+prot write_burst_increment_wrap_4<self: Wishbone>(mask: u4, start_addr: u32, data: [u32]++) {
+    assert_eq(mask, 4'b1111); // TODO: support other masks
+
+    // no RST
+    self.RST := 1'b0;
+    // incremental linear burst
+    self.CTI := 3'b010;
+    self.BTE := 2'b01; // wrap 4
+
+    // in our simple version, we always drive cyc and stb together
+    self.CYC := 1'b1;
+    self.STB := 1'b1;
+
+    // we are writing
+    self.WE := 1'b1;
+
+    // apply parameters
+    self.SEL := mask;
+
+    for d in data {
+        // we increment the last 2 bits, modulo the 2-bits that are always zero because of the 32-bit interface
+        self.ADR := start_addr[31:4] ## (start_addr[3:2] + iter_count::<u2>()) ## start_addr[1:0];
+        self.DAT_O := d;
+
+        // indicate end of cycle for last item
+        if is_last() {
+            self.CTI := 3'b111;
+        }
+
+        // wait for ack
+        while self.ACK == 1'b0 {
+            step();
+        }
+
+        // acknowledge is now true for one cycle
+        step();
+    }
+}
+
+prot read_burst_increment_wrap_4<self: Wishbone>(mask: u4, start_addr: u32, data: [u32]++) {
+    assert_eq(mask, 4'b1111); // TODO: support other masks
+
+    // no RST
+    self.RST := 1'b0;
+    // incremental linear burst
+    self.CTI := 3'b010;
+    self.BTE := 2'b01; // wrap 4
+
+    // in our simple version, we always drive cyc and stb together
+    self.CYC := 1'b1;
+    self.STB := 1'b1;
+
+    // we are reading
+    self.WE := 1'b0;
+
+    // apply parameters
+    self.SEL := mask;
+
+    for d in data {
+        // we increment the last 2 bits, modulo the 2-bits that are always zero because of the 32-bit interface
+        self.ADR := start_addr[31:4] ## (start_addr[3:2] + iter_count::<u2>()) ## start_addr[1:0];
+
+        // indicate end of cycle for last item
+        if is_last() {
+            self.CTI := 3'b111;
+        }
+
+        // wait for ack
+        while self.ACK == 1'b0 {
+            step();
+        }
+
+        // acknowledge is now true for one cycle and we get the data
+        assert_eq(self.DAT_I, d); // TODO: take mask into account
+        step();
+    }
+}
+
+prot write_burst_increment_wrap_8<self: Wishbone>(mask: u4, start_addr: u32, data: [u32]++) {
+    assert_eq(mask, 4'b1111); // TODO: support other masks
+
+    // no RST
+    self.RST := 1'b0;
+    // incremental linear burst
+    self.CTI := 3'b010;
+    self.BTE := 2'b10; // wrap 8
+
+    // in our simple version, we always drive cyc and stb together
+    self.CYC := 1'b1;
+    self.STB := 1'b1;
+
+    // we are writing
+    self.WE := 1'b1;
+
+    // apply parameters
+    self.SEL := mask;
+
+    for d in data {
+        // we increment the last 3 bits, modulo the 2-bits that are always zero because of the 32-bit interface
+        self.ADR := start_addr[31:5] ## (start_addr[4:2] + iter_count::<u3>()) ## start_addr[1:0];
+        self.DAT_O := d;
+
+        // indicate end of cycle for last item
+        if is_last() {
+            self.CTI := 3'b111;
+        }
+
+        // wait for ack
+        while self.ACK == 1'b0 {
+            step();
+        }
+
+        // acknowledge is now true for one cycle
+        step();
+    }
+}
+
+prot read_burst_increment_wrap_8<self: Wishbone>(mask: u4, start_addr: u32, data: [u32]++) {
+    assert_eq(mask, 4'b1111); // TODO: support other masks
+
+    // no RST
+    self.RST := 1'b0;
+    // incremental linear burst
+    self.CTI := 3'b010;
+    self.BTE := 2'b10; // wrap 8
+
+    // in our simple version, we always drive cyc and stb together
+    self.CYC := 1'b1;
+    self.STB := 1'b1;
+
+    // we are reading
+    self.WE := 1'b0;
+
+    // apply parameters
+    self.SEL := mask;
+
+    for d in data {
+        // we increment the last 3 bits, modulo the 2-bits that are always zero because of the 32-bit interface
+        self.ADR := start_addr[31:5] ## (start_addr[4:2] + iter_count::<u3>()) ## start_addr[1:0];
+
+        // indicate end of cycle for last item
+        if is_last() {
+            self.CTI := 3'b111;
+        }
+
+        // wait for ack
+        while self.ACK == 1'b0 {
+            step();
+        }
+
+        // acknowledge is now true for one cycle and we get the data
+        assert_eq(self.DAT_I, d); // TODO: take mask into account
+        step();
+    }
+}
+
+prot write_burst_increment_wrap_16<self: Wishbone>(mask: u4, start_addr: u32, data: [u32]++) {
+    assert_eq(mask, 4'b1111); // TODO: support other masks
+
+    // no RST
+    self.RST := 1'b0;
+    // incremental linear burst
+    self.CTI := 3'b010;
+    self.BTE := 2'b11; // wrap 16
+
+    // in our simple version, we always drive cyc and stb together
+    self.CYC := 1'b1;
+    self.STB := 1'b1;
+
+    // we are writing
+    self.WE := 1'b1;
+
+    // apply parameters
+    self.SEL := mask;
+
+    for d in data {
+        // we increment the last 4 bits, modulo the 2-bits that are always zero because of the 32-bit interface
+        self.ADR := start_addr[31:6] ## (start_addr[5:2] + iter_count::<u4>()) ## start_addr[1:0];
+
+        // indicate end of cycle for last item
+        if is_last() {
+            self.CTI := 3'b111;
+        }
+
+        // wait for ack
+        while self.ACK == 1'b0 {
+            step();
+        }
+
+        // acknowledge is now true for one cycle
+        step();
+    }
+}
+
+prot read_burst_increment_wrap_16<self: Wishbone>(mask: u4, start_addr: u32, data: [u32]++) {
+    assert_eq(mask, 4'b1111); // TODO: support other masks
+
+    // no RST
+    self.RST := 1'b0;
+    // incremental linear burst
+    self.CTI := 3'b010;
+    self.BTE := 2'b11; // wrap 16
+
+    // in our simple version, we always drive cyc and stb together
+    self.CYC := 1'b1;
+    self.STB := 1'b1;
+
+    // we are writing
+    self.WE := 1'b0;
+
+    // apply parameters
+    self.SEL := mask;
+
+    for d in data {
+        // we increment the last 4 bits, modulo the 2-bits that are always zero because of the 32-bit interface
+        self.ADR := start_addr[31:6] ## (start_addr[5:2] + iter_count::<u4>()) ## start_addr[1:0];
+
+        // indicate end of cycle for last item
+        if is_last() {
+            self.CTI := 3'b111;
+        }
+
+        // wait for ack
+        while self.ACK == 1'b0 {
+            step();
+        }
+
+        // acknowledge is now true for one cycle and we get the data
+        assert_eq(self.DAT_I, d); // TODO: take mask into account
+        step();
+    }
+}
diff --git a/graph-interp/src/main.rs b/graph-interp/src/main.rs
index 9ab03366..246bb20d 100644
--- a/graph-interp/src/main.rs
+++ b/graph-interp/src/main.rs
@@ -20,6 +20,7 @@ use protocols::ir::lowering::lower_ast_to_ir;
 use protocols::ir::propagate_assigns::propagate_assignments;
 use protocols::ir::proto_graph::ProtoGraph;
 use protocols::ir::reaching_defs::{format_reaching_defs, reaching_definitions};
+use protocols::ir::steady_state_lowering::lower_steady_state;
 use protocols::ir::trace_lowering::lower_trace_to_ir;
 use protocols::{PatronusSim, PortId, Value, frontend, transaction_frontend};
 use rustc_hash::FxHashMap;
@@ -84,6 +85,9 @@ struct Cli {
 
     #[arg(long, default_value_t)]
     bound: usize,
+
+    #[arg(long)]
+    steady_state: bool,
 }
 
 fn load_protocols(cli: &Cli) -> (SymbolTable, Vec<Module>) {
@@ -503,6 +507,142 @@ fn run_bmc(cli: &Cli, st: &SymbolTable, module: &Module, traces: &[Vec<(String,
     }
 }
 
+fn run_steady_state(
+    cli: &Cli,
+    st: &SymbolTable,
+    module: &Module,
+    traces: &[Vec<(String, Vec<Value>)>],
+) {
+    let protos_by_name: FxHashMap<String, &Protocol> =
+        module.protos.iter().map(|p| (p.name.clone(), p)).collect();
+
+    for (trace_index, trace) in traces.iter().enumerate() {
+        print_trace_separator(trace_index);
+        let mut used_protocol_names = Vec::new();
+        for (name, _) in trace {
+            if !used_protocol_names.contains(&name.as_str()) {
+                used_protocol_names.push(name.as_str());
+            }
+        }
+        let used_protocols: Vec<Protocol> = used_protocol_names
+            .iter()
+            .map(|name| (*protos_by_name.get(*name).unwrap()).clone())
+            .collect();
+        let protocol_arg_symbols: Vec<_> = used_protocols
+            .iter()
+            .flat_map(|protocol| protocol.args.iter().map(|arg| arg.symbol()))
+            .collect();
+        let protocol_choice_indices: FxHashMap<&str, u64> = used_protocol_names
+            .iter()
+            .enumerate()
+            .map(|(index, name)| (*name, index as u64))
+            .collect();
+
+        let sim = PatronusSim::new(&cli.verilog, cli.module.as_deref(), module, None).unwrap();
+        // The graph and DUT transition system must share an expression
+        // context, including port expressions such as DUT.o_ack.
+        let (mut pg, proto_choice) = lower_steady_state(used_protocols, st, sim.ctx.clone());
+        pg.garbage_collect_unreachable();
+        pg = determinized(pg, st);
+
+        if cli.graphout {
+            println!("{}", to_dot_string(&pg, st));
+        }
+
+        let port_expr_refs: FxHashMap<PortId, ExprRef> = FxHashMap::from_iter(
+            sim.ios()
+                .filter_map(|port| sim.get_port_expr(port).map(|expr| (port, expr))),
+        );
+        let res = into_bmc_transition_system(
+            pg,
+            sim.sys.clone(),
+            vec![proto_choice],
+            sim.port_map.clone(),
+            port_expr_refs,
+            &protocol_arg_symbols,
+            st,
+        );
+
+        let proto_choice_width = if used_protocol_names.len() <= 1 {
+            1
+        } else {
+            usize::BITS - (used_protocol_names.len() - 1).leading_zeros()
+        };
+        let mut transition_sim = Interpreter::new(&res.ctx, &res.ts);
+        transition_sim.init(InitKind::Zero);
+        let mut waveform = FxHashMap::default();
+        let mut transaction_idx = 0;
+
+        loop {
+            let at_fork = transition_sim
+                .get(res.fork_ready)
+                .try_into_u64()
+                .expect("fork ready failed")
+                == 1;
+            if at_fork {
+                if transaction_idx == trace.len() {
+                    print_trace_success(trace_index);
+                    break;
+                }
+
+                let (proto_name, values) = &trace[transaction_idx];
+                let proto = *protos_by_name.get(proto_name).unwrap();
+                for (arg_expr, value) in proto
+                    .args
+                    .iter()
+                    .map(|arg| res.protocol_inputs[&(0, arg.symbol())])
+                    .zip(values)
+                {
+                    let value: BitVecValue = value.clone().try_into().expect("value not in bitvec");
+                    transition_sim.set(arg_expr, &value);
+                }
+                transition_sim.set(
+                    res.protocol_choices[0],
+                    &BitVecValue::from_u64(
+                        protocol_choice_indices[proto_name.as_str()],
+                        proto_choice_width,
+                    ),
+                );
+                transaction_idx += 1;
+            }
+
+            record_transition_waveform(
+                &mut waveform,
+                &transition_sim,
+                &sim,
+                &res.port_to_expr,
+                &res.is_dont_care,
+            );
+            transition_sim.step();
+
+            let state = transition_sim.get(res.node_symbol);
+            if state == transition_sim.get(res.external_assert_state) {
+                println!(
+                    "Assertion failure while executing transaction {}.",
+                    transaction_idx - 1
+                );
+                break;
+            }
+            if state == transition_sim.get(res.internal_assert_state) {
+                println!(
+                    "Internal assertion failure while executing transaction {}.",
+                    transaction_idx - 1
+                );
+                break;
+            }
+        }
+
+        if cli.ascii_waveform {
+            print_ascii_waveform(
+                waveform,
+                |port| sim.port_name(port).to_string(),
+                |port| sim.port_width(port),
+                false,
+            );
+        }
+    }
+}
+
 fn main() {
     let cli = Cli::parse();
     let (st, modules) = load_protocols(&cli);
@@ -512,7 +652,9 @@ fn main() {
     // let old_hook = std::panic::take_hook();
     // std::panic::set_hook(Box::new(|_| {}));
     let _result = catch_unwind(AssertUnwindSafe(|| {
-        if cli.bound > 0 {
+        if cli.steady_state {
+            run_steady_state(&cli, &st, &module, &traces);
+        } else if cli.bound > 0 {
             run_bmc(&cli, &st, &module, &traces);
         } else if cli.transition_system {
             run_transition_system(&cli, &st, &module, &traces);
diff --git a/protocols/src/backends/transition_system.rs b/protocols/src/backends/transition_system.rs
index 705cdb1c..79d6a199 100644
--- a/protocols/src/backends/transition_system.rs
+++ b/protocols/src/backends/transition_system.rs
@@ -187,6 +187,229 @@ pub struct CoreLoweredSystem {
     pub reachable_nodes: Vec<NodeId>,
 }
 
+pub struct LoweredMonitorSystem {
+    pub ctx: Context,
+    pub ts: TransitionSystem,
+    pub inputs: FxHashMap<SymbolId, ExprRef>,
+    pub node_symbol: ExprRef,
+    pub done_state: ExprRef,
+    pub external_assert_state: ExprRef,
+    pub internal_assert_state: ExprRef,
+}
+
+fn replace_exprs(
+    ctx: &mut Context,
+    expr: ExprRef,
+    substitutions: &FxHashMap<ExprRef, ExprRef>,
+) -> ExprRef {
+    simple_transform_expr(ctx, expr, |_ctx, candidate, _children| {
+        substitutions.get(&candidate).copied()
+    })
+}
+
+/// Lower a monitor graph without a DUT transition system.
+///
+/// DUT ports become free inputs. Monitor symbols in `state_init` and the
+/// control node are transition-system state. Node actions are Moore-style:
+/// their updates are substituted into transition and done guards.
+pub fn into_monitor_transition_system(
+    mut pg: ProtoGraph,
+    mut ts: TransitionSystem,
+    st: &SymbolTable,
+) -> LoweredMonitorSystem {
+    let mut ctx = std::mem::take(&mut pg.expr_ctx);
+
+    let mut inputs = FxHashMap::default();
+    let dut_ports: Vec<_> = pg.proto_ctx.dut_pins(st).collect();
+    for symbol in dut_ports {
+        let symbol::Type::BitVec(width) = st[symbol].tpe() else {
+            panic!("monitor DUT ports must be bit-vectors");
+        };
+        let expr = pg.symbol_expr(symbol).unwrap_or_else(|| {
+            let name = st.full_name_from_symbol_id(&symbol);
+            ctx.bv_symbol(&name, width as WidthInt)
+        });
+        pg.cache_symbol_expr(symbol, expr);
+        ts.add_input(&ctx, expr);
+        inputs.insert(symbol, expr);
+    }
+
+    let mut reachable_nodes = Vec::new();
+    let mut seen = FxHashSet::default();
+    let mut worklist = vec![pg.entry];
+    while let Some(node) = worklist.pop() {
+        if !seen.insert(node) {
+            continue;
+        }
+        reachable_nodes.push(node);
+        worklist.extend(
+            pg[node]
+                .transitions
+                .iter()
+                .map(|transition| transition.target),
+        );
+    }
+
+    let monitor_states: Vec<_> = pg
+        .state_init
+        .iter()
+        .filter_map(|(&symbol, &init)| {
+            let expr = pg.symbol_expr(symbol)?;
+            Some((symbol, expr, init))
+        })
+        .collect();
+
+    // Compute each node's simultaneous monitor-state updates. Missing or
+    // untriggered assignments hold the current value.
+    let mut node_updates: FxHashMap<NodeId, FxHashMap<ExprRef, ExprRef>> = FxHashMap::default();
+    for &node in &reachable_nodes {
+        let mut updates: FxHashMap<ExprRef, ExprRef> = monitor_states
+            .iter()
+            .map(|(_, expr, _)| (*expr, *expr))
+            .collect();
+        for action in &pg[node].actions {
+            let Op::Assign(symbol, assignment) = pg[action.op].clone() else {
+                continue;
+            };
+            if !pg.state_init.contains_key(&symbol) {
+                continue;
+            }
+            let Some(state_expr) = pg.symbol_expr(symbol) else {
+                continue;
+            };
+            let prior = updates[&state_expr];
+            let assignment = Assignment {
+                dont_care: replace_exprs(&mut ctx, assignment.dont_care, &updates),
+                concretes: assignment
+                    .concretes
+                    .into_iter()
+                    .map(|(guard, rhs)| {
+                        (
+                            replace_exprs(&mut ctx, guard, &updates),
+                            replace_exprs(&mut ctx, rhs, &updates),
+                        )
+                    })
+                    .collect(),
+            };
+            let action_guard = replace_exprs(&mut ctx, action.guard, &updates);
+            let assigned = assignment_to_ite(assignment, &mut ctx, prior, prior);
+            let updated = ctx.ite(action_guard, assigned, prior);
+            updates.insert(state_expr, updated);
+        }
+        node_updates.insert(node, updates);
+    }
+
+    let node_count = pg.nodes().try_len().unwrap() as u64 + 2;
+    let node_id_width = u64::from(u64::BITS - node_count.leading_zeros());
+    let node_sym = ctx.bv_symbol("node", node_id_width as WidthInt);
+    let entry_id = ctx.bit_vec_val(pg.entry.as_u32(), node_id_width);
+    let external_bad_state_id = ctx.bit_vec_val(pg.next_node_id().as_u32(), node_id_width);
+    let internal_bad_state_id = ctx.bit_vec_val(pg.next_node_id().as_u32() + 1, node_id_width);
+
+    let mut control_transitions = Vec::new();
+    let mut done_next = ctx.get_false();
+    for &node in &reachable_nodes {
+        let node_id = ctx.bit_vec_val(node.as_u32(), node_id_width);
+        let node_guard = ctx.equal(node_sym, node_id);
+        let updates = &node_updates[&node];
+
+        for transition in &pg[node].transitions {
+            let guard = replace_exprs(&mut ctx, transition.guard, updates);
+            let guard = ctx.and(node_guard, guard);
+            control_transitions.push(IfThenExpr {
+                if_cond: guard,
+                then: ctx.bit_vec_val(transition.target.as_u32(), node_id_width),
+            });
+        }
+
+        for action in &pg[node].actions {
+            let action_guard = replace_exprs(&mut ctx, action.guard, updates);
+            let action_guard = ctx.and(node_guard, action_guard);
+            match pg[action.op].clone() {
+                Op::Done => done_next = ctx.or(done_next, action_guard),
+                Op::AssertEq(lhs, rhs) => {
+                    let lhs = replace_exprs(&mut ctx, lhs, updates);
+                    let rhs = replace_exprs(&mut ctx, rhs, updates);
+                    let equal = ctx.equal(lhs, rhs);
+                    let failed = ctx.not(equal);
+                    let failed = ctx.and(action_guard, failed);
+                    control_transitions.push(IfThenExpr {
+                        if_cond: failed,
+                        then: external_bad_state_id,
+                    });
+                }
+                Op::InternalAssertFalse => control_transitions.push(IfThenExpr {
+                    if_cond: action_guard,
+                    then: internal_bad_state_id,
+                }),
+                Op::Assign(_, _) | Op::Fork => {}
+            }
+        }
+    }
+
+    let external_bad_guard = ctx.equal(node_sym, external_bad_state_id);
+    control_transitions.push(IfThenExpr {
+        if_cond: external_bad_guard,
+        then: external_bad_state_id,
+    });
+    let internal_bad_guard = ctx.equal(node_sym, internal_bad_state_id);
+    control_transitions.push(IfThenExpr {
+        if_cond: internal_bad_guard,
+        then: internal_bad_state_id,
+    });
+    let control_next = if_thens_to_ite(control_transitions, &mut ctx, internal_bad_state_id);
+    ts.add_state(
+        &ctx,
+        State {
+            symbol: node_sym,
+            init: Some(entry_id),
+            next: Some(control_next),
+        },
+    );
+    ts.bad_states
+        .push(ctx.equal(node_sym, external_bad_state_id));
+    ts.bad_states
+        .push(ctx.equal(node_sym, internal_bad_state_id));
+
+    for (_, state_expr, init) in monitor_states {
+        let mut next = state_expr;
+        for &node in &reachable_nodes {
+            let node_id = ctx.bit_vec_val(node.as_u32(), node_id_width);
+            let node_guard = ctx.equal(node_sym, node_id);
+            next = ctx.ite(node_guard, node_updates[&node][&state_expr], next);
+        }
+        ts.add_state(
+            &ctx,
+            State {
+                symbol: state_expr,
+                init: Some(init),
+                next: Some(next),
+            },
+        );
+    }
+
+    let done_state = ctx.bv_symbol("monitor.done", 1);
+    ts.add_state(
+        &ctx,
+        State {
+            symbol: done_state,
+            init: Some(ctx.get_false()),
+            next: Some(done_next),
+        },
+    );
+    ts.add_output(&mut ctx, Cow::Borrowed("done"), done_state);
+
+    LoweredMonitorSystem {
+        ctx,
+        ts,
+        inputs,
+        node_symbol: node_sym,
+        done_state,
+        external_assert_state: external_bad_state_id,
+        internal_assert_state: internal_bad_state_id,
+    }
+}
+
 pub fn lower_proto_graph_to_transition_system(
     mut pg: ProtoGraph,
     mut ctx: Context,
@@ -455,3 +678,180 @@ pub fn into_transition_system(
         is_dont_care: core.is_dont_care,
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::frontend::diagnostic::DiagnosticHandler;
+    use crate::frontend::{frontend, require_single_module};
+    use crate::interpreter::Value as WaveValue;
+    use crate::ir::to_monitor::to_monitor;
+    use crate::scheduler::Scheduler;
+    use crate::{PatronusSim, transaction_frontend};
+    use baa::BitVecValue;
+    use patronus::sim::{InitKind, Interpreter, Simulator};
+    use std::fs;
+    use tempfile::NamedTempFile;
+
+    #[test]
+    fn standalone_monitor_system_reads_ports_and_updates_monitor_state() {
+        let file = NamedTempFile::new().unwrap();
+        fs::write(
+            file.path(),
+            r#"
+            struct Dut {
+                in req: u1,
+                out ack: u1,
+                out echo: u1,
+            }
+
+            prot request<dut: Dut>(value: u1) {
+                dut.req := value;
+                assert_eq(dut.echo, value);
+                while dut.ack == 1'b0 {
+                    step();
+                }
+                step();
+            }
+            "#,
+        )
+        .unwrap();
+        let mut diagnostics = DiagnosticHandler::default();
+        let (mut symbols, modules) = frontend(&[file.path()], &mut diagnostics, true).unwrap();
+        let module = require_single_module(modules, &[file.path()]).unwrap();
+        let monitor = to_monitor(module.protos, &mut symbols, Context::default()).unwrap();
+
+        let ts = TransitionSystem::new("protocol_monitor".to_string());
+
+        let lowered = into_monitor_transition_system(monitor, ts, &symbols);
+
+        assert_eq!(lowered.inputs.len(), 3);
+        assert_eq!(lowered.ts.inputs.len(), 3);
+        assert_eq!(lowered.ts.bad_states.len(), 2);
+        assert_eq!(lowered.ts.outputs.len(), 1);
+
+        let req = lowered
+            .inputs
+            .iter()
+            .find_map(|(symbol, expr)| (symbols[*symbol].name() == "req").then_some(*expr))
+            .unwrap();
+        let ack = lowered
+            .inputs
+            .iter()
+            .find_map(|(symbol, expr)| (symbols[*symbol].name() == "ack").then_some(*expr))
+            .unwrap();
+        let echo = lowered
+            .inputs
+            .iter()
+            .find_map(|(symbol, expr)| (symbols[*symbol].name() == "echo").then_some(*expr))
+            .unwrap();
+
+        let mut sim = Interpreter::new(&lowered.ctx, &lowered.ts);
+        sim.init(InitKind::Zero);
+        sim.set(req, &BitVecValue::from_u64(1, 1));
+        sim.set(echo, &BitVecValue::from_u64(1, 1));
+        sim.set(ack, &BitVecValue::from_u64(0, 1));
+        sim.step();
+        assert!(sim.get(lowered.done_state).try_into_u64().unwrap() == 0);
+
+        sim.set(ack, &BitVecValue::from_u64(1, 1));
+        sim.step();
+        assert!(sim.get(lowered.done_state).try_into_u64().unwrap() == 1);
+    }
+
+    fn monitor_accepts_waveform(
+        lowered: &LoweredMonitorSystem,
+        symbols: &SymbolTable,
+        waveform: &FxHashMap<String, Vec<WaveValue>>,
+    ) -> bool {
+        let cycle_count = waveform.values().map(Vec::len).max().unwrap_or(0);
+        let mut sim = Interpreter::new(&lowered.ctx, &lowered.ts);
+        sim.init(InitKind::Zero);
+
+        for cycle in 0..cycle_count {
+            for (&symbol, &input) in &lowered.inputs {
+                let name = symbols[symbol].name();
+                let width = match symbols[symbol].tpe() {
+                    symbol::Type::BitVec(width) => width,
+                    _ => unreachable!("monitor ports must be bit-vectors"),
+                };
+                let value = match &waveform[name][cycle] {
+                    WaveValue::Concrete(value) => value.clone(),
+                    WaveValue::DontCare => BitVecValue::from_u64(0, width),
+                };
+                sim.set(input, &value);
+            }
+            sim.step();
+            let node = sim.get(lowered.node_symbol);
+            if node == sim.get(lowered.external_assert_state)
+                || node == sim.get(lowered.internal_assert_state)
+            {
+                return false;
+            }
+        }
+
+        sim.get(lowered.done_state).try_into_u64().unwrap() == 1
+    }
+
+    #[test]
+    #[ignore = "requires yosys to execute the Wishbone RTL"]
+    fn generated_wishbone_waveform_is_accepted_and_mutation_is_rejected() {
+        let root = std::path::Path::new(env!("CARGO_MANIFEST_DIR"))
+            .parent()
+            .unwrap();
+        let protocol_file = root.join("examples/wishbone/wishbone.prot");
+        let trace_file = root.join("examples/wishbone/read_write.tx");
+        let dut_file = root.join("examples/wishbone/rtl/dut.v");
+        let tb_file = root.join("examples/wishbone/rtl/tb.v");
+
+        let mut diagnostics = DiagnosticHandler::default();
+        let (mut symbols, modules) = frontend(&[&protocol_file], &mut diagnostics, true).unwrap();
+        let module = require_single_module(modules, &[&protocol_file]).unwrap();
+        let traces =
+            transaction_frontend(&trace_file, &symbols, &module.protos, &mut diagnostics).unwrap();
+        let trace = traces[0].clone();
+        let selected_names: FxHashSet<_> = trace.iter().map(|(name, _)| name.as_str()).collect();
+        let selected = module
+            .protos
+            .iter()
+            .filter(|protocol| selected_names.contains(protocol.name.as_str()))
+            .cloned()
+            .collect();
+
+        let temp = tempfile::tempdir().unwrap();
+        let fst = temp.path().join("read_write.fst");
+        let sim = PatronusSim::new(
+            &[dut_file, tb_file],
+            Some("tb"),
+            &module,
+            Some(fst.to_str().unwrap()),
+        )
+        .unwrap();
+        let mut scheduler = Scheduler::new(
+            &symbols,
+            &module.protos,
+            trace,
+            sim,
+            &mut diagnostics,
+            u32::MAX,
+        );
+        assert!(scheduler.execute_transactions().iter().all(Result::is_ok));
+        let raw_waveform = scheduler.waveform();
+        let mut waveform: FxHashMap<_, _> = raw_waveform
+            .into_iter()
+            .map(|(port, values)| (scheduler.port_name(port).to_string(), values))
+            .collect();
+        drop(scheduler);
+        assert!(std::fs::metadata(fst).unwrap().len() > 0);
+
+        let monitor = to_monitor(selected, &mut symbols, Context::default()).unwrap();
+
+        let ts = TransitionSystem::new("protocol_monitor".to_string());
+        let lowered = into_monitor_transition_system(monitor, ts, &symbols);
+        assert!(monitor_accepts_waveform(&lowered, &symbols, &waveform));
+
+        // RST=1 and CYC=1 cannot be reset, idle, read, or write.
+        waveform.get_mut("CYC").unwrap()[0] = WaveValue::Concrete(BitVecValue::from_u64(1, 1));
+        assert!(!monitor_accepts_waveform(&lowered, &symbols, &waveform));
+    }
+}
diff --git a/protocols/src/frontend/remap.rs b/protocols/src/frontend/remap.rs
index 3fa67235..248537d2 100644
--- a/protocols/src/frontend/remap.rs
+++ b/protocols/src/frontend/remap.rs
@@ -361,6 +361,9 @@ impl Remapper<'_> {
                             .unwrap_or_else(|| unreachable!("{name} should have been declared!"));
                         self.out.e(Expr::Sym(out_sym))
                     }
+                    SymbolKind::MonitorState => {
+                        unreachable!("monitor state is not part of frontend remapping")
+                    }
                 }
             }
             Expr::DontCare => self.out.dont_care_id(),
diff --git a/protocols/src/frontend/symbol.rs b/protocols/src/frontend/symbol.rs
index 0ff97fe1..a3336b8b 100644
--- a/protocols/src/frontend/symbol.rs
+++ b/protocols/src/frontend/symbol.rs
@@ -53,6 +53,9 @@ pub enum SymbolKind {
     OutPort,
     Arg(u16),
     LoopVar,
+    /// State introduced by an IR-to-IR transformation, such as protocol
+    /// argument knownness in a generated monitor.
+    MonitorState,
 }
 
 #[derive(Clone, Copy, Hash, PartialEq, Eq, Default)]
@@ -596,4 +599,8 @@ impl SymbolTableEntry {
     pub fn is_loop_var(&self) -> bool {
         matches!(self.kind, SymbolKind::LoopVar)
     }
+
+    pub fn is_monitor_state(&self) -> bool {
+        matches!(self.kind, SymbolKind::MonitorState)
+    }
 }
diff --git a/protocols/src/interpreter.rs b/protocols/src/interpreter.rs
index 3c8658f1..15664e42 100644
--- a/protocols/src/interpreter.rs
+++ b/protocols/src/interpreter.rs
@@ -523,6 +523,9 @@ impl<'a> Evaluator<'a> {
                             .unwrap();
                         Ok(ExprValue::Concrete(value.clone()))
                     }
+                    SymbolKind::MonitorState => {
+                        unreachable!("monitor state is not part of AST interpretation")
+                    }
                 }
             }
             Expr::DontCare => Ok(ExprValue::DontCare),
@@ -741,6 +744,9 @@ impl<'a> Evaluator<'a> {
                 "loop_var".to_string(),
                 stmt_id,
             )),
+            SymbolKind::MonitorState => {
+                unreachable!("monitor state is not part of AST interpretation")
+            }
         }
     }
 
diff --git a/protocols/src/ir/bounded_lowering.rs b/protocols/src/ir/bounded_lowering.rs
index 7a538a41..20905922 100644
--- a/protocols/src/ir/bounded_lowering.rs
+++ b/protocols/src/ir/bounded_lowering.rs
@@ -5,7 +5,7 @@ use crate::ir::proto_graph::{Action, NodeId, Op, ProtoGraph};
 use patronus::expr::{Context as ExprContext, ExprRef, TypeCheck};
 use rustc_hash::FxHashMap;
 
-fn mark_graft_point_ready(lowerer: &mut Lowerer<'_>, node: NodeId, guard: ExprRef) {
+pub fn mark_graft_point_ready(lowerer: &mut Lowerer<'_>, node: NodeId, guard: ExprRef) {
     let already_ready = lowerer.ir[node]
         .actions
         .iter()
@@ -16,7 +16,7 @@ fn mark_graft_point_ready(lowerer: &mut Lowerer<'_>, node: NodeId, guard: ExprRe
     }
 }
 
-fn graft_choice_entries_into(
+pub fn graft_choice_entries_into(
     lowerer: &mut Lowerer<'_>,
     parent: NodeId,
     choices: Vec<(NodeId, ExprRef)>,
diff --git a/protocols/src/ir/determinize.rs b/protocols/src/ir/determinize.rs
index bde4775e..c4403e95 100644
--- a/protocols/src/ir/determinize.rs
+++ b/protocols/src/ir/determinize.rs
@@ -8,8 +8,8 @@ use crate::frontend::symbol::SymbolTable;
 use crate::ir::edge_contract::append_action;
 use crate::ir::proto_graph::{Node as NFANode, NodeId, ProtoGraph, Transition};
 use cranelift_entity::PrimaryMap;
-use patronus::expr::ExprRef;
-use rustc_hash::FxHashMap;
+use patronus::expr::{Expr, ExprRef, TypeCheck, simple_transform_expr};
+use rustc_hash::{FxHashMap, FxHashSet};
 
 /// A DFA Node is a set of NFA nodes active at the same time.
 type DFANode = BTreeSet<NodeId>;
@@ -39,6 +39,68 @@ pub enum SatResult {
     AlwaysSat,
 }
 
+fn collect_boolean_atoms(protocol: &ProtoGraph, expr: ExprRef, atoms: &mut FxHashSet<ExprRef>) {
+    if expr == protocol.true_id() || expr == protocol.false_id() {
+        return;
+    }
+    match protocol.expr_ctx[expr] {
+        Expr::BVAnd(lhs, rhs, 1) | Expr::BVOr(lhs, rhs, 1) => {
+            collect_boolean_atoms(protocol, lhs, atoms);
+            collect_boolean_atoms(protocol, rhs, atoms);
+        }
+        Expr::BVNot(inner, 1) => collect_boolean_atoms(protocol, inner, atoms),
+        _ => {
+            atoms.insert(expr);
+        }
+    }
+}
+
+fn eval_boolean_skeleton(
+    protocol: &ProtoGraph,
+    expr: ExprRef,
+    values: &FxHashMap<ExprRef, bool>,
+) -> bool {
+    if expr == protocol.true_id() {
+        return true;
+    }
+    if expr == protocol.false_id() {
+        return false;
+    }
+    match protocol.expr_ctx[expr] {
+        Expr::BVAnd(lhs, rhs, 1) => {
+            eval_boolean_skeleton(protocol, lhs, values)
+                && eval_boolean_skeleton(protocol, rhs, values)
+        }
+        Expr::BVOr(lhs, rhs, 1) => {
+            eval_boolean_skeleton(protocol, lhs, values)
+                || eval_boolean_skeleton(protocol, rhs, values)
+        }
+        Expr::BVNot(inner, 1) => !eval_boolean_skeleton(protocol, inner, values),
+        _ => values[&expr],
+    }
+}
+
+fn propositionally_unsat(protocol: &ProtoGraph, expr: ExprRef) -> bool {
+    let mut atoms = FxHashSet::default();
+    collect_boolean_atoms(protocol, expr, &mut atoms);
+    // Keep this lightweight. Falling back to MaybeSat is always sound.
+    if atoms.len() > 16 {
+        return false;
+    }
+    let atoms: Vec<_> = atoms.into_iter().collect();
+    for mask in 0usize..(1usize << atoms.len()) {
+        let values = atoms
+            .iter()
+            .enumerate()
+            .map(|(index, atom)| (*atom, (mask >> index) & 1 == 1))
+            .collect();
+        if eval_boolean_skeleton(protocol, expr, &values) {
+            return false;
+        }
+    }
+    true
+}
+
 // TODO: Strengthen this with a real SAT/SMT query to prune more aggressively.
 pub fn check_sat(protocol: &mut ProtoGraph, guard: ExprRef) -> SatResult {
     let simplified = {
@@ -50,11 +112,92 @@ pub fn check_sat(protocol: &mut ProtoGraph, guard: ExprRef) -> SatResult {
         SatResult::DefinitelyUnsat
     } else if simplified == protocol.true_id() {
         SatResult::AlwaysSat
+    } else if propositionally_unsat(protocol, simplified) {
+        SatResult::DefinitelyUnsat
     } else {
-        SatResult::MaybeSat
+        let negated = protocol.not_guard(simplified);
+        if propositionally_unsat(protocol, negated) {
+            SatResult::AlwaysSat
+        } else {
+            SatResult::MaybeSat
+        }
     }
 }
 
+fn transition_guards_after_node_updates(
+    protocol: &mut ProtoGraph,
+    actions: &[crate::ir::proto_graph::Action],
+    transitions: &[Transition],
+) -> Vec<ExprRef> {
+    let mut substitutions = FxHashMap::default();
+
+    for action in actions {
+        let crate::ir::proto_graph::Op::Assign(symbol, assignment) = protocol[action.op].clone()
+        else {
+            continue;
+        };
+        if !protocol.state_init.contains_key(&symbol) || assignment.dont_care != protocol.false_id()
+        {
+            continue;
+        }
+        let Some(lhs) = protocol.symbol_expr(symbol) else {
+            continue;
+        };
+        let prior = substitutions.get(&lhs).copied().unwrap_or(lhs);
+        let action_guard = simple_transform_expr(
+            &mut protocol.expr_ctx,
+            action.guard,
+            |_ctx, candidate, _children| substitutions.get(&candidate).copied(),
+        );
+        let branches: Vec<_> = assignment
+            .concretes
+            .iter()
+            .map(|(guard, rhs)| {
+                (
+                    simple_transform_expr(
+                        &mut protocol.expr_ctx,
+                        *guard,
+                        |_ctx, candidate, _children| substitutions.get(&candidate).copied(),
+                    ),
+                    simple_transform_expr(
+                        &mut protocol.expr_ctx,
+                        *rhs,
+                        |_ctx, candidate, _children| substitutions.get(&candidate).copied(),
+                    ),
+                )
+            })
+            .collect();
+
+        // Assignment branches use first-match priority. If no branch fires,
+        // monitor state holds its old value.
+        let mut next = prior;
+        for (branch_guard, rhs) in branches.into_iter().rev() {
+            let guard = protocol.and_guard(action_guard, branch_guard);
+            next = if lhs.is_bool(&protocol.expr_ctx) {
+                let when_set = protocol.and_guard(guard, rhs);
+                let not_guard = protocol.not_guard(guard);
+                let when_held = protocol.and_guard(not_guard, next);
+                protocol.or_guard(when_set, when_held)
+            } else {
+                protocol.expr_ctx.ite(guard, rhs, next)
+            };
+        }
+        substitutions.insert(lhs, next);
+    }
+
+    transitions
+        .iter()
+        .map(|transition| {
+            let guard = simple_transform_expr(
+                &mut protocol.expr_ctx,
+                transition.guard,
+                |_ctx, candidate, _children| substitutions.get(&candidate).copied(),
+            );
+            protocol.simplifier.simplify(&mut protocol.expr_ctx, guard)
+        })
+        .collect()
+}
+
 /// Perform subset construction.
 pub fn determinized(protocol: ProtoGraph, symbols: &SymbolTable) -> ProtoGraph {
     let mut protocol = protocol.clone();
@@ -93,13 +236,52 @@ pub fn determinized(protocol: ProtoGraph, symbols: &SymbolTable) -> ProtoGraph {
             ));
         }
 
+        // The DFA successor only records which NFA target nodes are active,
+        // not which of several parallel edges activated each target. Collapse
+        // those parallel edges before enumerating subsets. Otherwise every
+        // equivalent edge selection becomes a separate minterm which is later
+        // ORed back together into a very large expression.
+        let mut grouped: Vec<Transition> = Vec::new();
+        for transition in transitions {
+            if let Some(existing) = grouped
+                .iter_mut()
+                .find(|existing| existing.target == transition.target)
+            {
+                existing.guard = protocol.or_guard(existing.guard, transition.guard);
+            } else {
+                grouped.push(transition);
+            }
+        }
+        let transitions = grouped;
+
+        if let Some(first) = transitions.first()
+            && transitions
+                .iter()
+                .all(|transition| transition.target == first.target)
+        {
+            let guard = transitions
+                .iter()
+                .fold(protocol.false_id(), |guard, transition| {
+                    protocol.or_guard(guard, transition.guard)
+                });
+            let target = BTreeSet::from([first.target]);
+            let target_id =
+                get_or_create_state(target, &mut state_ids, &mut worklist, &mut new_nodes);
+            new_nodes[this_id] = NFANode {
+                actions,
+                transitions: vec![Transition::new(guard, target_id, true)],
+            };
+            continue;
+        }
+
         let mut new_trans: Vec<Transition> = Vec::new();
         let n = transitions.len();
-        let transition_guards: Vec<_> = transitions.iter().map(|t| t.guard).collect();
+        let analysis_guards =
+            transition_guards_after_node_updates(&mut protocol, &actions, &transitions);
         let mut mutually_exclusive = vec![vec![false; n]; n];
         for i in 0..n {
             for j in (i + 1)..n {
-                let overlap = protocol.and_guard(transition_guards[i], transition_guards[j]);
+                let overlap = protocol.and_guard(analysis_guards[i], analysis_guards[j]);
                 let disjoint = matches!(
                     check_sat(&mut protocol, overlap),
                     SatResult::DefinitelyUnsat
@@ -114,31 +296,40 @@ pub fn determinized(protocol: ProtoGraph, symbols: &SymbolTable) -> ProtoGraph {
         assert!(n <= 128);
         for mask in 1u128..(1u128 << n) {
             let mut guard = protocol.true_id();
+            let mut analysis_guard = protocol.true_id();
             let mut targets: DFANode = BTreeSet::new();
             for (i, t) in transitions.iter().enumerate() {
                 let selected = (mask >> i) & 1 == 1;
-                let lit = if selected {
+                let (lit, analysis_lit) = if selected {
                     targets.insert(t.target);
-                    t.guard
+                    (t.guard, analysis_guards[i])
                 } else if (0..n).any(|j| (mask >> j) & 1 == 1 && mutually_exclusive[i][j]) {
                     // A selected transition already implies that this guard is
                     // false, so its negation would only add expression noise.
                     continue;
                 } else {
-                    protocol.not_guard(t.guard)
+                    (
+                        protocol.not_guard(t.guard),
+                        protocol.not_guard(analysis_guards[i]),
+                    )
                 };
                 guard = protocol.and_guard(guard, lit);
+                analysis_guard = protocol.and_guard(analysis_guard, analysis_lit);
             }
 
-            let guard = match check_sat(&mut protocol, guard) {
+            match check_sat(&mut protocol, analysis_guard) {
                 SatResult::DefinitelyUnsat => continue,
-                SatResult::AlwaysSat => protocol.true_id(),
-                SatResult::MaybeSat => guard,
-            };
+                SatResult::AlwaysSat | SatResult::MaybeSat => {}
+            }
 
+            let target_id =
+                get_or_create_state(targets, &mut state_ids, &mut worklist, &mut new_nodes);
+            if let Some(existing) = new_trans
+                .iter_mut()
+                .find(|transition| transition.target == target_id && transition.consumes_step)
             {
-                let target_id =
-                    get_or_create_state(targets, &mut state_ids, &mut worklist, &mut new_nodes);
+                existing.guard = protocol.or_guard(existing.guard, guard);
+            } else {
                 new_trans.push(Transition::new(guard, target_id, true));
             }
         }
diff --git a/protocols/src/ir/mod.rs b/protocols/src/ir/mod.rs
index b500f2d5..f1909f64 100644
--- a/protocols/src/ir/mod.rs
+++ b/protocols/src/ir/mod.rs
@@ -8,6 +8,8 @@ pub mod lowering;
 pub mod propagate_assigns;
 pub mod proto_graph;
 pub mod reaching_defs;
+pub mod steady_state_lowering;
+pub mod to_monitor;
 pub mod trace_lowering;
 // TODO: add a function to transform AST to IR
 // pub fn frontend(
diff --git a/protocols/src/ir/proto_graph.rs b/protocols/src/ir/proto_graph.rs
index a2b23a92..026ae8ef 100644
--- a/protocols/src/ir/proto_graph.rs
+++ b/protocols/src/ir/proto_graph.rs
@@ -145,6 +145,14 @@ pub struct ProtoGraph {
     /// symbol expressions representing DontCare
     pub dont_cares: FxHashSet<ExprRef>,
 
+    /// Symbols that are state in this graph and their initial values.
+    ///
+    /// This is populated by IR-to-IR transformations such as `to_monitor`.
+    /// Keeping the declaration on the graph lets `Op::Assign` represent both
+    /// DUT driving assignments in a driver graph and state updates in a
+    /// monitor graph without adding another operation kind.
+    pub state_init: FxHashMap<SymbolId, ExprRef>,
+
     nodes: PrimaryMap<NodeId, Node>,
 
     ops: PrimaryMap<OpId, Op>,
@@ -163,6 +171,7 @@ impl Clone for ProtoGraph {
             simplifier: Simplifier::new(SparseExprMap::default()),
             symbol_expr: self.symbol_expr.clone(),
             dont_cares: self.dont_cares.clone(),
+            state_init: self.state_init.clone(),
             nodes: self.nodes.clone(),
             ops: self.ops.clone(),
             op_loc: self.op_loc.clone(),
@@ -190,6 +199,7 @@ impl ProtoGraph {
             simplifier: Simplifier::new(SparseExprMap::default()),
             symbol_expr: FxHashMap::default(),
             dont_cares: FxHashSet::default(),
+            state_init: FxHashMap::default(),
             nodes,
             ops,
             op_loc,
diff --git a/protocols/src/ir/steady_state_lowering.rs b/protocols/src/ir/steady_state_lowering.rs
new file mode 100644
index 00000000..89665ec7
--- /dev/null
+++ b/protocols/src/ir/steady_state_lowering.rs
@@ -0,0 +1,109 @@
+use crate::frontend::ast::Protocol;
+use crate::frontend::symbol::{SymbolId, SymbolKind, SymbolTable};
+use crate::ir::bounded_lowering::graft_choice_entries_into;
+use crate::ir::lowering::{LoweredFragmentInfo, Lowerer};
+use crate::ir::proto_graph::{Action, NodeId, Op, ProtoGraph};
+use patronus::expr::{Context as ExprContext, ExprRef, TypeCheck};
+use rustc_hash::FxHashMap;
+
+fn loop_exit_to_entry(lowerer: &mut Lowerer<'_>, fragment: &LoweredFragmentInfo, entry: NodeId) {
+    for node in fragment.nodes.iter().copied() {
+        if node == fragment.exit {
+            continue;
+        }
+
+        for transition in &mut lowerer.ir.node_mut(node).transitions {
+            if transition.target == fragment.exit {
+                transition.target = entry;
+                transition.consumes_step = true;
+            }
+        }
+    }
+}
+
+/// Lower a set of protocols to a joint IR that represents traces of any length
+/// Precondition: every `p \in protos` must fork in its exit node (there is no possibility of
+/// overlapping protcols)
+pub fn lower_steady_state(
+    protos: Vec<Protocol>,
+    symbols: &SymbolTable,
+    mut expr_ctx: ExprContext,
+) -> (ProtoGraph, ExprRef) {
+    assert!(!protos.is_empty());
+    let num_protos = protos.len();
+    let width = if num_protos <= 1 {
+        1
+    } else {
+        usize::BITS - (num_protos - 1).leading_zeros()
+    };
+    let proto_choice: ExprRef = expr_ctx.bv_symbol(&"proto_choice".to_string(), width);
+
+    let first_ast = protos.first().unwrap();
+
+    // set up the lowerer and lower all the protocols
+    let mut lowerer = Lowerer::with_expr_ctx(first_ast.ctx.clone(), symbols, expr_ctx);
+    // TODO: Handle done vs not done
+    let mut lowered_protocols: Vec<LoweredFragmentInfo> = vec![];
+    for protocol in protos {
+        let mut pg = lowerer.lower_protocol_fragment(&protocol, false, true);
+        // lowerer.postprocess_trace_fragment(&pg);
+        pg.graft_points = lowerer.graft_points(&pg);
+        lowered_protocols.push(pg);
+    }
+
+    let arg_symbols: Vec<SymbolId> = lowerer
+        .symbols
+        .get_args()
+        .into_iter()
+        .filter(|symbol_id| {
+            matches!(lowerer.symbols[*symbol_id].kind(), SymbolKind::Arg(_))
+                && lowerer.ir.symbol_expr(*symbol_id).is_some()
+        })
+        .collect();
+
+    // The steady-state automaton has one reusable transaction slot. Use the
+    // same #0 argument names that `into_bmc_transition_system` creates for its
+    // first slot so the copied graph reads those transition-system inputs.
+    let instance_substitutions: FxHashMap<ExprRef, ExprRef> = arg_symbols
+        .iter()
+        .filter_map(|symbol_id| {
+            let old_expr = lowerer.ir.symbol_expr(*symbol_id)?;
+            let width = old_expr.get_bv_type(&lowerer.ir.expr_ctx)?;
+            let name = lowerer.symbols.full_name_from_symbol_id(symbol_id);
+            let slot_expr = lowerer.ir.expr_ctx.bv_symbol(&format!("{name}#0"), width);
+            Some((old_expr, slot_expr))
+        })
+        .collect();
+
+    let entry_node = lowerer.ir.entry;
+    // the entry node is a fork point (where we start new transactions)
+    let fork_op = lowerer.ir.o(Op::Fork);
+    lowerer
+        .ir
+        .push_action(entry_node, Action::new(lowerer.ir.true_id(), fork_op));
+
+    let mut initial_choices = Vec::with_capacity(num_protos);
+    for (idx, prototype) in lowered_protocols.iter().enumerate().take(num_protos) {
+        let proto_idx_expr = lowerer.ir.expr_ctx.bit_vec_val(idx, width);
+        let node_equals = if idx + 1 == num_protos {
+            lowerer
+                .ir
+                .expr_ctx
+                .greater_or_equal(proto_choice, proto_idx_expr)
+        } else {
+            lowerer.ir.expr_ctx.equal(proto_choice, proto_idx_expr)
+        };
+        let new_frag = lowerer.copy_protocol_fragment(prototype.clone(), &instance_substitutions);
+
+        initial_choices.push((new_frag.entry, node_equals));
+
+        loop_exit_to_entry(&mut lowerer, &new_frag, entry_node);
+    }
+    graft_choice_entries_into(&mut lowerer, entry_node, initial_choices);
+
+    // contract_edges(&mut lowerer.ir, lowerer.symbols);
+
+    // pass in the initial IR with and its graft points, and append_trace_transactions will lower the rest of the trace from here.
+    lowerer.ir.simplify_all_exprs();
+    (lowerer.ir, proto_choice)
+}
diff --git a/protocols/src/ir/to_monitor.rs b/protocols/src/ir/to_monitor.rs
new file mode 100644
index 00000000..9a0d082e
--- /dev/null
+++ b/protocols/src/ir/to_monitor.rs
@@ -0,0 +1,947 @@
+use crate::frontend::ast::Protocol;
+use crate::frontend::symbol::{SymbolId, SymbolKind, SymbolTable, Type};
+use crate::ir::determinize::{SatResult, check_sat, determinized};
+use crate::ir::lowering::{LoweredFragmentInfo, Lowerer};
+use crate::ir::proto_graph::{Action, Assignment, NodeId, Op, ProtoGraph};
+use patronus::expr::{Context as ExprContext, ExprRef, simple_transform_expr};
+use rustc_hash::{FxHashMap, FxHashSet};
+use std::collections::VecDeque;
+use thiserror::Error;
+
+#[derive(Debug, Error, PartialEq, Eq)]
+pub enum ToMonitorError {
+    #[error("cannot construct a monitor from an empty protocol set")]
+    EmptyProtocolSet,
+    #[error("monitor parameters must be bit-vectors: {0}")]
+    NonBitVectorParameter(String),
+    #[error("assignment target has no expression in the ProtoGraph: {0:?}")]
+    MissingAssignmentTarget(SymbolId),
+    #[error("monitor lowering does not support fork actions")]
+    UnsupportedFork,
+}
+
+#[derive(Clone)]
+struct ParameterSeed {
+    original: SymbolId,
+    symbol: SymbolId,
+    known_symbol: SymbolId,
+    name: String,
+    known_name: String,
+    width: u32,
+}
+
+#[derive(Clone)]
+struct ProtocolSeed {
+    live_symbol: SymbolId,
+    live_name: String,
+    parameters: Vec<ParameterSeed>,
+}
+
+struct CandidateState {
+    live_symbol: SymbolId,
+    live_expr: ExprRef,
+    parameters: Vec<ParameterState>,
+}
+
+#[derive(Clone, Copy)]
+struct ParameterState {
+    symbol: SymbolId,
+    expr: ExprRef,
+    known_symbol: Option<SymbolId>,
+    known_expr: Option<ExprRef>,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+enum Knownness {
+    Unknown,
+    Known,
+    Maybe,
+}
+
+fn symbol_expr(
+    pg: &mut ProtoGraph,
+    symbols: &SymbolTable,
+    symbol: SymbolId,
+) -> Result<ExprRef, ToMonitorError> {
+    if let Some(expr) = pg.symbol_expr(symbol) {
+        return Ok(expr);
+    }
+    let Type::BitVec(width) = symbols[symbol].tpe() else {
+        return Err(ToMonitorError::MissingAssignmentTarget(symbol));
+    };
+    let name = symbols.full_name_from_symbol_id(&symbol);
+    let expr = pg.expr_ctx.bv_symbol(&name, width);
+    pg.cache_symbol_expr(symbol, expr);
+    Ok(expr)
+}
+
+fn parameters_in_expr(
+    pg: &mut ProtoGraph,
+    expr: ExprRef,
+    by_expr: &FxHashMap<ExprRef, ParameterState>,
+) -> Vec<ParameterState> {
+    let mut found = FxHashSet::default();
+    simple_transform_expr(&mut pg.expr_ctx, expr, |_ctx, candidate, _children| {
+        if by_expr.contains_key(&candidate) {
+            found.insert(candidate);
+        }
+        None
+    });
+    found
+        .into_iter()
+        .map(|candidate| by_expr[&candidate])
+        .collect()
+}
+
+fn join_knownness(lhs: Knownness, rhs: Knownness) -> Knownness {
+    if lhs == rhs { lhs } else { Knownness::Maybe }
+}
+
+fn or_all(pg: &mut ProtoGraph, guards: impl IntoIterator<Item = ExprRef>) -> ExprRef {
+    guards
+        .into_iter()
+        .fold(pg.false_id(), |acc, guard| pg.or_guard(acc, guard))
+}
+
+fn node_equalities(pg: &mut ProtoGraph, node: NodeId) -> Vec<(ExprRef, ExprRef, ExprRef)> {
+    let actions = pg[node].actions.clone();
+    let mut equalities = Vec::new();
+    for action in actions {
+        match pg[action.op].clone() {
+            Op::Assign(symbol, assignment) => {
+                let lhs = pg.symbol_expr(symbol).unwrap();
+                for (guard, rhs) in assignment.concretes {
+                    let guard = pg.and_guard(action.guard, guard);
+                    equalities.push((guard, lhs, rhs));
+                }
+            }
+            Op::AssertEq(lhs, rhs) => equalities.push((action.guard, lhs, rhs)),
+            Op::Fork | Op::InternalAssertFalse | Op::Done => {}
+        }
+    }
+    equalities
+}
+
+fn transfer_knownness(
+    pg: &mut ProtoGraph,
+    node: NodeId,
+    input: &FxHashMap<ExprRef, Knownness>,
+    parameters: &FxHashMap<ExprRef, ParameterState>,
+) -> FxHashMap<ExprRef, Knownness> {
+    let equalities = node_equalities(pg, node);
+    let mut output = input.clone();
+
+    let mut definite: FxHashMap<ExprRef, Vec<ExprRef>> = FxHashMap::default();
+    let mut possible: FxHashMap<ExprRef, Vec<ExprRef>> = FxHashMap::default();
+
+    for (guard, lhs, rhs) in &equalities {
+        for (candidate, other) in [(*lhs, *rhs), (*rhs, *lhs)] {
+            if !parameters.contains_key(&candidate) {
+                continue;
+            }
+            let dependencies = parameters_in_expr(pg, other, parameters);
+            if dependencies
+                .iter()
+                .all(|dependency| input[&dependency.expr] == Knownness::Known)
+            {
+                definite.entry(candidate).or_default().push(*guard);
+            }
+            if dependencies
+                .iter()
+                .all(|dependency| input[&dependency.expr] != Knownness::Unknown)
+            {
+                possible.entry(candidate).or_default().push(*guard);
+            }
+        }
+    }
+
+    for parameter in parameters.values() {
+        let definitely_learned = definite
+            .remove(&parameter.expr)
+            .map(|guards| or_all(pg, guards))
+            .is_some_and(|guard| matches!(check_sat(pg, guard), SatResult::AlwaysSat));
+        let possibly_learned = possible
+            .remove(&parameter.expr)
+            .map(|guards| or_all(pg, guards))
+            .is_some_and(|guard| !matches!(check_sat(pg, guard), SatResult::DefinitelyUnsat));
+
+        output.insert(
+            parameter.expr,
+            match (input[&parameter.expr], definitely_learned, possibly_learned) {
+                (Knownness::Known, _, _) | (_, true, _) => Knownness::Known,
+                (Knownness::Unknown, false, true) => Knownness::Maybe,
+                (knownness, false, false) => knownness,
+                (Knownness::Maybe, false, true) => Knownness::Maybe,
+            },
+        );
+    }
+
+    output
+}
+
+fn analyze_knownness(
+    pg: &mut ProtoGraph,
+    entry: NodeId,
+    parameters: &FxHashMap<ExprRef, ParameterState>,
+) -> FxHashMap<NodeId, FxHashMap<ExprRef, Knownness>> {
+    let unknown: FxHashMap<ExprRef, Knownness> = parameters
+        .keys()
+        .map(|expr| (*expr, Knownness::Unknown))
+        .collect();
+    let mut input_facts = FxHashMap::default();
+    input_facts.insert(entry, unknown.clone());
+    let mut worklist = VecDeque::from([entry]);
+
+    while let Some(node) = worklist.pop_front() {
+        let output = transfer_knownness(pg, node, &input_facts[&node], parameters);
+        let transitions = pg[node].transitions.clone();
+        for transition in transitions {
+            let incoming = output.clone();
+            let changed = if let Some(existing) = input_facts.get_mut(&transition.target) {
+                let old = existing.clone();
+                for (expr, knownness) in incoming {
+                    existing
+                        .entry(expr)
+                        .and_modify(|current| *current = join_knownness(*current, knownness))
+                        .or_insert(knownness);
+                }
+                *existing != old
+            } else {
+                input_facts.insert(transition.target, incoming);
+                true
+            };
+            if changed {
+                worklist.push_back(transition.target);
+            }
+        }
+    }
+
+    input_facts
+}
+
+fn and_all(pg: &mut ProtoGraph, terms: impl IntoIterator<Item = ExprRef>) -> ExprRef {
+    terms
+        .into_iter()
+        .fold(pg.true_id(), |acc, term| pg.and_guard(acc, term))
+}
+
+fn push_assign(
+    pg: &mut ProtoGraph,
+    actions: &mut Vec<Action>,
+    guard: ExprRef,
+    lhs: SymbolId,
+    rhs: ExprRef,
+) {
+    let assignment = Assignment::concrete(pg.false_id(), guard, rhs);
+    let op = pg.o(Op::Assign(lhs, assignment));
+    actions.push(Action::new(pg.true_id(), op));
+}
+
+fn known_expr(
+    pg: &ProtoGraph,
+    parameter: ParameterState,
+    facts: &FxHashMap<ExprRef, Knownness>,
+) -> ExprRef {
+    match facts[&parameter.expr] {
+        Knownness::Unknown => pg.false_id(),
+        Knownness::Known => pg.true_id(),
+        Knownness::Maybe => parameter.known_expr.unwrap(),
+    }
+}
+
+fn push_known_update(
+    pg: &mut ProtoGraph,
+    actions: &mut Vec<Action>,
+    guard: ExprRef,
+    parameter: ParameterState,
+) {
+    if let Some(symbol) = parameter.known_symbol {
+        push_assign(pg, actions, guard, symbol, pg.true_id());
+    }
+}
+
+fn push_candidate_failure(
+    pg: &mut ProtoGraph,
+    actions: &mut Vec<Action>,
+    active: ExprRef,
+    live_symbol: SymbolId,
+    lhs: ExprRef,
+    rhs: ExprRef,
+) {
+    let equal = pg.expr_ctx.equal(lhs, rhs);
+    let mismatch = pg.not_guard(equal);
+    let guard = pg.and_guard(active, mismatch);
+    push_assign(pg, actions, guard, live_symbol, pg.false_id());
+}
+
+fn lower_candidate_equality(
+    pg: &mut ProtoGraph,
+    actions: &mut Vec<Action>,
+    active: ExprRef,
+    lhs: ExprRef,
+    rhs: ExprRef,
+    live_symbol: SymbolId,
+    parameters: &FxHashMap<ExprRef, ParameterState>,
+    facts: &FxHashMap<ExprRef, Knownness>,
+) {
+    if matches!(check_sat(pg, active), SatResult::DefinitelyUnsat) {
+        return;
+    }
+
+    let lhs_parameters = parameters_in_expr(pg, lhs, parameters);
+    let rhs_parameters = parameters_in_expr(pg, rhs, parameters);
+    let mut all_parameters = lhs_parameters.clone();
+    for parameter in &rhs_parameters {
+        if !all_parameters
+            .iter()
+            .any(|other| other.expr == parameter.expr)
+        {
+            all_parameters.push(*parameter);
+        }
+    }
+
+    if all_parameters.is_empty()
+        || all_parameters
+            .iter()
+            .all(|parameter| facts[&parameter.expr] == Knownness::Known)
+    {
+        push_candidate_failure(pg, actions, active, live_symbol, lhs, rhs);
+        return;
+    }
+
+    if let Some(parameter) = parameters.get(&lhs).copied()
+        && facts[&parameter.expr] == Knownness::Unknown
+        && rhs_parameters
+            .iter()
+            .all(|other| facts[&other.expr] == Knownness::Known)
+    {
+        push_assign(pg, actions, active, parameter.symbol, rhs);
+        push_known_update(pg, actions, active, parameter);
+        return;
+    }
+    if let Some(parameter) = parameters.get(&rhs).copied()
+        && facts[&parameter.expr] == Knownness::Unknown
+        && lhs_parameters
+            .iter()
+            .all(|other| facts[&other.expr] == Knownness::Known)
+    {
+        push_assign(pg, actions, active, parameter.symbol, lhs);
+        push_known_update(pg, actions, active, parameter);
+        return;
+    }
+
+    let all_known = and_all(
+        pg,
+        all_parameters
+            .iter()
+            .map(|parameter| known_expr(pg, *parameter, facts))
+            .collect::<Vec<_>>(),
+    );
+    let check_guard = pg.and_guard(active, all_known);
+    push_candidate_failure(pg, actions, check_guard, live_symbol, lhs, rhs);
+
+    let mut handled = all_known;
+    if let Some(parameter) = parameters.get(&lhs).copied() {
+        let rhs_known = and_all(
+            pg,
+            rhs_parameters
+                .iter()
+                .map(|other| known_expr(pg, *other, facts))
+                .collect::<Vec<_>>(),
+        );
+        let lhs_unknown = pg.not_guard(known_expr(pg, parameter, facts));
+        let can_bind = pg.and_guard(lhs_unknown, rhs_known);
+        let bind_guard = pg.and_guard(active, can_bind);
+        push_assign(pg, actions, bind_guard, parameter.symbol, rhs);
+        push_known_update(pg, actions, bind_guard, parameter);
+        handled = pg.or_guard(handled, can_bind);
+    }
+    if let Some(parameter) = parameters.get(&rhs).copied() {
+        let lhs_known = and_all(
+            pg,
+            lhs_parameters
+                .iter()
+                .map(|other| known_expr(pg, *other, facts))
+                .collect::<Vec<_>>(),
+        );
+        let rhs_unknown = pg.not_guard(known_expr(pg, parameter, facts));
+        let can_bind = pg.and_guard(rhs_unknown, lhs_known);
+        let bind_guard = pg.and_guard(active, can_bind);
+        push_assign(pg, actions, bind_guard, parameter.symbol, lhs);
+        push_known_update(pg, actions, bind_guard, parameter);
+        handled = pg.or_guard(handled, can_bind);
+    }
+
+    let unsupported = pg.not_guard(handled);
+    let unsupported = pg.and_guard(active, unsupported);
+    push_assign(pg, actions, unsupported, live_symbol, pg.false_id());
+}
+
+fn learn_equality_knownness(
+    pg: &mut ProtoGraph,
+    active: ExprRef,
+    lhs: ExprRef,
+    rhs: ExprRef,
+    parameters: &FxHashMap<ExprRef, ParameterState>,
+    facts: &mut FxHashMap<ExprRef, Knownness>,
+) {
+    let active_sat = check_sat(pg, active);
+    if matches!(active_sat, SatResult::DefinitelyUnsat) {
+        return;
+    }
+
+    for (candidate, other) in [(lhs, rhs), (rhs, lhs)] {
+        if !parameters.contains_key(&candidate) {
+            continue;
+        }
+        let dependencies = parameters_in_expr(pg, other, parameters);
+        if dependencies
+            .iter()
+            .all(|dependency| facts[&dependency.expr] == Knownness::Known)
+        {
+            let learned = if matches!(active_sat, SatResult::AlwaysSat) {
+                Knownness::Known
+            } else {
+                Knownness::Maybe
+            };
+            facts.entry(candidate).and_modify(|knownness| {
+                if *knownness == Knownness::Unknown {
+                    *knownness = learned;
+                }
+            });
+        }
+    }
+}
+
+fn allocate_protocol_seeds(
+    protos: &[Protocol],
+    symbols: &mut SymbolTable,
+) -> Result<Vec<ProtocolSeed>, ToMonitorError> {
+    let mut seeds = Vec::with_capacity(protos.len());
+    for protocol in protos {
+        let prefix = protocol.name.clone();
+        let live_name = format!("{prefix}_live");
+        let live_symbol = symbols.add_without_parent(
+            live_name.clone(),
+            Type::BitVec(1),
+            SymbolKind::MonitorState,
+        );
+        let mut parameters = Vec::with_capacity(protocol.args.len());
+        for argument in &protocol.args {
+            let original = argument.symbol();
+            let Type::BitVec(width) = symbols[original].tpe() else {
+                return Err(ToMonitorError::NonBitVectorParameter(
+                    symbols.full_name_from_symbol_id(&original),
+                ));
+            };
+            let argument_name = symbols[original].name();
+            let name = format!("{prefix}_{argument_name}");
+            let known_name = format!("{name}_known");
+            let symbol = symbols.add_without_parent(
+                name.clone(),
+                Type::BitVec(width),
+                SymbolKind::MonitorState,
+            );
+            let known_symbol = symbols.add_without_parent(
+                known_name.clone(),
+                Type::BitVec(1),
+                SymbolKind::MonitorState,
+            );
+            parameters.push(ParameterSeed {
+                original,
+                symbol,
+                known_symbol,
+                name,
+                known_name,
+                width,
+            });
+        }
+        seeds.push(ProtocolSeed {
+            live_symbol,
+            live_name,
+            parameters,
+        });
+    }
+    Ok(seeds)
+}
+
+fn instantiate_candidate(
+    lowerer: &mut Lowerer<'_>,
+    protocol: &Protocol,
+    seed: &ProtocolSeed,
+) -> (LoweredFragmentInfo, CandidateState) {
+    let prototype = lowerer.lower_protocol_fragment(protocol, false, true);
+    let mut substitutions = FxHashMap::default();
+    let mut parameters = Vec::with_capacity(seed.parameters.len());
+
+    for parameter in &seed.parameters {
+        let expr = lowerer
+            .ir
+            .expr_ctx
+            .bv_symbol(&parameter.name, parameter.width);
+        lowerer.ir.cache_symbol_expr(parameter.symbol, expr);
+        lowerer.ir.state_init.insert(
+            parameter.symbol,
+            lowerer.ir.expr_ctx.bit_vec_val(0, parameter.width),
+        );
+        if let Some(original_expr) = lowerer.ir.symbol_expr(parameter.original) {
+            substitutions.insert(original_expr, expr);
+        }
+        parameters.push(ParameterState {
+            symbol: parameter.symbol,
+            expr,
+            known_symbol: None,
+            known_expr: None,
+        });
+    }
+
+    let live_expr = lowerer.ir.expr_ctx.bv_symbol(&seed.live_name, 1);
+    lowerer.ir.cache_symbol_expr(seed.live_symbol, live_expr);
+    lowerer
+        .ir
+        .state_init
+        .insert(seed.live_symbol, lowerer.ir.true_id());
+    let fragment = lowerer.copy_protocol_fragment(prototype, &substitutions);
+    (
+        fragment,
+        CandidateState {
+            live_symbol: seed.live_symbol,
+            live_expr,
+            parameters,
+        },
+    )
+}
+
+fn transform_candidate_fragment(
+    pg: &mut ProtoGraph,
+    symbols: &SymbolTable,
+    fragment: &LoweredFragmentInfo,
+    seed: &ProtocolSeed,
+    candidate: &mut CandidateState,
+) -> Result<(), ToMonitorError> {
+    for node_id in &fragment.nodes {
+        for action in pg[*node_id].actions.clone() {
+            if let Op::Assign(symbol, _) = pg[action.op] {
+                symbol_expr(pg, symbols, symbol)?;
+            }
+        }
+    }
+
+    let mut parameters: FxHashMap<ExprRef, ParameterState> = candidate
+        .parameters
+        .iter()
+        .map(|parameter| (parameter.expr, *parameter))
+        .collect();
+    let facts = analyze_knownness(pg, fragment.entry, &parameters);
+
+    for (parameter, parameter_seed) in candidate.parameters.iter_mut().zip(&seed.parameters) {
+        if !facts
+            .values()
+            .any(|fact| fact.get(&parameter.expr) == Some(&Knownness::Maybe))
+        {
+            continue;
+        }
+        let known_expr = pg.expr_ctx.bv_symbol(&parameter_seed.known_name, 1);
+        pg.cache_symbol_expr(parameter_seed.known_symbol, known_expr);
+        pg.state_init
+            .insert(parameter_seed.known_symbol, pg.false_id());
+        parameter.known_symbol = Some(parameter_seed.known_symbol);
+        parameter.known_expr = Some(known_expr);
+    }
+    parameters = candidate
+        .parameters
+        .iter()
+        .map(|parameter| (parameter.expr, *parameter))
+        .collect();
+
+    for node_id in facts.keys().copied().collect::<Vec<_>>() {
+        let node_active = if node_id == fragment.entry {
+            pg.true_id()
+        } else {
+            candidate.live_expr
+        };
+        let old_actions = pg[node_id].actions.clone();
+        let mut actions = Vec::new();
+        let mut local_facts = facts[&node_id].clone();
+        for action in old_actions {
+            match pg[action.op].clone() {
+                Op::Assign(port, assignment) => {
+                    let port_expr = symbol_expr(pg, symbols, port)?;
+                    for (assignment_guard, rhs) in assignment.concretes {
+                        let active = pg.and_guard(action.guard, assignment_guard);
+                        let active = pg.and_guard(node_active, active);
+                        lower_candidate_equality(
+                            pg,
+                            &mut actions,
+                            active,
+                            port_expr,
+                            rhs,
+                            candidate.live_symbol,
+                            &parameters,
+                            &local_facts,
+                        );
+                        learn_equality_knownness(
+                            pg,
+                            active,
+                            port_expr,
+                            rhs,
+                            &parameters,
+                            &mut local_facts,
+                        );
+                    }
+                }
+                Op::AssertEq(lhs, rhs) => {
+                    let active = pg.and_guard(node_active, action.guard);
+                    lower_candidate_equality(
+                        pg,
+                        &mut actions,
+                        active,
+                        lhs,
+                        rhs,
+                        candidate.live_symbol,
+                        &parameters,
+                        &local_facts,
+                    );
+                    learn_equality_knownness(pg, active, lhs, rhs, &parameters, &mut local_facts);
+                }
+                Op::Fork => return Err(ToMonitorError::UnsupportedFork),
+                Op::InternalAssertFalse | Op::Done => {
+                    let guard = pg.and_guard(node_active, action.guard);
+                    actions.push(action.with_guard(guard));
+                }
+            }
+        }
+
+        let transitions = pg[node_id].transitions.clone();
+        let transition_guards: Vec<_> = transitions
+            .iter()
+            .map(|transition| pg.expr_ctx.and(candidate.live_expr, transition.guard))
+            .collect();
+        pg.node_mut(node_id).actions = actions;
+        for (transition, guard) in pg
+            .node_mut(node_id)
+            .transitions
+            .iter_mut()
+            .zip(transition_guards)
+        {
+            transition.guard = guard;
+        }
+    }
+    initialize_candidate_entry(pg, fragment.entry, candidate);
+    Ok(())
+}
+
+fn initialize_candidate_entry(pg: &mut ProtoGraph, entry: NodeId, candidate: &CandidateState) {
+    let old_actions = pg[entry].actions.clone();
+    let mut actions = Vec::new();
+    let mut live_kills = Vec::new();
+    let known_symbols: FxHashSet<_> = candidate
+        .parameters
+        .iter()
+        .filter_map(|parameter| parameter.known_symbol)
+        .collect();
+    let mut known_sets: FxHashMap<SymbolId, Vec<ExprRef>> = FxHashMap::default();
+
+    for action in old_actions {
+        let Op::Assign(symbol, assignment) = pg[action.op].clone() else {
+            actions.push(action);
+            continue;
+        };
+        if symbol != candidate.live_symbol && !known_symbols.contains(&symbol) {
+            actions.push(action);
+            continue;
+        }
+        for (branch_guard, rhs) in assignment.concretes {
+            let guard = pg.and_guard(action.guard, branch_guard);
+            if symbol == candidate.live_symbol && rhs == pg.false_id() {
+                live_kills.push(guard);
+            } else if known_symbols.contains(&symbol) && rhs == pg.true_id() {
+                known_sets.entry(symbol).or_default().push(guard);
+            }
+        }
+    }
+
+    let kill = or_all(pg, live_kills);
+    let survives = pg.not_guard(kill);
+    let live_assignment = Assignment {
+        dont_care: pg.false_id(),
+        concretes: vec![(kill, pg.false_id()), (survives, pg.true_id())],
+    };
+    let live_op = pg.o(Op::Assign(candidate.live_symbol, live_assignment));
+    actions.push(Action::new(pg.true_id(), live_op));
+
+    for parameter in &candidate.parameters {
+        let Some(known_symbol) = parameter.known_symbol else {
+            continue;
+        };
+        let set = or_all(pg, known_sets.remove(&known_symbol).unwrap_or_default());
+        let clear = pg.not_guard(set);
+        let assignment = Assignment {
+            dont_care: pg.false_id(),
+            concretes: vec![(set, pg.true_id()), (clear, pg.false_id())],
+        };
+        let op = pg.o(Op::Assign(known_symbol, assignment));
+        actions.push(Action::new(pg.true_id(), op));
+    }
+    pg.node_mut(entry).actions = actions;
+}
+
+fn loop_fragment_exit_to_entry(
+    pg: &mut ProtoGraph,
+    fragment: &LoweredFragmentInfo,
+    entry: NodeId,
+    live_expr: ExprRef,
+) {
+    for node in fragment
+        .nodes
+        .iter()
+        .copied()
+        .filter(|node| *node != fragment.exit)
+    {
+        for transition in &mut pg.node_mut(node).transitions {
+            if transition.target == fragment.exit {
+                transition.target = entry;
+                transition.consumes_step = true;
+            }
+        }
+        let return_guards: Vec<_> = pg[node]
+            .transitions
+            .iter()
+            .filter(|transition| transition.target == entry)
+            .map(|transition| transition.guard)
+            .collect();
+        let return_guard = or_all(pg, return_guards);
+        if return_guard != pg.false_id() {
+            let done = pg.o(Op::Done);
+            let done_guard = pg.and_guard(live_expr, return_guard);
+            pg.push_action(node, Action::new(done_guard, done));
+        }
+    }
+}
+
+/// Lower protocols directly into a deterministic steady-state monitor.
+///
+/// Each protocol receives its own parameter bank and live bit. Observations
+/// bind unknown parameters and eliminate only that protocol on a known-value
+/// mismatch. The live protocol fragments are grafted together and subset
+/// construction makes every surviving combination explicit.
+pub fn to_monitor(
+    protos: Vec<Protocol>,
+    symbols: &mut SymbolTable,
+    expr_ctx: ExprContext,
+) -> Result<ProtoGraph, ToMonitorError> {
+    let Some(first) = protos.first() else {
+        return Err(ToMonitorError::EmptyProtocolSet);
+    };
+    let seeds = allocate_protocol_seeds(&protos, symbols)?;
+    let mut lowerer = Lowerer::with_expr_ctx(first.ctx.clone(), symbols, expr_ctx);
+    let mut fragments = Vec::with_capacity(protos.len());
+    let mut candidates = Vec::with_capacity(protos.len());
+
+    for (protocol, seed) in protos.iter().zip(&seeds) {
+        let (fragment, candidate) = instantiate_candidate(&mut lowerer, protocol, seed);
+        fragments.push(fragment);
+        candidates.push(candidate);
+    }
+
+    for ((fragment, seed), candidate) in fragments.iter().zip(&seeds).zip(&mut candidates) {
+        transform_candidate_fragment(&mut lowerer.ir, lowerer.symbols, fragment, seed, candidate)?;
+    }
+
+    let entry = lowerer.ir.entry;
+    for (fragment, candidate) in fragments.iter().zip(&candidates) {
+        loop_fragment_exit_to_entry(&mut lowerer.ir, fragment, entry, candidate.live_expr);
+        lowerer.graft_contracted_entry(entry, fragment.entry, lowerer.ir.true_id());
+    }
+
+    lowerer.ir.simplify_all_exprs();
+    let mut monitor = determinized(lowerer.ir, symbols);
+    monitor.garbage_collect_unreachable();
+    Ok(monitor)
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::frontend;
+    use crate::frontend::diagnostic::DiagnosticHandler;
+    use crate::frontend::require_single_module;
+    use crate::ir::graphviz::to_dot_string;
+    use patronus::expr::Context as ExprContext;
+    use std::fs;
+    use tempfile::NamedTempFile;
+
+    fn lower_monitor(source: &str) -> (ProtoGraph, SymbolTable) {
+        let file = NamedTempFile::new().unwrap();
+        fs::write(file.path(), source).unwrap();
+        let mut diagnostics = DiagnosticHandler::default();
+        let (mut symbols, modules) = frontend(&[file.path()], &mut diagnostics, true).unwrap();
+        let module = require_single_module(modules, &[file.path()]).unwrap();
+        let monitor = to_monitor(module.protos, &mut symbols, ExprContext::default()).unwrap();
+        (monitor, symbols)
+    }
+
+    #[test]
+    fn steady_state_driver_actions_become_explicit_monitor_state_updates() {
+        let (monitor, symbols) = lower_monitor(
+            r#"
+            struct Device {
+                in x: u32,
+                out z: u32,
+            }
+
+            prot transaction<dut: Device>(a: u32) {
+                dut.x := a;
+                step();
+                assert_eq(dut.z, a);
+                step();
+            }
+            "#,
+        );
+
+        let mut saw_argument_update = false;
+        let mut saw_knownness_update = false;
+        let mut saw_monitor_assertion = false;
+
+        for (_, node) in monitor.nodes() {
+            for action in &node.actions {
+                match &monitor[action.op] {
+                    Op::Assign(symbol, _) => match symbols[*symbol].kind() {
+                        SymbolKind::Arg(_) => saw_argument_update = true,
+                        SymbolKind::MonitorState => saw_knownness_update = true,
+                        SymbolKind::InPort | SymbolKind::OutPort => {
+                            panic!("monitor graph still drives a DUT port")
+                        }
+                        SymbolKind::Dut | SymbolKind::LoopVar => {
+                            panic!("unexpected monitor assignment target")
+                        }
+                    },
+                    Op::AssertEq(_, _) => saw_monitor_assertion = true,
+                    Op::Fork => panic!("synthetic steady-state fork was not removed"),
+                    Op::InternalAssertFalse | Op::Done => {}
+                }
+            }
+        }
+
+        assert!(!saw_argument_update);
+        assert!(saw_knownness_update);
+        assert!(!saw_monitor_assertion);
+        assert_eq!(
+            monitor
+                .state_init
+                .keys()
+                .filter(|symbol| symbols[**symbol].is_arg())
+                .count(),
+            0
+        );
+        assert_eq!(
+            monitor
+                .state_init
+                .keys()
+                .filter(|symbol| symbols[**symbol].is_monitor_state())
+                .count(),
+            2
+        );
+    }
+
+    #[test]
+    fn serializes_normal_swapped_monitor() {
+        let (monitor, symbols) = lower_monitor(
+            r#"
+            struct Device {
+                in x: u32,
+                in y: u32,
+                out z: u32,
+            }
+
+            prot normal<dut: Device>(a: u32, b: u32) {
+                dut.x := a;
+                dut.y := b;
+                step();
+                assert_eq(dut.z, a);
+                step();
+            }
+
+            prot swapped<dut: Device>(a: u32, b: u32) {
+                dut.x := b;
+                dut.y := a;
+                step();
+                assert_eq(dut.z, a);
+                step();
+            }
+            "#,
+        );
+
+        let serialized = to_dot_string(&monitor, &symbols);
+        println!("{}", serialized);
+        assert!(!serialized.contains("proto_choice"));
+        assert!(serialized.contains("_live"));
+    }
+
+    #[test]
+    fn serializes_add_d0_monitor() {
+        let (monitor, symbols) = lower_monitor(
+            r#"
+            struct Device {
+                in a: u32,
+                in b: u32,
+                in op: u1,
+                out s: u32,
+            }
+
+            prot add<dut: Device>(a: u32, b: u32, s: u32) {
+                dut.a := a;
+                dut.b := b;
+                dut.op := 1'b0;
+                step();
+                dut.a := X;
+                dut.b := X;
+                assert_eq(dut.s, s);
+                step();
+            }
+
+            prot sub<dut: Device>(a: u32, b: u32, s: u32) {
+                dut.a := a;
+                dut.b := b;
+                dut.op := 1'b1;
+                step();
+                dut.a := X;
+                dut.b := X;
+                assert_eq(dut.s, s);
+                step();
+            }
+            "#,
+        );
+
+        let serialized = to_dot_string(&monitor, &symbols);
+        println!("{serialized}");
+    }
+
+    #[test]
+    fn serializes_wishbone_read_write_monitor() {
+        use crate::transaction_frontend;
+        use std::collections::HashSet;
+
+        let protocol_file = "../examples/wishbone/wishbone.prot";
+        let trace_file = "../examples/wishbone/read_write.tx";
+        let mut diagnostics = DiagnosticHandler::default();
+        let (mut symbols, modules) = frontend(&[protocol_file], &mut diagnostics, true).unwrap();
+        let module = require_single_module(modules, &[protocol_file]).unwrap();
+        let traces =
+            transaction_frontend(trace_file, &symbols, &module.protos, &mut diagnostics).unwrap();
+        let selected_names: HashSet<_> = traces[0].iter().map(|(name, _)| name.as_str()).collect();
+        let selected = module
+            .protos
+            .into_iter()
+            .filter(|protocol| selected_names.contains(protocol.name.as_str()))
+            .collect();
+
+        let monitor = to_monitor(selected, &mut symbols, ExprContext::default()).unwrap();
+        let serialized = to_dot_string(&monitor, &symbols);
+        let output = std::path::Path::new(env!("CARGO_MANIFEST_DIR"))
+            .join("../scripts/wishbone_read_write_monitor.dot");
+        fs::write(output, &serialized).unwrap();
+        assert!(!serialized.contains("internal_assert_false"));
+        println!("{serialized}");
+    }
+}
diff --git a/scripts/wishbone_read_write_monitor.dot b/scripts/wishbone_read_write_monitor.dot
new file mode 100644
index 00000000..3182d1dd
--- /dev/null
+++ b/scripts/wishbone_read_write_monitor.dot
@@ -0,0 +1,16 @@
+digraph "reset" {
+  rankdir=LR;
+  node [shape=box];
+  entry_marker [shape=plain,label="ENTRY"];
+  entry_marker -> node0;
+  node0 [label="[1] reset_live := 0 if or(or(not(self.RST), self.CYC), self.STB); 1 if not(or(or(not(self.RST), self.CYC), self.STB))\n[or(or(or(reset_live, idle_no_cycle_live), and(write_live, and(write_live, self.ACK))), and(read_live, and(read_live, self.ACK)))] done\n[1] idle_no_cycle_live := 0 if or(self.RST, self.CYC); 1 if not(or(self.RST, self.CYC))\n[1] write_mask := 15 if 1\n[1] write_addr := self.ADR if 1\n[1] write_data := self.DAT_O if 1\n[1] write_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0))))\n[1] read_mask := 15 if 1\n[1] read_data := self.DAT_I if self.ACK\n[1] read_addr := self.ADR if 1\n[1] read_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0))))\n[1] read_data_known := 1 if self.ACK; 0 if not(self.ACK)"];
+  node0 -> node0 [label="or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)) / step"];
+  node0 -> node1 [label="and(write_live, not(self.ACK)) / step"];
+  node0 -> node2 [label="and(read_live, not(self.ACK)) / step"];
+  node1 [label="[1] write_live := 0 if or(or(or(or(or(or(or(and(write_live, self.RST), and(write_live, not(eq(self.ADR, write_addr)))), and(write_live, not(self.CYC))), and(write_live, not(eq(self.DAT_O, write_data)))), and(write_live, not(eq(self.SEL, write_mask)))), and(write_live, not(self.STB))), and(write_live, not(self.WE))), and(write_live, not(eq(self.CTI, 0))))\n[and(write_live, and(write_live, self.ACK))] done"];
+  node1 -> node0 [label="and(write_live, self.ACK) / step"];
+  node1 -> node1 [label="and(write_live, not(self.ACK)) / step"];
+  node2 [label="[1] read_live := 0 if or(or(or(or(or(or(or(and(and(and(read_live, self.ACK), read_data_known), not(eq(self.DAT_I, read_data))), and(read_live, self.RST)), and(read_live, not(eq(self.ADR, read_addr)))), and(read_live, not(self.CYC))), and(read_live, not(eq(self.SEL, read_mask)))), and(read_live, not(self.STB))), and(read_live, self.WE)), and(read_live, not(eq(self.CTI, 0))))\n[1] read_data := self.DAT_I if and(and(read_live, self.ACK), not(read_data_known))\n[1] read_data_known := 1 if and(and(read_live, self.ACK), not(read_data_known))\n[and(read_live, and(read_live, self.ACK))] done"];
+  node2 -> node0 [label="and(read_live, self.ACK) / step"];
+  node2 -> node2 [label="and(read_live, not(self.ACK)) / step"];
+}