Specification and verification

This part is for the verification team.

• writing specification (Sphinx + directives to extract rules)
• running verification (CI + locally replaying a random test from CI)
• reporting results (HTML?)

Kinds of directives:

• requirements (on the inputs): asserted in integration tests and unit tests; met in random component tests
• assertions (on the outputs): asserted in integration tests and component tests; met in "model" random tests if we implement the feature.