correctness-assurance

Compare original and translation side by side

🇺🇸

Original

English

🇨🇳

Translation

Chinese

Correctness Assurance

correctness assuranceは、単一の手法で「正しさ」を保証することではない。

何を正しいと呼ぶのかを性質ごとに分解し、その性質に対して最小十分なassurance mechanismを割り当て、保証できた範囲・保証していない範囲・前提を明示する。

形式検証を自動的に優先しない。型・静的解析・テスト・runtime check・reviewで十分な性質にproofを持ち込まない。一方で、有限個のテストでは本質的に届かない全称的な性質を「テストが多いから十分」と扱わない。

correctness assurance 并不是通过单一方法保证“正确性”。

将每种性质分别定义为“正确”，为每种性质分配最小充分的 assurance mechanism，并明确已保证的范围、未保证的范围以及前提。

不应自动优先采用 formal verification。不应将 proof 引入那些通过类型、静态分析、测试、runtime check 和 review 已足以保证的性质。另一方面，不应因为测试数量多，就把有限测试本质上无法覆盖的全称性质视为已经得到充分保证。

1. いつ使うか

1. 何时使用

次のいずれかがある場合に使用する。

配列添字、範囲、長さ、offset、cursor、partition等の境界条件がある
sentinel / optional state / partial stateを最終的に解消する必要がある
state machineで到達不能状態や遷移制約がある
sort / merge / search / scheduler / parser / allocator等に構造的不変条件がある
「事前条件を満たすすべての入力」で成り立ってほしい性質がある
property-based testや差分テストでも入力空間を有限標本としてしか扱えない
破れるとpanic / trap / out-of-bounds / corruption / wrong-stateになる
型で責任箇所を狭められるが、そのconstruction function自体の正しさが残る
runtime semanticsとverification/model semanticsの差がriskになる
AI生成・変更されるコードに、機械可読なcontractを置く価値がある

次だけを理由に起動しない。

UIの見た目だけを確認したい
external API / DB / network wiringだけを確認したい
product semantics自体がまだ決まっていない
重要な性質を具体的なpredicateとして書けない
formal verification toolを使ってみたいだけ

出现以下任一情况时使用。

存在数组索引、范围、长度、offset、cursor、partition 等边界条件
最终必须消除 sentinel / optional state / partial state
state machine 中存在不可达状态或转换约束
sort / merge / search / scheduler / parser / allocator 等存在结构性不变量
希望某项性质对“满足前置条件的所有输入”都成立
即使使用 property-based test 或差分测试，也只能将输入空间作为有限样本来处理
一旦破坏就会导致 panic / trap / out-of-bounds / corruption / wrong-state
类型可以缩小责任范围，但 construction function 本身的正确性仍未得到保证
runtime semantics 与 verification/model semantics 之间的差异会带来 risk
对 AI 生成或修改的代码而言，添加机器可读的 contract 具有价值

不要仅因以下原因启动本流程。

只想确认 UI 的外观
只想确认 external API / DB / network wiring
product semantics 本身尚未确定
无法将重要性质写成具体的 predicate
只是想试用 formal verification tool

2. 最初に「正しさ」を分解する

2. 首先分解“正确性”

実装を見る前に、必要な性質を曖昧な「正しい」から分離する。

最低限、該当するものを列挙する。

在查看实现之前，将所需性质从模糊的“正确”中分离出来。

至少应枚举适用的性质。

Structure / construction

Structure / construction（结构与构造）

例:

この値は特定constructorを通してのみ生成される
invalid variantを呼び出し側へ渡せない
schema / shape / enum stateが正しい

主に型・visibility・module boundaryで担保する。

示例：

该值只能通过特定 constructor 生成
无法将 invalid variant 传递给调用方
schema / shape / enum state 正确

主要由类型、visibility 和 module boundary 提供保证。

Range / bounds

Range / bounds（范围与边界）

例:

```
0 <= index < length
```
offsetがbuffer範囲内
selected rangeが空間外へ出ない
integer resultがruntime表現範囲内

型だけで表現できない場合、contract / static analysis / runtime assertion / proofを検討する。

示例：

