kayabanerve: cdck-file-uploads-global.s3.dualsta…efe301239d8d774a43e1f1d6234eab9.pdf

High Assurance Specification of the halo2 Protocol

I've heard of the effort

AFAIK, it offers a guarantee you match a spec, not a guarantee the spec does what it claims. It's also only partially formalized by this effort.

Do you think hacspec would be a good option for us to verify our implementation follows our own theoretical design?