[FEATURE] Verify / test MKM module

[septract]

Summary

We want to see whether the MKM module can be verified and/or tested in CN. This is ahead of our end-of-phase milestone in early 2025.

Feature

The aim of this branch is to try to apply cn verify or cn test to some bits of the MKM module. See #98 for the associated issue tracking the MKM code itself

Acceptance Criteria

Done when the MKM code or client code can be tested or verified.

Do

• Construct reduced examples based on MKM client code
• Test / verify reduced examples
• Write specifications for MKM client code
• Test / verify production client code