FAQ

Frequently Asked Questions

Answers to common questions about formal verification, certificates, and auditing policies.

How does NPA differ from a standard Lean kernel check?

Standard Lean checking compiles and verifies files on the local machine. NPA takes these verified compilation outputs, packages them with deterministic hashes, and wraps them in a cryptographically signed certificate (.npcert). This allows third-party users to audit the verification state instantly without needing to re-compile or re-run the entire proof search, which can take hours.

How is certificate tampering prevented?

NPA certificates contain cryptographically signed SHA-256 hashes of the module export data. The site generator verifies that the actual files on disk match these hashes, and the reference checker cryptographically verifies the producer signatures against the trusted keys registered in repositories.yaml.

Why are some module source blocks marked as untrusted sidecars?

To maintain strict safety, only the kernel-verified proofs and signed signatures (.npcert) represent trusted evidence. Source code text, comments, and overlays are considered metadata sidecars. Even if the source code text is altered, the underlying cryptographic check ensures the mathematically verified theorem itself remains untainted.

Can I run the checker offline?

Yes, the NPA CLI is designed to run completely offline. Once you have downloaded a package and its certificates, you can verify everything locally without any internet connection.