In order to understand whether an implementation of
3vat CapTP is correct, we need to look at diagram
sequences like
http://www.erights.org/elib/distrib/captp/DeliverOp.html#step1
for each case that needs to be verified. There are too
many cases to draw these diagrams manually, so we need
to find a way to snapshot CapTP state at appropriate
points of execution, and feed it to a tool that'll
automatically generate the corresponding diagram
sequences (or "whiteboard animation").
Once 2vat CapTP is better tested textually, we can use
it as a proving ground for the visualizer.