Reference. Audit-before-commit decisions [ftip-00IZ]
✍️source

    The audit record in Definition [ftip-00HL] binds a decision to the execution evidence. The required checks and digest condition are stated in Theorem [ftip-00HM].