This is blatantly false. People are using formal verification tools in hardware design, and they do work and they do compose. Here is a simple verilog code whic

This is blatantly false. People are using formal verification tools in hardware design, and they do work and they do compose. Here is a simple verilog code which accomplishes some of what he wants. module Blinker ( input wire clock, output reg state ); always @(posedge clock) state <= !state; `if FORMAL always @(posedge clock) assert ($past(state) != state); `endif endmodule module testbench ( input wire clock, output wire state1, output wire state2 ); Blinker blinker1(clock, state1); Blinker blinker2(clock, state2); `if FORMAL # assume that they are different assume (state1 != state2); # then they stay different always @(posedge clock) assert (state1 != state2); `endif endmodule Of course you NEED clock wires to the blinker. Composability comes from the use of assume and assert. You assume that your environment is behaving according to spec and you prove that you are also behaving to spec PROVIDED the environment working correctly. See https://symbiyosys.readthedocs.io/en/latest/index.html https://symbiyosys.readthedocs.io/en/latest/index.html for more details. Moral of the story: broken spec cannot be used, and I am saying this as a mathematician!