diff --git a/docs/source/getting_started/example_synth.rst b/docs/source/getting_started/example_synth.rst
index d155d41c9..b3d4aa679 100644
--- a/docs/source/getting_started/example_synth.rst
+++ b/docs/source/getting_started/example_synth.rst
@@ -23,6 +23,9 @@ A simple counter
 .. role:: yoscrypt(code)
    :language: yoscrypt
 
+.. todo:: consider changing simple counter example for something with memory
+   using e.g. synth_ice40 to cover more of the synth flow
+
 This section covers an `example project`_ available in
 ``docs/source/code_examples/intro/``.  The project contains a simple ASIC
 synthesis script (``counter.ys``), a digital design written in Verilog
@@ -181,11 +184,11 @@ Some of the commands we might use here are:
 - :doc:`/cmd/alumacc`, and
 - :doc:`/cmd/share`.
 
-We could have also 
-
 Logic gate mapping
 ~~~~~~~~~~~~~~~~~~
 
+.. todo:: example_synth mapping to gates
+
 :yoscrypt:`techmap` - Map coarse-grain RTL cells (adders, etc.) to fine-grain
 logic gates (AND, OR, NOT, etc.).
 
@@ -207,6 +210,8 @@ cells used.
 Mapping to hardware
 ~~~~~~~~~~~~~~~~~~~
 
+.. todo:: example_synth mapping to hardware
+
 :ref:`cmos_lib`
 
 #. :yoscrypt:`dfflibmap -liberty mycells.lib` - Map registers to available
diff --git a/docs/source/introduction.rst b/docs/source/introduction.rst
index 727426fa8..7f5f1e106 100644
--- a/docs/source/introduction.rst
+++ b/docs/source/introduction.rst
@@ -117,13 +117,22 @@ Benefits of open source HDL synthesis
 The extended Yosys universe
 ---------------------------
 
-.. todo:: links and add SCY
-
 In no particular order:
 
 - SBY for formal verification
+   - https://github.com/YosysHQ/sby
+   - https://yosyshq.readthedocs.io/projects/sby
+
 - EQY for equivalence checking
+   - https://github.com/YosysHQ/eqy
+   - https://yosyshq.readthedocs.io/projects/eqy
+
 - MCY for mutation coverage
+   - https://github.com/YosysHQ/mcy
+   - https://yosyshq.readthedocs.io/projects/mcy
+
+- SCY for deep formal traces
+   - https://github.com/YosysHQ/scy
 
 History of Yosys
 ----------------
diff --git a/docs/source/using_yosys/more_scripting/load_design.rst b/docs/source/using_yosys/more_scripting/load_design.rst
index 91da5b538..d64c50959 100644
--- a/docs/source/using_yosys/more_scripting/load_design.rst
+++ b/docs/source/using_yosys/more_scripting/load_design.rst
@@ -24,6 +24,9 @@ keyword: Frontends
     read_verilog file6.v
     verilog_defaults -pop
 
+.. todo:: more info on other ``read_*`` commands, also is this the first time we
+   mention verific?
+
 Others:
 
 - :doc:`/cmd/read`
diff --git a/docs/source/using_yosys/yosys_flows.rst b/docs/source/using_yosys/yosys_flows.rst
index 170db416c..a3fae32a4 100644
--- a/docs/source/using_yosys/yosys_flows.rst
+++ b/docs/source/using_yosys/yosys_flows.rst
@@ -39,7 +39,8 @@ The extract pass
   subcircuit with an instance of the module from the map file.
 - In a way the :cmd:ref:`extract` pass is the inverse of the techmap pass.
 
-.. todo:: add/expand supporting text
+.. todo:: add/expand supporting text, also mention custom pattern matching and
+   pmgen
 
 .. literalinclude:: /code_examples/macc/macc_simple_test.ys
     :language: yoscrypt
@@ -277,7 +278,7 @@ Checking.
 Checking techmap
 ~~~~~~~~~~~~~~~~
 
-.. todo:: add/expand supporting text
+.. todo:: add/expand supporting text, reference no longer exists
 
 Remember the following example from :doc:`/getting_started/typical_phases`?
 
diff --git a/docs/source/yosys_internals/flow/verilog_frontend.rst b/docs/source/yosys_internals/flow/verilog_frontend.rst
index 6a0389f20..b36eb3bbf 100644
--- a/docs/source/yosys_internals/flow/verilog_frontend.rst
+++ b/docs/source/yosys_internals/flow/verilog_frontend.rst
@@ -409,9 +409,7 @@ multiplexers.
 In more complex examples (e.g. asynchronous resets) the part of the
 ``RTLIL::CaseRule``/``RTLIL::SwitchRule`` tree that describes the asynchronous
 reset must first be transformed to the correct ``RTLIL::SyncRule`` objects. This
-is done by the ``proc_adff`` pass.
-
-.. todo:: The ``proc_adff`` pass doesn't exist anymore?
+is done by the ``proc_arst`` pass.
 
 The ProcessGenerator algorithm
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~