用途：契约式设计（DbC）以 PRE（前置条件）、POST（后置条件）、INV（不变式）定义行为规格，在代码存在之前从需求出发进行设计，形式化为 Hoare 三元组 {P} C {Q}。资料指出，DbC 可作为 LLM 生成代码的安全护栏，澄清意图并防止 AI 破坏集成，属于“可执行规格”。
主要能力：提供验证层级——静态断言（编译期）优先于测试/调试契约，再优先于运行时契约；能静态验证的属性不应添加运行时契约。适用场景包括公共 API 边界、复杂状态不变式（如 balance >= 0）、金融/业务规则、不可信外部数据、多组件集成点以及 AI 生成代码。不适用场景包括行为显然的内部辅助函数、简单 getter/setter、性能关键热路径、原型开发，以及类型系统已强制保证的属性。
使用方式：按语言中立工作流执行——PLAN 从需求提取 PRE/POST/INV 并编号；CREATE 按验证层级在合适级别实施契约，运行时契约仅保留给公共 API 边界与不可信输入；VERIFY 运行静态分析与构建，契约须能编译和 lint；TEST 为每个 PRE/POST/INV 编写违规测试。契约继承规则：子类型中前置条件可放宽（逆变），后置条件可加强（协变），不变式只能加强，从而自动满足里氏替换原则。
限制与注意：反模式包括契约重复类型系统、对编译期属性做运行时检查、无违规测试的契约、契约疲劳、后置条件复述实现、忽略 old() 语义、忽略契约继承。退出码含义：0 全部契约已实施并测试；1 生产代码前置条件违规；2 后置条件违规；3 不变式违规；11 契约库未安装；13 运行时断言被禁用；14 契约 lint 失败。资料未提供具体语言库名称、安装命令与代码示例细节。