Peace API + Rei-Solver SaaS (enterprise) — product spec v0.1

STEP 1307 / concept 段階 (実 SaaS infra 未実装) / 「assurance-first inference paradigm」 を enterprise compliance / verification 市場 に 提示する 概念設計書 / 藤本伸樹 / 2026-08-08

★ 現状 段階 明示: 本 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

SegmentPain pointRei-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 scarce3,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)

TierTargetMonthly (USD)API callsFeatures
Tier 1 Solo個人研究者 + 学生$291,000/月Peace API basic + Rei-Solver lean4 engine only + Lean 4 3,471 theorem library read-only + community support
Tier 2 ProSMB (10-100 人)$49950,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

★ 価格は 業界相場 (Cadence JasperGold $100K+/year、 Palantir Foundry $150K+/年、 Snowflake $50K+/年) 参考の indicative range、 実際は POC + demand curve 実測後 調整。

5. Roadmap (3 phase, 6-12 か月)

PhaseDurationDeliverable状態
Phase 1本 STEP 1307 (spec)Product spec document (本 page) + landing page + positioning + architecture diagram + 3-tier pricing indicative✅ 本日完成 (spec のみ)
Phase 23-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 36-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)

Phase 2 で 追加必要 な asset

6. 差別化 (vs 既存 formal verification market)

ComparisonCadence JasperGoldSynopsys VC FormalOpenROAD (OSS)Peace API + Rei-Solver
License$100K+/year$150K+/yearfree$29-$4,999+/月
Formal verification✓ industry standard✓ industry standardpartial (Yosys 経由)✓ Lean 4 axiom-free + 4-substrate
LLM integrationpartial (SmartOne)✓ LLM adaptor layer (「私は測れない」 admission)
3+ value output (PASS/FAIL/UNKNOWN)partialpartial✓ 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 explicitpartialpartial✓ 「実装しない、包む」 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 (譲れない線)

  1. 本 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。
  2. 「差別化 table」 は 概念比較: Cadence JasperGold / Synopsys VC Formal との 直接比較 benchmark 未実施、 「差別化 line」 は Rei stack architecture 由来 の 予測、 実測 evidence ではない。
  3. Pricing tier は indicative range: 実際の pricing は POC + demand curve 実測後 調整、 業界相場 参考のみ。
  4. 「規制産業 target customer 4 segment」 は 概念設計: 実 pilot customer 未獲得、 sales cycle 未検証、 domain expertise gap あり (医療/金融/法務 は 藤本さん Rei stack と 領域外)。
  5. 「Bitter Lesson の 射程外」 主張 は 論拠 base: chat-Claude 21 turn debate synthesis 由来、 但し independent verification 未実施、 実際に Bitter Lesson 射程内か否かは 5-10 年 pilot 実測が必要。
  6. Mathlib PR 対象外 (`feedback_external_community_outreach_premature.md` 継承)、 Rei stack backend は Rei 内保持、 SaaS の 商業化に focus。

8. 関連 memory + files