```
0 <= index < length
```
offset 位于 buffer 范围内
selected range 不会超出空间范围
integer result 位于 runtime 表示范围内

如果仅靠类型无法表达，应考虑 contract / static analysis / runtime assertion / proof。

Totality / completion

Totality / completion（完备性与完成状态）

例:

completion後にsentinelが残らない
```
Option
```
/ nullable stateがfinal phaseではすべて解消される
partial mappingがcompleteになる

「特定関数を通った」と「その関数が本当にcompleteにした」を分ける。

示例：

completion 后不残留 sentinel
```
Option
```
/ nullable state 在 final phase 全部得到消除
partial mapping 变为 complete

应区分“经过了特定函数”和“该函数确实完成了处理”。

State transition

State transition（状态转换）

例:

forbidden transitionが存在しない
terminal stateから通常stateへ戻らない
event sequenceに対してinvariantが保存される

型、state-machine test、model checking、formal verification等を候補にする。

示例：

不存在 forbidden transition
无法从 terminal state 返回普通 state
针对 event sequence，invariant 始终得到保持

候选手段包括类型、state-machine test、model checking 和 formal verification 等。

Ordering / uniqueness / preservation

Ordering / uniqueness / preservation（顺序性、唯一性与保持性）

例:

sort後に順序が保たれる
stable orderingが必要
keyが重複しない
length / membership / correspondenceが処理前後で保存される

示例：

sort 后仍保持顺序
需要 stable ordering
key 不重复
length / membership / correspondence 在处理前后保持不变

Arithmetic / numeric model

Arithmetic / numeric model（算术与数值模型）

例:

overflowしない
saturation semanticsを守る
floating-point orderingの差で結果順序を壊さない
fixed-width integerと数学整数を混同しない

ここはverification modelとruntime modelの一致確認を必須にする。

示例：

不发生 overflow
遵守 saturation semantics
不因 floating-point ordering 差异破坏结果顺序
不混淆 fixed-width integer 与数学整数

这里必须确认 verification model 与 runtime model 保持一致。

Semantic correctness

Semantic correctness（语义正确性）

例:

最適解である
推薦結果が正しい
business rule上正解である
user intentを満たす

構造的安全性と分離する。「クラッシュしない」を「答えが正しい」に拡張しない。

示例：

是最优解
推荐结果正确
符合 business rule
满足 user intent

应将其与结构性安全性分开。不能将“不崩溃”扩展为“答案正确”。

3. Assurance mechanismをproperty単位で選ぶ

3. 按 property 选择 assurance mechanism

各propertyについて、最小十分な手段を選択する。

Mechanism	強い領域	単独では弱い領域
Type system	shape、construction boundary、invalid stateの排除	collection全体の内容、不変条件、constructor内部の仕事
Static analysis	language/toolがmodelできるdefect class	runtime integration、tool model外
Runtime assertion	実行したcaseのpre/post condition違反	未実行入力への全称保証
Unit test	局所behavior、境界値、machine semantics	入力空間全体
Property-based test	広い入力探索、反例発見	全入力保証ではない
Differential test	既存実装との互換性、移植	oracle自体の誤り、未実行入力
Integration/E2E	real boundaryとsystem behavior	局所invariantの網羅
Formal verification / model checking	model内の全入力・全状態に対するproperty	specification error、model外のruntime semantics
Review	specificationの十分性、意図、assumption妥当性	機械的網羅性

原則:

同じpropertyを複数手法で無意味に重複させるのではなく、異なるfailure classを補完する。

ただし高risk propertyでは独立な二重化が有効な場合がある。たとえばproofしたpredicateと同義のruntime checkerを別実装で持ち、model/runtimeの食い違いを検出する。

为每项 property 选择最小且充分的手段。

