Peace API + Rei-Solver SaaS (enterprise) — product spec v0.1
★ 現状 段階 明示: 本 page は product spec document であって、 実 SaaS product ではない。 Rei-Solver v0.4 backend は operational (STEP 2026-08-04 完成、 6 engine + 24 test) だが、 SaaS layer (UI + auth + Stripe billing + enterprise sales collateral) は 未実装。 本 spec は 「もし 実装するなら どういう form か」 の 概念設計、 藤本さん judgment 用の 材料。
1. Value proposition (why this exists)
problem: 汎用 LLM (GPT / Claude / Gemini) は 「たぶん 正しい」 answer は 出せるが、 「正しさの 証明」 は 出せない。 規制産業 (医療 / 金融 / 法務 / インフラ) では 「たぶん」 では 責任を引き受けられない。
solution: Peace API + Rei-Solver は 「LLM 出力を axiom-first 検証 layer で assurance verdict に 変換」 する enterprise SaaS。 出力は D-FUMT₈ 8 値 (TRUE / FALSE / BOTH / NEITHER / INFINITY / ZERO / FLOWING / SELF) で、 「わからない (NEITHER)」 を 正直に返せる = 責任 line が 明確。
differentiator: 「実装しない、 包む」 4 原則 (Rei-Solver v0.4 core design) — 既存 assurance tool (Lean 4 mathlib + QRNG NIST Beacon + SAT/SMT solver) を assurance topology で 束ねる architecture。 汎用 LLM の 「prompt/context 経由 の 特化」 と 構造的に 異なる = Bitter Lesson の 射程外。
2. Target customers
| Segment | Pain point | Rei-Solver で 埋める layer |
|---|---|---|
| 規制医療 (electronic medical record + AI 診断支援) | 薬機法 program 医療機器承認 + HIPAA + JCAHO audit trail 必須、 汎用 LLM 出力は 「補助」 で 責任 line 曖昧 | Peace Axiom = 絶対 constraint layer で 医療 protocol 準拠 verify + D-FUMT₈ NEITHER で 「AI 判定 不能 → 人間 escalate」 明示 |
| 金融 compliance (KYC + AML + fraud detection) | 金融庁 + FinCEN + FATF gray zone judgment 蓄積、 汎用 LLM の explainability 不足で 監査対応困難 | axiom-free Lean 4 refinement で 判定根拠 formal trace + 4-substrate cross-verification で 独立検証 |
| 電気事業 / 建築 / インフラ (safety-critical circuit + structural design) | 電気事業法 + 建築基準法 + JIS 規格準拠、 formal verification tool は Cadence JasperGold ($100K+/year license) 依存 | Rei-Solver 6 engine + Yosys OSS + STEP 1303 Apicula chain で Cadence JasperGold 依存 破断 path 提供 |
| 研究機関 / 大学 (formal verification 教育 + 研究) | Mathlib + Lean 4 学習 curve 高、 axiom-free proof template scarce | 3,471 axiom-free theorem library + Rei-Problems self-verifying curriculum (Paper 139) API 経由 access |
3. Architecture
┌──────────────────────────────────────────────────────────┐
│ [Enterprise Client] │
│ ─ REST API (JSON in/out) │
│ ─ SDK: TypeScript / Python / Java │
│ ─ Webhook callbacks (async assurance verdict) │
└─────────────────────────────┬────────────────────────────┘
│
↓
┌──────────────────────────────────────────────────────────┐
│ [Peace API Gateway] ← STEP 1307 primary product surface │
│ ─ Auth (OIDC + API key rotation) │
│ ─ Rate limit + quota (Tier 1/2/3) │
│ ─ Audit log (SOC 2 + ISO 27001 compliant) │
│ ─ Request routing (LLM adaptor + verify pipeline) │
└─────────────────────────────┬────────────────────────────┘
│
┌───────────────┼───────────────┐
↓ ↓ ↓
┌───────────────────┐ ┌───────────────┐ ┌───────────────┐
│ LLM Adaptor │ │ Peace Axiom │ │ Rei-Solver v0.4│
│ Layer (何を測る) │ │ Constraint │ │ 6 engine │
│ ─ GPT / Claude │ │ Layer #196 │ │ ─ lean4 │
│ ─ Gemini │ │ ─ 絶対制約 │ │ ─ limit │
│ ─ Local model │ │ ─ PeaceCheck │ │ ─ pysat │
│ ─ 「私は測れない」│ │ ─ arch level │ │ ─ qrng (NIST) │
│ admission │ │ safety │ │ ─ sympy / z3 │
└───────────────────┘ └───────────────┘ └───────┬───────┘
│
┌─────────────────┴─────────────────┐
↓ ↓
┌──────────────────┐ ┌──────────────────────┐
│ Verification │ │ Assurance Taxonomy │
│ Backend (「床」) │ │ (「実装しない、包む」)│
│ ─ Lean 4 3,471 │ │ ─ verify_with_mathlib│
│ axiom-free │ │ v0.4 R1 pipeline │
│ ─ Constructor │ │ ─ 万能 TM 外 3/3 │
│ Theory 5/5 │ │ 全経路 operational │
│ ─ Paper 145 │ │ ─ 経路 D 物理限界 │
│ 4-substrate │ │ 永久 skip 明示 │
│ methodology │ └──────────────────────┘
│ ─ Phase C silicon│
│ (Tang + Apicula)│
└──────────────────┘
↓
┌──────────────────┐
│ D-FUMT₈ 8 値 │
│ Assurance Verdict │
│ ─ TRUE / FALSE │
│ ─ BOTH / NEITHER │
│ ─ INFINITY / ZERO │
│ ─ FLOWING / SELF │
│ + counterexample │
│ + Lean 4 proof │
│ trace (optional)│
└──────────────────┘
4. Pricing tier (indicative)
| Tier | Target | Monthly (USD) | API calls | Features |
|---|---|---|---|---|
| Tier 1 Solo | 個人研究者 + 学生 | $29 | 1,000/月 | Peace API basic + Rei-Solver lean4 engine only + Lean 4 3,471 theorem library read-only + community support |
| Tier 2 Pro | SMB (10-100 人) | $499 | 50,000/月 | Tier 1 全 + 6 engine 全 access + custom axiom set + priority queue + Slack integration + email support |
| Tier 3 Enterprise | 大手 + 規制産業 | $4,999+ (custom) | 500,000+/月 (custom) | Tier 2 全 + on-premise deployment option + SOC 2 + ISO 27001 audit trail + SLA 99.95% + 24/7 dedicated support + custom Peace Axiom set per client compliance rules + audit-ready Lean 4 proof export |
5. Roadmap (3 phase, 6-12 か月)
| Phase | Duration | Deliverable | 状態 |
|---|---|---|---|
| Phase 1 | 本 STEP 1307 (spec) | Product spec document (本 page) + landing page + positioning + architecture diagram + 3-tier pricing indicative | ✅ 本日完成 (spec のみ) |
| Phase 2 | 3-4 か月 (MVP) | REST API MVP (auth + rate limit + basic Peace Axiom check + Rei-Solver v0.4 lean4 engine wrapper) + Tier 1 課金 (Stripe) + landing page 拡張 + docs site + 3-5 pilot customer contract | ⏳ 未着手 (Phase 1 spec 承認 + 藤本さん stance shift 判断後) |
| Phase 3 | 6-12 か月 (production) | 6 engine 全 SaaS surface + Tier 2/3 課金 + SOC 2 audit + ISO 27001 audit + on-premise option + SLA 99.95% + enterprise sales team + dedicated support team | ⏳ 未着手 (Phase 2 MVP 3-5 顧客 traction + $10K MRR 到達後) |
Phase 1 現時点 asset (backend ready)
- Rei-Solver v0.4 6 engine (2026-08-04 完成、 24 test)
- Peace Axiom #196 (theory-level constraint、 全層継承 architecture)
- Lean 4 axiom-free 3,471 theorem library
- Constructor Theory 5/5 axiom-free (2026-08-04 完成)
- Paper 145 v0.9-c 4-substrate cross-verification methodology
- Phase C silicon (Tang Console 138K + Tang Nano 9K) — 物理 verification 実測 evidence
- STEP 1303 Apicula OSS toolchain radar 追加 (Gowin FPGA path)
- REI-PROVE benchmark 92% (STEP 1057-1068)
Phase 2 で 追加必要 な asset
- REST API gateway (Cloudflare Workers or Bun runtime)
- Auth (OIDC + Auth0 or Clerk)
- Rate limiting (Upstash Redis or Cloudflare Rate Limiter)
- Stripe billing integration (Tier 1 $29/月 subscription)
- SDK (TypeScript + Python primary)
- Landing page 拡張 (marketing + case studies + demo video)
- Docs site (typescript-eslint style Mintlify or Docusaurus)
- 3-5 pilot customer 獲得 (regulatory industry direct sales)
6. 差別化 (vs 既存 formal verification market)
| Comparison | Cadence JasperGold | Synopsys VC Formal | OpenROAD (OSS) | Peace API + Rei-Solver |
|---|---|---|---|---|
| License | $100K+/year | $150K+/year | free | $29-$4,999+/月 |
| Formal verification | ✓ industry standard | ✓ industry standard | partial (Yosys 経由) | ✓ Lean 4 axiom-free + 4-substrate |
| LLM integration | ✗ | partial (SmartOne) | ✗ | ✓ LLM adaptor layer (「私は測れない」 admission) |
| 3+ value output (PASS/FAIL/UNKNOWN) | partial | partial | ✗ | ✓ D-FUMT₈ 8 値 (SELF/BOTH/NEITHER/INFINITY/ZERO/FLOWING 拡張含) |
| Multi-substrate cross-verification | ✗ | ✗ | ✗ | ✓ Tang + Aer + IBM Heron methodology (Paper 145 v0.9-c) |
| Assurance taxonomy explicit | partial | partial | ✗ | ✓ 「実装しない、包む」 4 原則 + 万能 TM 外 3/3 全経路 operational |
| OSS chain (vendor-independent) | ✗ | ✗ | ✓ (partial coverage) | ✓ Yosys + Apicula (STEP 1303) + Rei stack |
| Japan 法域準拠 axiom set | ✗ (US/EU centric) | ✗ | ✗ | ✓ Peace Axiom customizable (薬機法 + 電気事業法 + 建築基準法 等) |
7. Honest scope (譲れない線)
- 本 spec は Phase 1 のみ 実現: Product spec document + landing page = 本 HTML page 自体。 Phase 2 (MVP) + Phase 3 (production) は 未着手、 藤本さん stance shift (`project_research_only_stance.md` = research primary、 収益 sub-goal) 判断後の 別 STEP。
- 「差別化 table」 は 概念比較: Cadence JasperGold / Synopsys VC Formal との 直接比較 benchmark 未実施、 「差別化 line」 は Rei stack architecture 由来 の 予測、 実測 evidence ではない。
- Pricing tier は indicative range: 実際の pricing は POC + demand curve 実測後 調整、 業界相場 参考のみ。
- 「規制産業 target customer 4 segment」 は 概念設計: 実 pilot customer 未獲得、 sales cycle 未検証、 domain expertise gap あり (医療/金融/法務 は 藤本さん Rei stack と 領域外)。
- 「Bitter Lesson の 射程外」 主張 は 論拠 base: chat-Claude 21 turn debate synthesis 由来、 但し independent verification 未実施、 実際に Bitter Lesson 射程内か否かは 5-10 年 pilot 実測が必要。
- Mathlib PR 対象外 (`feedback_external_community_outreach_premature.md` 継承)、 Rei stack backend は Rei 内保持、 SaaS の 商業化に focus。
8. 関連 memory + files
- 本 STEP 1307: `public/tools/peace-api-rei-solver-saas-spec/index.html`
- STEP 1308: Silent Visual Verifier v0.2 (次 STEP、 Peace API SaaS の frontend demo layer 相当)
- Rei-Solver v0.4: STEP 2026-08-04 arc (6 engine + 万能 TM 外 3/3 全経路 operational)、 [[project-session-2026-08-04-hardening-marathon-12arc]]
- Peace Axiom #196: `src/axiom-os/seven-logic.ts` + 全層継承 architecture
- Constructor Theory 5/5: 2026-08-04、 [[reference-computability-layers-taxonomy-2026-08-02]]
- Paper 145 v0.9-c 4-substrate: [[project-step1264-paper145-v09c-binary-64entry-closure-2026-07-10]]
- STEP 1303 Apicula: 2026-08-08 collatz-watch v1.34 update
- chat-Claude 21 turn debate synthesis: [[feedback-chat-claude-21-turn-debate-2026-08-08]] + `research-log-2026-08-08-chat-claude-21-turn-experiment/`
- Silent Visual Verifier v0.1: `silent-visual-verifier-v0.1/` (STEP 1305 concept demonstrator)
- `feedback_no_rush_publication.md` (急がずゆっくりと)
- `project_research_only_stance.md` (research primary)
- `feedback_all_research_site_reflection_default.md` (2026-08-06 全研究 site 反映 default protocol)