NPAは通常のLeanカーネルのチェックとどう違うのですか？
標準のLeanチェックはローカルマシン上でファイルをコンパイルして検証します。NPAはこれらの検証済みのコンパイル出力を取り込み、決定論的ハッシュとともに暗号署名付き証明書（.npcert）にパッケージ化します。これにより、第三者は数時間かかる再コンパイルや証明探索を再実行することなく、検証ステータスを即座に監査できます。
証明書の改ざんはどのように防がれますか？
NPA証明書には、モジュールエクスポートデータの暗号署名付きSHA-256ハッシュが含まれています。サイトジェネレータは、ディスク上の実際のファイルがこれらのハッシュと一致することを確認し、リファレンスチェッカーは、repositories.yamlに登録されている信頼できるキーに対してプロデューサーの署名を暗号的に検証します。
一部のモジュールソースコードが信頼されていないサイドカーデータとされているのはなぜですか？
厳格な安全性を維持するため、カーネルが検証した証明と署名された証明書（.npcert）のみが信頼できる証拠となります。ソースコードのテキスト、コメント、ドキュメントは「メタデータサイドカー（補足アセット）」とみなされます。仮にソースコードのテキストが改ざんされたとしても、数学的に検証された定理自体は暗号的チェックによって保護されたままです。
チェッカーをオフラインで実行することはできますか？
はい、NPA CLIは完全にオフラインで動作するように設計されています。パッケージと証明書をダウンロードすれば、インターネット接続なしでローカルですべてを検証できます。