Mechanism	强项领域	单独使用时的薄弱领域
Type system	shape、construction boundary、排除 invalid state	collection 的整体内容、不变量、constructor 内部的工作
Static analysis	language/tool 能够建模的 defect class	runtime integration、tool model 之外的部分
Runtime assertion	检测已执行 case 的 pre/post condition 违规	对未执行输入提供全称保证
Unit test	局部 behavior、边界值、machine semantics	整个输入空间
Property-based test	广泛探索输入、发现反例	并非对所有输入的保证
Differential test	与现有实现的兼容性、移植	oracle 本身的错误、未执行输入
Integration/E2E	真实 boundary 与 system behavior	局部 invariant 的全面覆盖
Formal verification / model checking	model 内所有输入、所有状态上的 property	specification error、model 之外的 runtime semantics
Review	specification 的充分性、意图、assumption 的合理性	机械化的全面覆盖

原则：

不要用多种方法无意义地重复保障同一个 property，而应让它们补全不同的 failure class。

不过，对于高 risk property，独立的双重保障有时是有效的。例如，将与已 proof 的 predicate 等价的 runtime checker 作为独立实现，用于检测 model 与 runtime 之间的偏差。

4. Assurance mapを作る

4. 构建 Assurance map

実装前または変更前に、対象propertyごとに次を記録する。

text

Property:
  completion後に未決定sentinelが残らない

Scope:
  事前条件を満たすすべてのmapping input

Mechanism:
  formal verification

Supporting mechanisms:
  runtime checker
  boundary unit tests

Assumptions:
  input length > 0
  first/last entries are assigned
  verification modelのinteger semanticsが対象propertyに十分

Not covered:
  assigned valueが有効な参照添字であること
  floating-point側の候補選択の正しさ
  global optimum

「Aを証明した」からB・Cまで保証したように書かない。

在实现前或变更前，为目标 property 记录以下内容。

text

Property:
  completion後に未決定sentinelが残らない

Scope:
  事前条件を満たすすべてのmapping input

Mechanism:
  formal verification

Supporting mechanisms:
  runtime checker
  boundary unit tests

Assumptions:
  input length > 0
  first/last entries are assigned
  verification modelのinteger semanticsが対象propertyに十分

Not covered:
  assigned valueが有効な参照添字であること
  floating-point側の候補選択の正しさ
  global optimum

不要将“已证明 A”写成仿佛也保证了 B 和 C。

5. Contractを具体的にする

5. 将 Contract 具体化

formal verificationを使うかどうかに関係なく、重要なpropertyは可能なら次へ分解する。

precondition / requires
postcondition / ensures
invariant
frame / preservation property
termination condition
model assumption

悪い例:

text

mapping is valid

良い分解:

text

forall i in [0, map.length):
  map[i] != SENTINEL

forall i in [0, map.length):
  0 <= map[i] < reference.length

result.length == input.length

sentinelが消えたことと、有効なindexだけが入っていることは別propertyとして扱う。

无论是否使用 formal verification，重要 property 都应在可能的情况下分解为：

precondition / requires
postcondition / ensures
invariant
frame / preservation property
termination condition
model assumption

糟糕的示例：

text

mapping is valid

良好的分解：

text

forall i in [0, map.length):
  map[i] != SENTINEL

forall i in [0, map.length):
  0 <= map[i] < reference.length

result.length == input.length

应将“sentinel 已消失”和“仅包含有效 index”作为不同的 property 处理。

6. Preconditionをcall chainで閉じる

6. 沿 call chain 闭合 precondition

contractのpreconditionはruntime checkとは限らない。

text

caller
  ↓ must establish P
function f requires P
  ↓ proves Q
caller uses Q

次を確認する。

preconditionはどこで成立するのか
呼び出し側でもproof/static checkされるのか
runtime validationが必要なのか
external inputから来る場合、trusted boundaryはどこか
call chain途中で保証が切れていないか

「functionがproof済み」でも、precondition違反のcallが可能ならその実行は保証外である。

contract 的 precondition 不一定意味着 runtime check。

text

caller
  ↓ must establish P
function f requires P
  ↓ proves Q
caller uses Q

需要检查以下事项：

precondition 在何处成立
调用方是否也会进行 proof/static check
是否需要 runtime validation
如果输入来自外部，trusted boundary 位于何处
保证是否在 call chain 中途断开

即使 function 已经 proof，如果仍可能调用违反 precondition 的路径，该执行仍处于保证范围之外。

7. 検証困難なら先にboundaryを疑う

