Formal Verification

Formal verification describes the process of proving the correctness of a system with respect to a formal specification using mathematical methods. In the context of Nock, this involves demonstrating that the Nock opcodes and evaluation rules behave as intended under all possible inputs.

Several formal verifications of Nock have been conducted:

• KNock in K Framework, an evaluation model for correctness.

• Pure Nock in Lean, the Nockchain zkVM formalization.