kani-proof

Compare original and translation side by side

🇺🇸

Original

English

🇨🇳

Translation

Chinese

Kani Formal Verification

Kani形式化验证

Kani is a bounded model checker — it explores ALL possible values of symbolic inputs within bounds, making proofs exhaustive (not sampled like fuzzing).

Kani是一款有界模型检查器——它会在限定范围内探索符号输入的所有可能值，从而实现穷尽式证明（不同于模糊测试的抽样方式）。

Critical Rules

关键规则

These rules prevent the most common proof failures. Violating any one will likely cause the proof to fail.

No
#[kani::unwind]
or
#[kani::solver]
on first attempt. Omit both decorators entirely. Only add
```
#[kani::unwind(N)]
```
after getting an "unwinding assertion" error, and only add
```
#[kani::solver(cadical)]
```
after a timeout. Kani's defaults work better than guessing.
Assert the target property inline, not via helper methods. Do not call methods that check multiple invariants or iterate over collections — they introduce loops, extra assertions, and unrelated failure points. Read the struct fields directly and write the comparison yourself:
rust
```
// WRONG — helper checks more than the target property, adds loops
assert!(engine.check_all_invariants());

// RIGHT — asserts exactly what you're proving, no extra logic
assert!(engine.x.get() >= engine.y.get() + engine.z.get());
```
Use
kani::any()
without
kani::assume()
bounds first. Only add assume constraints after a timeout or OOM. Unconstrained symbolic values are often easier for the solver than bounded ranges.
Build state through public API only. Use constructors,
```
add_user()
```
,
```
deposit()
```
, etc. Never assign struct fields directly — it creates unreachable states that cause spurious failures. The only exception is
```
vault
```
or similar top-level fields with no setter API.
Stack allocation, not Box. Use
```
let mut engine = Engine::new(params)
```
not
```
Box::new(Engine::new(params))
```
. Box adds heap tracking overhead to the solver.
Small config parameters. If the constructor takes a size/capacity parameter that controls a loop (e.g.
```
max_accounts
```
), pass a small value (4–8) that matches
```
#[cfg(kani)]
```
constants found by the analyzer agent.

这些规则可避免最常见的证明失败。违反任何一条都可能导致证明失败。

首次尝试时不要使用
#[kani::unwind]
或
#[kani::solver]
。完全省略这两个装饰器。仅当出现“unwinding assertion”错误后再添加
```
#[kani::unwind(N)]
```
，仅当出现超时后再添加
```
#[kani::solver(cadical)]
```
。Kani的默认设置比自行猜测效果更好。

直接在代码中断言目标属性，不要通过辅助方法。不要调用检查多个不变量或遍历集合的方法——它们会引入循环、额外断言和无关的失败点。直接读取结构体字段并自行编写比较逻辑：

rust

// 错误示例——辅助方法检查的内容超出目标属性，还会引入循环
assert!(engine.check_all_invariants());

// 正确示例——仅断言你要证明的内容，无额外逻辑
assert!(engine.x.get() >= engine.y.get() + engine.z.get());

先使用无
kani::assume()
限制的
kani::any()
。仅当出现超时或内存不足（OOM）时再添加假设约束。无约束的符号值通常比有界范围更易被求解器处理。
仅通过公开API构建状态。使用构造函数、
```
add_user()
```
、
```
deposit()
```
等方法。永远不要直接赋值结构体字段——这会创建无法到达的状态，导致虚假失败。唯一例外是
```
vault
```
或类似无setter API的顶级字段。
使用栈分配，而非Box。使用
```
let mut engine = Engine::new(params)
```
而非
```
Box::new(Engine::new(params))
```
。Box会给求解器增加堆跟踪开销。
使用小配置参数。如果构造函数接受控制循环的大小/容量参数（如
```
max_accounts
```
），传入一个小值（4–8），该值需与分析Agent找到的
```
#[cfg(kani)]
```
常量匹配。

Workflow

工作流程

Step 1 — Analyze the Codebase

步骤1 — 分析代码库

Before writing any proof, spawn an Explore agent following references/agents/kani-analyzer-agent.md. It will return loop bounds, existing infrastructure, and state construction patterns. Do not skip this.

在编写任何证明之前，启动一个遵循references/agents/kani-analyzer-agent.md的Explore Agent。它会返回循环边界、现有基础设施和状态构建模式。不要跳过此步骤。

Step 2 — Write the Proof

步骤2 — 编写证明

Use the agent's output to write a harness. Select a pattern from the pattern table and see references/proof-patterns.md for templates.

利用Agent的输出来编写测试套。从证明模式表中选择一种模式，并查看references/proof-patterns.md获取模板。

Step 3 — Verify and Iterate