7. 难以验证时，先检查 boundary

重要なinvariantが検証しにくい場合、すぐにcontractを弱めない。

次が混在していないか確認する。

I/O
mutable shared state
floating-point decision
external service
nondeterminism
time
random
UI/event wiring
index/range arithmetic
pure transformation

可能なら、

text

unverified / environment-dependent layer
        ↓ explicit boundary
small verifiable core
        ↓
unverified / environment-dependent layer

へ分離する。

典型例:

floating-pointで「どれを選ぶか」を決める
integer coreで「選ばれた位置を安全に扱う」
external layerで結果をI/Oへ接続する

ただし、proofの都合だけで不必要なallocation、copy、latency、複雑化を入れる場合は、その設計コストを明示する。

如果重要 invariant 难以验证，不要立即弱化 contract。

检查以下内容是否混杂在一起：

I/O
mutable shared state
floating-point decision
external service
nondeterminism
time
random
UI/event wiring
index/range arithmetic
pure transformation

如果可能，应分离为：

text

unverified / environment-dependent layer
        ↓ explicit boundary
small verifiable core
        ↓
unverified / environment-dependent layer

典型示例：

使用 floating-point 决定“选择哪一个”
使用 integer core 安全处理“被选中的位置”
由 external layer 将结果连接到 I/O

但是，如果仅仅为了 proof 而引入不必要的 allocation、copy、latency 或复杂化，则必须明确说明相应的设计成本。

8. Formal verificationを選ぶ基準

8. 选择 Formal verification 的标准

次が揃うほど適用価値が高い。

propertyが明確なpredicateとして書ける
全入力・全状態に対する保証が本当に必要
test enumerationでは本質的に保証できない
pureまたは副作用が限定されたcoreへ分離できる
index/range/state/ordering等の構造的property
failure impactが高い
solver/modelが必要なlanguage featureを正しく扱える
proof maintenance costに見合う

適用価値が低い、または先に別手段を選ぶ例:

specificationが曖昧
UI appearance
external integration correctness
modelが対象featureを表現できない
rapidly changing exploratory codeでproperty自体が未確定
unit/property testで十分な局所logic
proofを通すこと自体が目的化している

以下条件越齐备，应用价值越高。

property 可以明确写成 predicate
确实需要对所有输入、所有状态提供保证
通过 test enumeration 本质上无法获得保证
可以将逻辑分离为 pure core，或副作用受到限制
涉及 index/range/state/ordering 等结构性 property
failure impact 较高
solver/model 能正确处理所需的 language feature
收益足以覆盖 proof 的 maintenance cost

应用价值较低，或应优先选择其他手段的示例：

specification 含糊
UI appearance
external integration correctness
model 无法表达目标 feature
在快速变化的探索性代码中，property 本身尚未确定
unit/property test 已足以覆盖局部 logic
将“通过 proof”本身视为目的

9. Verification modelとruntime semanticsを照合する

9. 对照 Verification model 与 runtime semantics

proofの前後で必ずmodel boundaryを確認する。

最低限:

integerはmathematical integerかfixed-width machine integerか
overflow / underflowはmodelされるか
floating-pointはIEEE 754としてmodelされるか、未対応か
division / modulo / shift semanticsはruntimeと同じか
pointer / alias / mutation / memory modelは同じか
concurrency / atomicity / orderingはmodelされるか
exceptions / panic / trapはmodelされるか
compiler target差、Wasm/JS/native差があるか
library / host functionはaxiom扱いか、verified implementationか

例:

text

proof model: unbounded mathematical Int
runtime: signed 32-bit Int

なら、結果範囲のcontractだけでは途中式のoverflow安全性を保証できない場合がある。

proof greenとmachine-safeを同義にしない。

在 proof 前后都必须检查 model boundary。

至少需要确认：

integer 是 mathematical integer 还是 fixed-width machine integer
overflow / underflow 是否被建模
floating-point 是否按 IEEE 754 建模，或尚未支持
division / modulo / shift semantics 是否与 runtime 相同
pointer / alias / mutation / memory model 是否相同
concurrency / atomicity / ordering 是否被建模
exceptions / panic / trap 是否被建模
是否存在 compiler target 差异、Wasm/JS/native 差异
library / host function 是作为 axiom 处理，还是已有 verified implementation

