Back to Details

create-formal-verification-skill

Compare original and translation side by side

🇺🇸

Original

English
🇨🇳

Translation

Chinese

Create a formal verification skill

创建形式化验证 skill

A test checks the cases that someone thought to write. Formal verification checks every case in a stated scope: every order of steps in a model, every input up to a bound, or every input. This skill finds the part of the repo where that matters most, verifies one property of it, and leaves a project-local skill that lets the next agent check a change against that property. Write that skill for an agent who reads it cold, mid-change, and has never seen your work. The user must be able to trust the result and act on it without learning the verification language.
测试只能检查有人想到并编写的用例。形式化验证则检查既定范围内的每一种情况：模型中步骤的每一种顺序、界限以内的每个输入，或所有输入。该 skill 会找出 repo 中最需要这种验证的部分，验证其中一项 property，并留下一个项目本地 skill，让下一位 Agent 能够根据该 property 检查变更。编写该 skill 时，要设想下一位 Agent 在变更进行到一半、毫无前置上下文且从未见过你工作的条件下阅读它。用户必须能够信任结果并据此采取行动，而无需学习验证语言。

Choose the target from the code

从代码中选择目标

Answer from the codebase, and ask the user only what you cannot observe. If the user named an area or a bug, start there.
A good target is a promise the code makes, where a break harms users and tests rarely reach the case that breaks it. Choose the strongest such target in the repo, not the one that is easiest to verify.
根据代码库回答，只询问无法从代码库观察到的内容。如果用户指定了某个区域或 bug，就从那里开始。
理想目标是代码作出的一项保证：一旦破坏就会伤害用户，而测试很少触达破坏它的场景。选择 repo 中最强的此类目标，而不是最容易验证的目标。

Let the question choose the tool

让问题决定工具

Pick the tool that answers the question at the lowest cost: a model checker, a proof assistant, an SMT-backed verifier, or another tool. Whether events can happen in a bad order usually suits a model checker over a small model of the design, and TLA+ is the default for that in any language. Whether the code itself behaves for every input, as with memory safety, overflow, or a data-structure invariant, usually suits a verifier that runs on the code. If no verifier runs on this language, say so, and test the real code with generated inputs, not a hand model of the function. A property that must hold at every size, where a bound is not enough, can need a proof. Prefer a tool that the repo's developers can install and run, and tell the user why you chose it.
选择能以最低成本回答问题的工具：model checker、proof assistant、基于 SMT 的 verifier 或其他工具。若要判断事件是否可能以不良顺序发生，通常适合使用 model checker 检查设计的小型模型；对于任何语言，TLA+ 都是此类问题的默认选择。若要判断代码本身对每个输入的行为，例如内存安全、溢出或数据结构不变量，通常适合使用直接作用于代码的 verifier。如果这种语言没有可运行的 verifier，应明确说明，并用生成的输入测试真实代码，而不是手工建立函数模型。一项必须在所有规模下都成立、仅设置界限仍不足以覆盖的 property，可能需要 proof。优先选择 repo 的开发者能够安装并运行的工具，并告诉用户选择它的原因。

What makes it good