步骤3 — 验证与迭代

Run

cargo kani --harness proof_name

and diagnose failures using the diagnosis table. See references/kani-features.md for the full Kani API (contracts, stubbing, concrete playback, partitioned verification).

运行

cargo kani --harness proof_name

，并使用故障诊断表排查失败原因。完整的Kani API（契约、存根、具体回放、分区验证）请参考references/kani-features.md。

Kani-Specific Concepts

Kani专属概念

Non-Vacuity

非空性

A proof can report SUCCESS while proving nothing. This happens when no execution path reaches assertions — because the operation always fails for your inputs, assumptions are contradictory, results are discarded, or state is empty/trivial.

Detect with

kani::cover!(condition, "message")

— if Kani reports UNSATISFIABLE, that path is never taken.

Prevent by handling results explicitly:

rust

// VACUOUS — if operation always fails, nothing is checked
if result.is_ok() { assert!(invariant); }

// NON-VACUOUS — proof fails if operation can't succeed
match result {
    Ok(_) => { /* assert properties */ },
    Err(_) => { kani::assert(false, "must succeed"); unreachable!() }
};

Contradictory assumptions: If every path hits

assume(false)

or all

kani::cover!()

checks are UNSATISFIABLE, your

kani::assume()

constraints are contradictory — no valid inputs exist. Remove constraints and start unconstrained.

证明可能显示“成功”但实际未证明任何内容。当没有执行路径到达断言时会出现这种情况——可能是因为操作始终对输入失败、假设矛盾、结果被丢弃，或者状态为空/无意义。

检测方法：使用

kani::cover!(condition, "message")

——如果Kani返回UNSATISFIABLE，则该路径从未被执行。

预防方法：显式处理结果：

rust

// 空证明——如果操作始终失败，则不会检查任何内容
if result.is_ok() { assert!(invariant); }

// 非空证明——如果操作无法成功，证明会失败
match result {
    Ok(_) => { /* 断言属性 */ },
    Err(_) => { kani::assert(false, "must succeed"); unreachable!() }
};

矛盾假设：如果所有路径都触发

assume(false)

，或者所有

kani::cover!()

检查都返回UNSATISFIABLE，说明你的

kani::assume()

约束存在矛盾——不存在有效的输入。移除约束并从无约束状态重新开始。

Loop Unwinding

循环展开

Only relevant if you get an "unwinding assertion" error. Add

#[kani::unwind(N)]

where N = max_iterations + 1. Trace ALL loops in the call graph (target + callees + constructors). Check for

#[cfg(kani)]

constants that reduce collection sizes.

Parameter-driven loops: If a constructor loops over a config param (e.g.

for i in 0..capacity

), that param must be small (4–8). Use

#[cfg(kani)]

constants when they exist.

仅当出现“unwinding assertion”错误时才需要关注此问题。添加

#[kani::unwind(N)]

，其中N = 最大迭代次数 + 1。追踪调用图中的所有循环（目标函数、被调用函数、构造函数）。检查是否存在可减小集合大小的

#[cfg(kani)]

常量。

参数驱动的循环：如果构造函数遍历一个配置参数（如

for i in 0..capacity

），该参数必须是较小的值（4–8）。如果存在

#[cfg(kani)]

常量，请使用该值。

Diagnosing Failures

故障诊断

Kani Output	Fix
`unwinding assertion`	Add `#[kani::unwind(N)]` with N = loop_count + 1
Timeout / solver hang	Add `kani::assume()` to narrow ranges, try `#[kani::solver(cadical)]`
`VERIFICATION:- FAILED`	Use `cargo kani -Z concrete-playback --concrete-playback=print --harness name`
OOM / out of memory	Reduce state size, remove Box, fewer symbolic variables
`assume(false)` on all paths	Remove `kani::assume()` constraints — they're contradictory
`VERIFICATION:- SUCCESSFUL`	Check `kani::cover!()` statements are SATISFIED (non-vacuity)

Iterative approach: Start SIMPLE (no decorators, unconstrained inputs, API-built state) → add constraints only on timeout/OOM → add unwind only on unwinding errors → switch solver only on timeout.

Kani输出	修复方案
`unwinding assertion`	添加 `#[kani::unwind(N)]` ，其中N = 循环次数 + 1
超时/求解器挂起	添加 `kani::assume()` 缩小范围，尝试使用 `#[kani::solver(cadical)]`
`VERIFICATION:- FAILED`	使用 `cargo kani -Z concrete-playback --concrete-playback=print --harness name`
内存不足（OOM）	减小状态大小，移除Box，减少符号变量
所有路径均触发 `assume(false)`	移除 `kani::assume()` 约束——它们存在矛盾
`VERIFICATION:- SUCCESSFUL`	检查 `kani::cover!()` 语句是否为SATISFIED（非空性）

