Interesting stuff, the uniformity for so many proofs is compelling.

The names/id's are pretty hard imho yet they are used everywhere, e.g "readdcli": could be about "read" or "add" at first sight. Maybe if they were a bit longer and more descriptive, less clicking on them to view what they are might be needed...