構成員の誰もが今日辞められる会社を作る｜bounded model checking

会社に所属する人や会社を創業する人は、永遠に続くアルゴリズムを求めてしまいがちであるが、永遠に続くアルゴリズムあるいは、いつアルゴリズムが止まるかを判定する汎用アルゴリズムは数学的に存在しないことがアランチューリングにより1936年に証明されている。未来は予測できない、永遠はないというのは自明の理なのであるが、毎日の判断になると、すぐに辞められると困る、いなくなると困るというコメントがたくさん出る。

人がすぐ辞めても高速で回転し、純利益を出し続けるアルゴリズムがあるのであれば、構成要素としての人間が入れ替わっても問題ない。どんなポジションであれ、誰かが辞めるとシステムが止まってしまうような収益構造である方が課題である。実際、会社というのはシステムなので、意外と、想像以上にいなくなったとしても問題ないケースがほとんどである。

辞めたいと言われた日に、その人を即日辞めさせられる組織の方が成熟度が高い。特に会社が急成長するとき、暗闇の中を手探りで進み、尚且つその速度がジェットコースターのように早いと、ほとんどの人は恐怖や不安を感じるものである。辞めたくなるということは情報量が爆発しているので、エネルギーに耐えらないということでもある。その人の限界にすでに達しているのである。個人の能力は限られているので、会社の急成長はどんな人でもキャパシティオーバーになるため、ネットワークノードとしての問題の定式化ができないと容易に消耗、バーンアウトする。

例えば株主であっても明日すぐに売り抜けることが重要である。いざ売ろうとしたら価値がつかないとか、待ってくれと言われるようであれば柔軟性に欠ける。このautonomous versatility、自律的な汎用性、臨機応用性を身につけるというのは普段からworst scenario case、最悪のシナリオのシミュレーションやlower bound（境界下限）の閾値を特定するbounded model checking（破綻する検証回数kの深さ）の日常化が必要である。

1. 概念の原典：米軍規格「MIL規格」（1940〜1950年代）

SPOF（Single Point of Failure）という思想が初めて明文化され、システム設計の必須要件となったのは、第二次世界大戦中から戦後にかけてのアメリカ軍の規格（MIL規格：Military Standard）である。

当時、レーダーやミサイル、爆撃機などの電子機器が複雑化するにつれ、「たった一つの真空管が壊れただけで、機体全体が墜落する」という問題が多発した。

• 源流となる学問： これを解決するために生まれたのが「信頼性工学（Reliability Engineering）」。
• 初期の文書： 1950年代に制定された米軍規格（例えば、のちにFMEA［Failure Mode and Effects Analysis 故障モード影響解析］へと発展する軍用手続き）のなかで、「システムの全壊を招く、冗長性のない単一の構成要素」を排除するための設計基準として、この概念が法制化・標準化された。

2. 思考の原典：フォン・ノイマンの「信頼性の高い組織の構築」（1956年）

計算機科学（Computation）の文脈において、SPOFを排除する（＝不確実な部品を集めて、確実なシステムを作る）というアプローチの理論的基礎を築いたのは、コンピューターの元祖であるジョン・フォン・ノイマンである。

• 原著論文： “Probabilistic Logics and the Synthesis of Reliable Organisms from Unreliable Components” (1956) （信頼性の低い構成要素から、信頼性の高い組織を合成する確率論的論理）
• https://static.ias.edu/pitp/archive/2012files/Probabilistic_Logics.pdf

ノイマンはこの論文で、コンピュータの真空管（あるいは人間の脳のニューロン）が確率的に必ず故障する（＝SPOFになり得る）としても、それらを冗長化し、多数決（マジョリティ・ロジック）のネットワークを組めば、システム全体としては絶対にエラーを起こさないようにできるということを数学的に証明した。

これは、「個々の人間はキャパシティオーバーでいつ辞める（壊れる）か分からないが、ネットワーク構造によってシステム全体の停止を防ぐ」という、経営のReliability Engineeringの数学的ベースである。

工学的なリスク管理手法を、より厳密に、複雑性理論化した計算科学的アプローチがBMCである。

1. FMEAとBounded Model Checkingの共通構造

FMEAが「人間が経験ベースで故障のパターン（故障モード）を洗い出す」のに対し、BMCは「システムがとり得る状態の遷移を数学的（論理式）に展開し、最悪のシナリオ（反例：Counterexample）を自動的・網羅的に検出する」という違いがある。

2. BMCの視点で見る「組織の検証」

「急成長時の情報爆発とバーンアウト」をBMCのフレームワークで定式化する。

• 状態（States）： 組織の処理している情報量、売上、各ノード（人員）の負荷レベル。
• 遷移（Transitions）： 日々の業務実行、人員の即日退職、新規採用、案件の流入。
• 境界（Bound = k）： 「今後kステップ（例：3ヶ月間、あるいは15プロジェクト先まで）」という限定された未来。
• 安全特性（Safety Property）： 「純利益 ＞ 0」かつ「コアシステムが停止しない」。

BMCのアルゴリズムは、この現在の状態から「kステップ以内」に、安全特性を破るような状態（＝純利益がマイナスになる、あるいはSPOFが抜けてシステムが止まるという最悪のシナリオ）が存在するかどうかを、SATソルバ（論理式を満たす解を見つけるプログラム）のように徹底的に探索する。

もし「3ステップ先に、キーマンAが辞めるとシステムが全壊する」というルート（反例）が見つかれば、それはLower Bound（下限の境界線）を突破したことを意味するため、アルゴリズムの段階でそのルートを遮断するか、Aのノードを冗長化するコードに書き換える必要がある。

3. FMEAとBMCが融合した「自律的汎用性（Autonomous Versatility）」

FMEAの影響度評価の感受性が高く、BMCの境界線を特定する数理的アプローチが日常化している組織は、次のような超高速なフィードバックループが回っている。

【自律的汎用性（Autonomous Versatility）のループ】
 1. [FMEA的思考] ──＞ 「明日、全営業が即日退職したらどうなる？」という故障モードを定義
 2. [BMC的思考] ───＞ 直近のkステップで、純利益のLower Bound（下限）を下回るか検証
 3. [コード変更] ───＞ 下回るなら、即座に「自動フォームとAI追客」へルーティングを切り替える

このレベルに達した組織にとって、従業員の「辞めたい」という一言は、システムを揺るがす危機（パニック）ではなく、事前にBMCで検証済みの、想定内の条件分岐（If-Then）が一つ発動したというだけの淡々としたイベントである。

「未来は予測できない（停止問題）」という暗闇のなかで、ジェットコースターのような速度で突っ走る組織をコントロールする唯一の方法は、FMEA的にバグの形を予見し、BMC的に破綻の下限（Lower Bound）をステップごとにProbablisticに検証し続けること（Arthur-Melin）。このBounded（限定された範囲）での検証をリアルタイムに繰り返し、その都度システムを書き換えられる組織は、強靭で、高い資本効率を叩き出し続けるアルゴリズムを持った組織と言える。