什么让 skill 足够好

  • True to the code. Every part of the model or proof points to code that a reviewer can open. What the verification treats as one indivisible step is one indivisible step in the code. Names come from this repo.
  • Able to fail. A check that you have never seen fail proves nothing. Show each property failing on a broken variant of the code it guards, such as a removed check or a reordered step.
  • Findings stay findings. When the current code breaks the property, report it with the counterexample in the code's terms. Do not weaken the property or the model until it passes, and do not change product code unless the user asks.
  • Honest about scope. Say what is verified, under which bounds and assumptions, and what is left out. A pass covers the model or the bound, not the whole system.
  • Readable without the tool. State the property and the harm in one plain sentence each. Tell a counterexample as a short sequence of steps in the code's words.
  • Cheap to rerun. One command, a reproducible tool version, and a run short enough that the next agent will use it on every relevant change.
  • Kept in step with the code. Record which files and functions each check covers, and the commit at which you last confirmed that the verification describes them. When the covered code changes after that commit, the next agent can see that the verification needs another look.
  • 忠于代码。 模型或 proof 的每个部分都应指向评审者能够打开的代码。验证将其视为不可分割一步的部分，在代码中也必须是不可分割的一步。名称取自这个 repo。
  • 能够失败。 一项从未见过失败的检查什么也证明不了。通过移除检查或重排步骤等方式，构造其所守护代码的错误变体，展示每个 property 都会失败。
  • 如实保留发现。 当当前代码违反 property 时，应使用代码中的术语报告问题并附上 counterexample。不要为了通过检查而弱化 property 或模型，除非用户要求，否则不要修改产品代码。
  • 诚实说明范围。 说明验证了什么、在哪些界限和假设下进行了验证，以及未涵盖什么。一次通过只覆盖模型或界限，并不代表整个系统都通过验证。
  • 不依赖工具也能读懂。 分别用一句直白的话说明 property 及其危害。用代码中的术语，以简短步骤序列讲出 counterexample。
  • 重新运行成本低。 只需一条命令，工具版本可复现，运行时间足够短，使下一位 Agent 能在每次相关变更时使用它。
  • 与代码保持同步。 记录每项检查覆盖哪些文件和函数，以及最后确认验证与这些代码一致时所对应的 commit。当覆盖代码在该 commit 之后发生变化时，下一位 Agent 能够看出需要重新检查验证。

Generate the verify skill

生成 verify skill

Write a project-local skill with frontmatter that names the area and says when to use it. Without frontmatter, the skill never registers. From the skill alone, the next agent must be able to tell whether a change touches the verified code, run the check, tell a real bug from a modeling error, and update the verification when a change is intended. Put the coverage record and the sync commit in the skill, and tell the next agent to move the sync commit forward only after it confirms that the verification describes the code at the new commit. Use this repo's real commands, paths, and nouns, and leave no placeholders.
编写一个项目本地 skill，其 frontmatter 标明目标区域和适用时机。没有 frontmatter，skill 就无法注册。仅凭该 skill，下一位 Agent 就必须能够判断变更是否触及已验证的代码、运行检查、区分真实 bug 与建模错误，并在变更属于预期修改时更新验证。将覆盖记录和同步 commit 写入 skill，并告诉下一位 Agent，只有在确认验证仍能描述新 commit 中的代码后，才能推进同步 commit。使用这个 repo 中真实的命令、路径和术语，不留下任何 placeholder。

Prove it before you hand off

移交前先证明其有效

Follow the generated skill once, as the next agent would, on a scratch change that breaks the property in the real code. It must catch the break. Then drop the scratch change and confirm that the check is back where it started: passing, or failing only on the findings you will report. A verify skill that was never run is a draft. If the skill misses the break or a step does not run, fix the skill or the verification, not the scratch change.
按照生成的 skill 所规定的流程，像下一位 Agent 那样，针对一处会破坏真实代码中 property 的临时变更完整执行一次。它必须发现该破坏。然后撤销临时变更，并确认检查恢复到起始状态：通过，或者仅在将要报告的发现上失败。从未运行过的 verify skill 只是一份草稿。如果 skill 漏掉了破坏，或某一步无法运行，应修复 skill 或验证，而不是临时变更。

Hand off

移交

Tell the user what you verified, which tool you used and why, the bounds, what the check found in plain words, how to run it, and what it does not cover. Suggest a second target only if you found a close one. Point the user at 
/maintain-formal-verification-skill
for bringing the verification back in line after changes that did not recheck it.
告诉用户验证了什么、使用了什么工具及其原因、验证的界限、检查以直白语言发现的问题、运行方法，以及未覆盖的范围。只有在发现紧密相关的第二个目标时，才建议用户继续验证该目标。引导用户使用 /maintain-formal-verification-skill，在发生未重新检查的变更后，让验证重新与代码保持一致。