04:12:03 <xmrack[m]> kayabanerve: https://cdck-file-uploads-global.s3.dualstack.us-west-2.amazonaws.com/zcash/original/3X/5/0/50b210737efe301239d8d774a43e1f1d6234eab9.pdf
04:12:47 <xmrack[m]> High Assurance Specification of the halo2 Protocol
04:14:04 <kayabanerve[m]> I've heard of the effort
04:26:25 <kayabanerve[m]> 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.
12:21:17 <xmrack[m]> Do you think hacspec would be a good option for us to verify our implementation follows our own theoretical design?