Readable by commit.
Small steps in pulling the synthesis entry point for Specifications free for external use. Note that f8ead57c (Check the result spec for correctness rather than the input spec) is a bugfix, it checks the wrong specification.
Specification
Addresses #738