迭代方法：从简单开始（无装饰器、无约束输入、API构建的状态）→ 仅在超时/内存不足时添加约束 → 仅在出现展开错误时添加unwind → 仅在超时切换求解器。

Proof Patterns

证明模式

See references/proof-patterns.md for templates.

Pattern	When to Use	What It Proves
Conservation	Moves, creates, or destroys quantities	Accounting equation preserved
Frame / Isolation	Targets one entity in multi-entity system	Bystander entities unchanged
INV Preservation	Any state mutation	Canonical invariant holds before and after
Error Path	Input validation / preconditions	Specific error + state completely unchanged
Monotonicity	Counters, timestamps, accumulators	Value only moves in one direction
Idempotency	Settlement, sync, recompute	Applying twice = applying once
Arithmetic Safety	Numeric computation	No overflow/underflow/div-by-zero
Access Control	Privileged operations	Unauthorized callers rejected
State Machine	Lifecycle transitions	Only valid transitions occur
Inductive Delta	Core accounting (strongest form)	Equation holds with raw primitives
Lifecycle / Sequence	Multi-step user flows	Properties hold through chained operations

模板请参考references/proof-patterns.md。

模式	使用场景	证明内容
守恒性	移动、创建或销毁数量	会计等式保持不变
框架/隔离性	多实体系统中的单个目标实体	无关实体未被修改
不变量保持	任何状态变更	标准不变量在变更前后均成立
错误路径	输入验证/前置条件	特定错误 + 状态完全未变更
单调性	计数器、时间戳、累加器	值仅向一个方向变化
幂等性	结算、同步、重新计算	执行两次等同于执行一次
算术安全性	数值计算	无溢出/下溢/除零错误
访问控制	特权操作	拒绝未授权调用者
状态机	生命周期转换	仅发生有效转换
归纳增量	核心会计（最强形式）	等式基于原始原语成立
生命周期/序列	多步骤用户流程	属性在链式操作中始终成立

Harness Skeleton

测试套骨架

rust

#[cfg(kani)]
mod kani_proofs {
    use super::*;

    #[kani::proof]
    // NO #[kani::unwind] — only add after getting unwinding assertion error
    // NO #[kani::solver] — only add after getting timeout
    fn proof_name() {
        // 1. Build state through public API (NOT field mutation)
        // 2. Symbolic inputs: kani::any() with NO kani::assume() bounds
        // 3. Call function, handle result explicitly (no if result.is_ok())
        // 4. Assert ONLY the target property using raw field access
        //    (NOT check_conservation or other aggregate methods)
        // 5. kani::cover!() for non-vacuity
    }
}

rust

#[cfg(kani)]
mod kani_proofs {
    use super::*;

    #[kani::proof]
    // 不要使用#[kani::unwind] — 仅在出现unwinding assertion错误后添加
    // 不要使用#[kani::solver] — 仅在出现超时后添加
    fn proof_name() {
        // 1. 通过公开API构建状态（不要直接修改字段）
        // 2. 符号输入：使用无kani::assume()限制的kani::any()
        // 3. 调用函数，显式处理结果（不要用if result.is_ok()）
        // 4. 仅通过直接访问字段来断言目标属性
        //    （不要使用check_conservation或其他聚合方法）
        // 5. 使用kani::cover!()确保非空性
    }
}

Codebase Preparation

代码库准备

The Explore agent identifies what's needed. Common preparations:

#[cfg(kani)] const MAX_ITEMS: usize = 4;

— reduce collection sizes

[workspace.metadata.kani] flags = { tests = true }

in Cargo.toml

```
#[cfg(kani)] extern crate kani;
```
at crate root

Explore Agent会识别所需的准备工作。常见准备项：

#[cfg(kani)] const MAX_ITEMS: usize = 4;

— 减小集合大小

在Cargo.toml中添加

[workspace.metadata.kani] flags = { tests = true }

在 crate 根目录添加
```
#[cfg(kani)] extern crate kani;
```

Reference Files

参考文件

references/proof-patterns.md — Pattern catalog with templates and examples
references/kani-features.md — Kani API: contracts, stubbing, concrete playback, partitioned verification
references/invariant-design.md — Layered invariant design methodology
references/agents/kani-analyzer-agent.md — Explore agent for pre-proof codebase analysis

references/proof-patterns.md — 包含模板和示例的模式目录
references/kani-features.md — Kani API：契约、存根、具体回放、分区验证
references/invariant-design.md — 分层不变量设计方法
references/agents/kani-analyzer-agent.md — 用于证明前代码库分析的Explore Agent",