Bit gadget isn't formally verified and/or audited

[kayabaNerve]

Ideally, we can formally verify it lines up with a security proof on our end, then have it audited with everything.