示例：

text

proof model: unbounded mathematical Int
runtime: signed 32-bit Int

在这种情况下，仅靠结果范围的 contract，可能无法保证中间表达式的 overflow 安全性。

不要将 proof green 与 machine-safe 等同。

10. Specification自体をadversarialにreviewする

10. 对 Specification 本身进行对抗性 Review

solverは「書いた仕様」を検証する。必要だった仕様を自動で発見してはくれない。

reviewでは少なくとも次を行う。

solver 只会验证“已经写出的规格”，不会自动发现原本需要的规格。

review 至少应执行以下操作。

Counterexample challenge

contractを満たすが、実際には受け入れたくない値を探す。

例:

text

property: value != -1
counterexample: -2

この反例が危険なら、必要propertyは

0 <= value < n

のように強化する。

寻找满足 contract、但实际上并不希望接受的值。

示例：

text

property: value != -1
counterexample: -2

如果该反例存在危险，应将所需 property 强化为

0 <= value < n

。

Vacuity challenge

preconditionが強すぎて、実質的に何も保証していない可能性を確認する。

检查 precondition 是否过强，以至于实际上没有提供任何实质保证。

Missing-dimension challenge

safetyだけでlivenessを忘れていないか
totalityだけでrange validityを忘れていないか
local correctnessだけでpreservationを忘れていないか
resultだけでintermediate overflowを忘れていないか

是否只考虑 safety，而忘记了 liveness
是否只考虑 totality，而忘记了 range validity
是否只考虑 local correctness，而忘记了 preservation
是否只考虑 result，而忘记了 intermediate overflow

Oracle challenge

differential testではreference implementation自体を無条件に正しいと扱わない。

在 differential test 中，不要无条件地将 reference implementation 视为正确。

11. Loop / recursive invariantは必要な性質から逆算する

11. 从所需性质反推 Loop / recursive invariant

強いinvariantを大量に入れれば良いわけではない。

まずpostconditionに必要なpropertyを特定し、そのpropertyを各stepで保存できる最小限のinvariantを置く。

例:

text

post:
  all entries are assigned

loop invariant:
  all entries before cursor are assigned

必要以上に値そのものを追うことでsolver costやmaintenance costが増える場合がある。

一方で、弱すぎるinvariantでproofを通すために本来必要なpropertyを削ってはいけない。

并不是加入越强越多的 invariant 就越好。

首先确定 postcondition 所需的 property，再设置能在每个 step 保持该 property 的最小 invariant。

示例：

text

post:
  all entries are assigned

loop invariant:
  all entries before cursor are assigned

如果过度追踪值本身，solver cost 和 maintenance cost 可能会增加。

另一方面，不能为了通过 proof 而将过弱的 invariant 弱化到丧失原本必要的 property。

12. Tool resultの意味を正確に読む

12. 准确解读 Tool result

formal toolのstatusを過大解釈しない。

proved / valid: 指定model・assumption・contractのもとで成立
invalid / counterexample: propertyが偽であるevidenceになり得る
timeout / unknown: この設定では結論が出なかっただけ
unsupported: model外。propertyが正しいとも間違いとも言っていない

timeoutを「バグがある証拠」と扱わない。 proof obligation数を「保証の強さ」のmetricとして使わない。

不要过度解释 formal tool 的 status。

proved / valid：在指定的 model、assumption 和 contract 下成立
invalid / counterexample：可能构成 property 为假的 evidence
timeout / unknown：仅表示在当前配置下无法得出结论
unsupported：位于 model 之外，既不能说明 property 正确，也不能说明其错误

不要将 timeout 视为“存在 bug 的证据”。不要将 proof obligation 的数量用作“保证强度”的 metric。

13. Runtime verificationを残す判断

13. 判断是否保留 Runtime verification

proof済みでもruntime checkやtestを残す価値がある。

残す候補:

machine integer境界
floating-point behavior
compiler/backend差
Wasm/JS/native差
serialization
FFI
generated code
host API
unsafe code
proof modelで抽象化したboundary
contractと同義のindependent runtime checker

