diff --git a/docs/source/appendix/auxlibs.rst b/docs/source/appendix/auxlibs.rst
index 2f443c041..861634648 100644
--- a/docs/source/appendix/auxlibs.rst
+++ b/docs/source/appendix/auxlibs.rst
@@ -4,12 +4,7 @@ Auxiliary libraries
 The Yosys source distribution contains some auxiliary libraries that are bundled
 with Yosys.
 
-SHA1
-----
-
-The files in ``libs/sha1/`` provide a public domain SHA1 implementation written
-by Steve Reid, Bruce Guenter, and Volker Grabsch. It is used for generating
-unique names when specializing parameterized modules.
+.. todo:: fill out the newer auxiliary libs
 
 BigInt
 ------
@@ -22,15 +17,10 @@ ConstEval class provided in kernel/consteval.h.
 
 See also: http://mattmccutchen.net/bigint/
 
-.. _sec:SubCircuit:
+dlfcn-win32
+-----------
 
-SubCircuit
-----------
-
-The files in ``libs/subcircuit`` provide a library for solving the subcircuit
-isomorphism problem. It is written by C. Wolf and based on the Ullmann Subgraph
-Isomorphism Algorithm :cite:p:`UllmannSubgraphIsomorphism`. It is used by the
-extract pass (see :doc:`../cmd/extract`).
+The files in ``libs/dlfcn-win32`` provide...
 
 ezSAT
 -----
@@ -40,3 +30,34 @@ formulas for SAT solvers. It also contains bindings of MiniSAT. The ezSAT
 library is written by C. Wolf. It is used by the sat pass (see
 :doc:`../cmd/sat`).
 
+fst
+---
+
+The files in ``libs/fst`` provide...
+
+json11
+------
+
+The files in ``libs/json11`` provide...
+
+MiniSAT
+-------
+
+The files in ``libs/minisat`` provide...
+
+SHA1
+----
+
+The files in ``libs/sha1/`` provide a public domain SHA1 implementation written
+by Steve Reid, Bruce Guenter, and Volker Grabsch. It is used for generating
+unique names when specializing parameterized modules.
+
+.. _sec:SubCircuit:
+
+SubCircuit
+----------
+
+The files in ``libs/subcircuit`` provide a library for solving the subcircuit
+isomorphism problem. It is written by C. Wolf and based on the Ullmann Subgraph
+Isomorphism Algorithm :cite:p:`UllmannSubgraphIsomorphism`. It is used by the
+extract pass (see :doc:`../cmd/extract`).
diff --git a/docs/source/appendix/auxprogs.rst b/docs/source/appendix/auxprogs.rst
index 9071abfd1..a80e8f535 100644
--- a/docs/source/appendix/auxprogs.rst
+++ b/docs/source/appendix/auxprogs.rst
@@ -1,6 +1,8 @@
 Auxiliary programs
 ==================
 
+.. todo:: check this list is up to date and correct, esp yosys-smtbmc
+
 Besides the main yosys executable, the Yosys distribution contains a set of
 additional helper programs.
 
@@ -27,3 +29,11 @@ This is a fork of ABC with a small set of custom modifications that have not yet
 been accepted upstream. Not all versions of Yosys work with all versions of ABC.
 So Yosys comes with its own yosys-abc to avoid compatibility issues between the
 two.
+
+yosys-smtbmc
+------------
+
+yosys-witness
+-------------
+
+yosys-witness is a new tool to inspect and convert yosys witness traces.