공개 상태
연구 및 구현 저장소
GitHub 저장소는 공개되어 있지만, 이 페이지는 배포된 서비스가 아니라 연구 및 구현 저장소를 설명합니다.
수학 랩으로 돌아가기
NPA / 인증서 우선 증명 확인
NPA: 결과를 신뢰하기 전에 증명 증거의 경계를 드러냅니다.
이 페이지는 수학 랩의 NPA 섹션을 독립적인 증거 페이지로 재구성합니다. 공개 상태, 신뢰 모델, 증명 파이프라인, 주장 관리표, 저장소, 출처, 대체물이 아니라는 명시적 경계를 함께 보여줍니다.
- 공개 상태
- 연구 저장소
- 운영 보증 서비스가 아니라 연구 및 구현으로 표시합니다.
- 공개 재확인
- 2026-07-02 / NPA v0.2.0
- 확인한 최신 git 태그: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
- 라이선스
- Apache-2.0
- Apache-2.0은 npa, npa-std, npa-mathlib에 대해 2026-07-02에 확인했습니다.
공개 재확인: 2026-07-02. NPA 저장소의 최신 git 태그는 v0.2.0이고, npa-std는 v0.1.0, npa-mathlib는 v0.1.30입니다. 패키지 README의 고정값은 저장소별 맥락으로 표시하며 하나의 NPA 버전 주장으로 합치지 않습니다.
공개 상태
무엇이 공개되어 있고, 무엇이 증거이며, 언제 재확인했는지 밝힙니다.
이 페이지는 근거를 보이게 합니다. 로컬 진실 스냅샷, 공개 저장소 출처, 최종 공개 전 재확인 날짜를 함께 표시합니다.
공개 재확인
2026-07-02
공개 원본 조회는 2026-07-02에 완료했습니다. 원래의 출처 재구성은 여전히 2026-06-21 로컬 진실 스냅샷을 사용합니다.
증거
인증서와 해시
출처 스냅샷은 정규 .npcert, certificate_hash, export_hash, axiom_report_hash, 검사기 판정을 기록합니다.
라이선스
Apache-2.0 확인됨
Apache-2.0은 npa, npa-std, npa-mathlib에 대해 2026-07-02 공개 LICENSE 메타데이터로 확인했습니다.
경계
NPA는 Lean이나 Rocq의 실무적 대체물이 아닙니다. 배포된 브라우저 점검 시뮬레이션은 NPA 자체를 실행하지 않습니다. 공개 태그, 라이선스, 저장소 공개 상태는 최종 공개 전 조회로 2026-07-02에 확인했습니다.
신뢰 경계
정규 인증서만 증거 경계를 넘깁니다.
경계의 핵심은 어떤 도구가 더 정교해 보이는지가 아닙니다. 독립 확인 뒤에 어떤 산출물이 증거가 될 수 있는지입니다.
파서, 정교화기, 전술, 자동화, 정리 검색, 플러그인, AI 시스템, 원본 파일, 재실행 파일, 정리 색인, 공개 계획, CI 상태, 릴리스 페이지, 레지스트리 메타데이터는 비신뢰 후보 영역에 머뭅니다.
증명 파이프라인 / 설명용 시뮬레이션
인증서 바이트에서 확인 증거까지의 정확한 파이프라인을 보여줍니다.
브라우저 시뮬레이션은 NPA 자체, Rust, WASM, 실제 증명 인증서를 실행하지 않습니다. 실제 산출물이 만족해야 하는 원본 없는 확인 순서를 시각화합니다.
CLI 증거 경로
npa package verify-certs --root . --checker reference --json
NPA / 감사 추적
준비됨
- 01 인증서 형식정규 .npcert 바이트 / 파싱 가능한 인증서 / 형식 확인 대기
- 02 인증서 해시인증서 바이트 / certificate_hash / 결정적 다이제스트 대기
- 03 커널 판정인증서 / 승인 또는 거부 / Rust 검증기 보고서 대기
- 04 참조 검사기해시로 고정된 인증서 / 독립적인 승인 또는 거부 / 원본 없는 검사기 보고서 대기
- 05 공리 보고서확인된 패키지 / axiom_report_hash / 가정 목록 대기
판정
아직 설명용 파이프라인을 실행하지 않았습니다.설명을 실행하면 원본 없는 확인 경로가 순서대로 표시됩니다.
주장 관리표
증거, 시간에 민감한 사실, 경계 주장을 분리합니다.
이 페이지는 느슨한 연구 문구에 의존하지 않습니다. 각 공개 문장은 로컬 진실 스냅샷, 출처, 공개 전 조치와 연결되어 있습니다.
| 주장 | 공개 문구 | 상태 | 출처 | 공개 전 조치 |
|---|---|---|---|---|
| CL-001 | NPA는 인증서 우선 방식입니다. 감사 가능한 경계는 정규 .npcert 산출물과 그 주변의 확인 경로입니다. | 검증된 공개 주장 | S01 / 2026-07-02 | README가 바뀌면 다시 검토합니다. |
| CL-002 | 2026-07-02 공개 재확인에서 NPA 저장소의 최신 git 태그가 v0.2.0임을 확인했습니다. 관련 패키지 README에는 저장소별 고정 버전이 남아 있으므로 버전 문구는 저장소별 범위로 유지합니다. | 검증된 공개 재확인 | S01 / S02 / 2026-07-02 | 태그 문구를 저장소별 범위로 유지합니다. |
| CL-003 | 로컬 진실 스냅샷에는 Rust 1.95.0 도구 체인 고정값이 기록되어 있습니다. 이 값은 마케팅 주장으로 사용하지 않습니다. | 검증됨, 시간 민감 | S01 / 2026-07-02 | 도구 체인 버전을 표시할 경우 다시 확인합니다. |
| CL-004 | NPA는 Lean이나 Rocq의 실무적 대체물이 아닙니다. 이 경계는 어떤 비교 옆에서도 계속 보여야 합니다. | 검증된 경계 주장 | S01 / S03 / S05 / 2026-07-02 | 면책 문구를 유지합니다. |
| CL-005 | npa-std와 npa-mathlib는 finitefield-org 조직에 있는 별도의 공개 정리 패키지 저장소입니다. | 검증된 공개 주장 | S01 / S02 / 2026-07-02 | 공개가 지연되거나 저장소가 바뀌면 저장소 공개 상태를 다시 확인합니다. |
| CL-006 | npa, npa-std, npa-mathlib 저장소는 각각 공개 LICENSE 메타데이터를 통해 Apache-2.0 라이선스를 표시합니다. | 검증된 공개 주장 | S01 / S02 / 2026-07-02 | 주요 릴리스 때 LICENSE를 다시 확인합니다. |
저장소와 라이선스
코드, 패키지 저장소, 조직 공개 상태를 명확히 둡니다.
저장소 링크는 공개 원본을 가리키는 포인터이며, 현재 페이지가 최신 GitHub 상태와 동기화되어 있다는 보장은 아닙니다.
4 개 저장소
finitefield-org
npa
인증서 우선 증명 지원 및 검증 도구 체인입니다.
- 라이선스
- 2026-07-02에 LICENSE에서 Apache-2.0을 확인했습니다.
- 검증
- 최신 git 태그: v0.2.0. 최신 GitHub 릴리스는 공개되어 있지 않습니다. README의 현재 도구 체인 참조: NPA_GIT_TAG=v0.2.0.
실험Rust / OCaml인증서 우선
저장소 열기
finitefield-org
npa-std
NPA 증명 원본을 위한 표준 정리 패키지 저장소입니다.
- 라이선스
- 2026-07-02에 LICENSE에서 Apache-2.0을 확인했습니다.
- 검증
- 최신 git 태그와 GitHub 릴리스: v0.1.0. README 패키지 메타데이터 버전: 0.1.0; 패키지 도구 체인 고정값: NPA_GIT_TAG=v0.1.1.
실험정리 패키지증명 원본
저장소 열기
finitefield-org
npa-mathlib
형식 수학 라이브러리 연구 저장소입니다.
- 라이선스
- 2026-07-02에 LICENSE에서 Apache-2.0을 확인했습니다.
- 검증
- 최신 git 태그: v0.1.30. 최신 GitHub 릴리스: v0.1.9. README 패키지 메타데이터 버전: 0.2.1; 패키지 도구 체인 고정값: NPA_GIT_TAG=v0.1.1.
연구형식 수학라이브러리
저장소 열기
finitefield-org
Finite Field GitHub 조직
Lab 저장소군의 공개 조직 스냅샷입니다.
- 라이선스
- 저장소별 라이선스가 적용됩니다.
- 검증
- 2026-07-02 GitHub API 조회 기준으로 npa, npa-std, npa-mathlib는 공개되어 있습니다.
공개 색인공개 상태 스냅샷출처
조직 열기
현재 검색 조건에 맞는 저장소가 없습니다.
GitHub 저장소는 공개 코드 상태의 출처입니다. 라이선스, 현재 태그, 공개 상태, 릴리스 문구는 M10-T14 최종 조회로 2026-07-02에 확인했습니다.
증명 생태계 가드
증명 도구를 비교하기 전에 역할부터 명확히 합니다.
이 표는 순위표가 아니라 역할표입니다. Lean과 Rocq는 기준이 되는 증명 보조 도구 생태계로 두고, NPA는 인증서 중심의 연구 및 구현 작업으로 소개합니다.
| 항목 | Lean | Rocq | NPA |
|---|---|---|---|
| 위치 | 오픈소스 프로그래밍 언어이자 증명 보조 도구입니다. | 오랜 연구 역사를 가진 대화형 정리 증명기입니다. | 인증서 우선 확인을 위한 연구 및 구현 저장소입니다. |
| 주요 용도 | 수학, 소프트웨어 검증, 프로그래밍. | 수학, 명세, 프로그램 검증, 추출. | 증명 인증서, 독립 확인, 작은 신뢰 기반에 관한 연구. |
| 증거 경계 | 자체 신뢰 커널과 생태계가 확인 경계를 정의합니다. | 자체 커널과 확인된 개발 결과가 확인 경계를 정의합니다. | 정규 .npcert 산출물이 생성 단계에서 확인 단계로 넘어갑니다. |
| 이 페이지의 취급 방식 | 학습, 비교, 상호 운용성을 위한 참고 기준입니다. | 학습, 비교, 형식화 방법을 위한 참고 기준입니다. | 제품 약속이 아니라 Finite Field의 연구 프로젝트입니다. |
| 경계 | 전문 지식은 여전히 필요합니다. | 전문 지식은 여전히 필요합니다. | 현재 NPA는 Lean이나 Rocq의 실무적 대체물이 아닙니다. |
출처
해석 옆에 출처 지도를 함께 공개합니다.
독자가 어떤 주장이 공개 저장소, 공식 증명 도구 사이트, 회사 맥락에서 나온 것인지 구분할 수 있도록 출처를 함께 표시합니다.
S01
finitefield-org/npa
NPA의 목적, 신뢰 모델, v0.2.0 현재 저장소 태그 문구, 명령, 저장소 구성, 라이선스에 관한 1차 출처입니다.
출처 열기 S02Finite Field GitHub 조직
2026-07-02에 확인한 공개 저장소 상태, 최신 git 태그, 릴리스 페이지, Lab 저장소군 스냅샷의 1차 출처입니다.
출처 열기 S03Lean 공식 사이트
2026-07-02에 확인한 Lean의 공개 위치 설명에 관한 1차 출처입니다.
출처 열기 S04Lean 언어 참조
2026-07-02에 확인한 의존 타입 이론과 커널 참조 맥락에 관한 1차 출처입니다.
출처 열기 S05Rocq Prover 공식 사이트
2026-07-02에 확인한 Rocq의 공개 위치 설명에 관한 1차 출처입니다.
출처 열기 S06FINITE FIELD 회사 사이트
Finite Field 브랜드와 업무 맥락에 관한 회사 출처입니다.
출처 열기01 이 페이지가 제품 보증인가요?
아니요. 여기서 NPA는 연구 및 구현 저장소로 소개됩니다.
02 NPA가 Lean이나 Rocq를 대체할 수 있나요?
아니요. NPA는 Lean이나 Rocq의 실무적 대체물이 아닙니다.
03 이 페이지가 실제 NPA 검증을 실행하나요?
아니요. 브라우저 시뮬레이션은 NPA 자체, Rust, WASM, 실제 증명 인증서를 실행하지 않습니다.
04 여기서 무엇을 증거로 보나요?
인증서 산출물, 결정적 해시, Rust 커널/검증기 결과, 원본 없는 참조 검사기 결과, 공리 보고서가 확인 측 증거입니다.
05 어떤 사실을 다시 확인해야 하나요?
현재 공개 버전, 저장소 공개 상태, 도구 체인 고정값, 라이선스 문구, 출처 문구는 2026-07-02에 재확인했습니다.