contractがcompile artifactへ残らないtoolでは、必要ならruntime safety checkを別途設計する。

即使已经 proof，仍可能有必要保留 runtime check 或 test。

候选场景：

machine integer 边界
floating-point behavior
compiler/backend 差异
Wasm/JS/native 差异
serialization
FFI
generated code
host API
unsafe code
proof model 中被抽象化的 boundary
与 contract 等价的 independent runtime checker

如果 contract 不会保留在 compile artifact 中，则应在必要时单独设计 runtime safety check。

14. Evidence

assuranceの結果は最低限次で報告する。

既知のmodel gapが存在する場合、
Known model gaps
項目に必ず記載する。 gapがないと確認できる場合のみ「なし」と明記する。

text

Correctness properties
- P1: ...
- P2: ...

Verified / assured
- P1: formal proof, tool/version, result
- P2: type-level construction boundary

Runtime-tested
- integer boundary cases
- differential compatibility
- target backend behavior

Assumptions
- ...
- ...

Not verified
- ...
- ...

Known model gaps
- ...
- ...

Evidence
- command
- artifact
- commit/SHA
- toolchain/version

「tests green」「proof green」だけで終了しない。

assurance 的结果至少应按以下方式报告。

如果存在已知的 model gap，必须将其列在
Known model gaps
项中。只有在能够确认不存在 gap 时，才明确写为“无”。

text

Correctness properties
- P1: ...
- P2: ...

Verified / assured
- P1: formal proof, tool/version, result
- P2: type-level construction boundary

Runtime-tested
- integer boundary cases
- differential compatibility
- target backend behavior

Assumptions
- ...
- ...

Not verified
- ...
- ...

Known model gaps
- ...
- ...

Evidence
- command
- artifact
- commit/SHA
- toolchain/version

不能仅以“tests green”或“proof green”结束。

15. Reproducibility

proof/toolingをCIやteamで使う場合は、通常のtest toolchainと同じく再現可能にする。

compiler/tool version
verifier / SMT solver / model checker version
solver strategy/configuration
timeout/resource limit
architecture差
package/lock/Nix/container等のenvironment definition

solver versionやstrategy差で結果が変わり得る場合は、current working environmentを固定する。

如果在 CI 或团队中使用 proof/tooling，应像常规 test toolchain 一样确保可复现性。

compiler/tool version
verifier / SMT solver / model checker version
solver strategy/configuration
timeout/resource limit
architecture 差异
package/lock/Nix/container 等 environment definition

如果 solver version 或 strategy 的差异可能改变结果，应固定 current working environment。

16. AI agent向けルール

16. 面向 AI agent 的规则

AIにcontract・invariant・proof annotationを書かせることはできるが、生成されたcontractを意図の代わりにしない。

AI agentは:

先にpropertyを自然言語とpredicateの両方で述べる
implementationから都合の良いpostconditionを逆算しない
counterexampleを最低1回探す
model/runtime差を確認する
proofを通すためだけにpreconditionを強めない
unsupported領域を隠さない
verified / Not verified / assumptionsを分離する
contract変更をbehavior変更と同じくreview対象にする

contractはAIにとってもmachine-readable specificationとして扱う。

可以让 AI 编写 contract、invariant 和 proof annotation，但不能将生成的 contract 当作真实意图的替代品。

AI agent 应当：

首先使用自然语言和 predicate 两种形式陈述 property
不从 implementation 中反向推导对实现有利的 postcondition
至少寻找一次 counterexample
检查 model/runtime 差异
不为了通过 proof 而任意强化 precondition
不隐藏 unsupported 区域
分离 verified / Not verified / assumptions
将 contract 变更与 behavior 变更同等对待并进行 review

对于 AI，contract 同样应被视为 machine-readable specification。

17. Anti-patterns

禁止:

「formal verification済み」だけでprogram全体の正しさを主張する
test件数の多さから全入力保証を推論する
proof greenをruntime overflow安全性へ自動拡張する
sentinel absenceをindex validityと同一視する
timeoutをfailure/counterexampleとみなす
type-safeだからcollection invariantも成立するとみなす
abstract type constructorを通ったからconstructor内部も正しいとみなす
proofを通すために必要なpropertyを弱める
preconditionを呼び出し側で成立させずに利用する
modelで扱えない部分を「証明済み範囲」に含める
generated proof obligation数をquality KPIにする
testをproofで置換する
proofを理由にreviewを省略する

禁止：

仅凭“formal verification 已通过”就主张整个 program 正确
根据测试数量多推断可以保证所有输入
自动将 proof green 扩展为 runtime overflow 安全性
将 sentinel absence 与 index validity 视为同一回事
将 timeout 视为 failure/counterexample
认为 type-safe 就能保证 collection invariant
认为通过了 abstract type constructor 就能保证 constructor 内部正确
为使 proof 通过而弱化必要的 property
未在调用方建立 precondition 就直接使用它
将 model 无法处理的部分纳入“已证明范围”
将生成的 proof obligation 数量作为 quality KPI
使用 proof 替换 test
以 proof 为理由省略 review

18. Completion gate

このSkillを適用したtaskは、少なくとも次を満たして終了する。

correctness-critical propertyが列挙されている
各propertyのassurance mechanismが決まっている
mechanism選択理由がpropertyの性質とriskに対応している
必要なpre/post/invariantが具体化されている
preconditionの成立元が追跡できる
verification modelとruntime modelの差を確認した
formal verificationを使う場合、unsupported領域を明示した
specificationへcounterexample challengeを行った
verified / runtime-tested / assumptions / Not verifiedを分離した
Known model gapsを明示している
evidenceがcurrent code revisionへ紐づいている

应用此 Skill 的 task 结束时，至少应满足以下要求。

已枚举 correctness-critical property
已为每项 property 确定 assurance mechanism
mechanism 的选择理由与 property 的性质和 risk 相匹配
所需的 pre/post/invariant 已具体化
可以追踪 precondition 的成立来源
已检查 verification model 与 runtime model 之间的差异
如果使用 formal verification，已明确 unsupported 区域
已对 specification 执行 counterexample challenge
已分离 verified / runtime-tested / assumptions / Not verified
已明确 Known model gaps
evidence 已与当前 code revision 建立关联

19. Source case

このSkillの初期設計では、MoonBitで実プロダクトの整数部分をSMT solverで検証した次の記事を重要なcase studyとして使用した。

Mates Engineering: アルゴリズムの実装に MoonBit の Formal Verification を活用する

case studyから一般化した主な点:

型・テスト・proof・reviewは競合ではなく責務が異なる
finite test suiteと全称propertyを区別する
verifiableな整数の骨格を、浮動小数点等のmodel外領域から分離できる
mathematical integer modelとmachine integerの差はproofのsoundness interpretationに直結する
specificationの不足はsolverでは救えない
proofはtestの置き換えではなく、testでは見落とし得るfailure classを検出する手段である。finite test suite が見落とすfailure classをproofは補完的に検出し、両者は相互補完の関係にある

MoonBit固有の制約を他toolへ一般化してはならない。実際のprojectでは採用するlanguage/verifier/modelのcurrent behaviorを個別に確認する。

在此 Skill 的初始设计中，重要的 case study 是一篇文章，其中使用 SMT solver 验证了真实产品的整数部分所使用的 MoonBit。

Mates Engineering: 将 MoonBit 的 Formal Verification 应用于算法实现

从 case study 中总结出的主要观点：

类型、测试、proof 和 review 并非彼此竞争，而是承担不同职责
应区分 finite test suite 与全称 property
可以将可验证的 integer 骨架与 floating-point 等 model 外区域分离
mathematical integer model 与 machine integer 之间的差异，直接关系到 proof 的 soundness 解读
solver 无法弥补 specification 的不足
proof 不会替代 test，而是检测 test 可能遗漏的 failure class。finite test suite 遗漏的 failure class 可由 proof 补全检测，两者具有相互补充的关系

不应将 MoonBit 特有的约束推广到其他 tool。在实际 project 中，应分别确认所采用的 language/verifier/model 的 current behavior。