1. Auditor Environment Pins
The following toolchain versions are strictly pinned to ensure compilation and replay hashes are deterministic:
- Rust
- 1.95.0
- NPA
- v0.1.1
NPA
Technical Spec
Toolchain & Replay Spec
Technical specifications of the cryptographic checker environment and deterministic replay logs.
To ensure mathematical correctness remains absolute, all checkers run in a pinned deterministic sandbox. This page details our compiler environments and replay configurations.
2. Cryptographic Certificate Format (.npcert)
NPA certificate files are structured binary payloads containing export hashes and ECDSA signatures verified by the reference checker.
3. Deterministic Replay Engine
The proof replay engine reads verification steps from replay.json and reconstructs formal proof terms to re-verify them inside the kernel.