该技能介绍契约式设计（DbC）开发方法：契约由前置条件（PRE）、后置条件（POST）和不变式（INV）组成，用于在代码存在前从需求定义行为规格，可形式化为 Hoare 三元组 {P} C {Q}。资料认为契约可作为 LLM 生成代码的安全护栏，属于可执行规格。
验证层级：能静态验证的属性不要加运行时契约，顺序为静态断言（编译期）高于测试/调试契约，高于运行时契约。类型大小与对齐用 static_assert；空值与类型安全交给类型检查器；穷尽性交给模式匹配；高开销 O(n)+ 用 test_ensures；内部不变式用 debug_invariant；公共 API 输入用 requires；外部/不可信数据始终需要校验。
适用场景：公共 API 边界、复杂状态不变式（如 balance>=0）、金融与业务规则合规、不可信外部数据、多组件集成点、AI 生成代码。不适用：行为显然的内部辅助函数、简单 getter/setter、性能敏感热路径、原型阶段、类型系统已保证的属性。
反模式包括：契约与类型系统重复、为编译期属性加运行时检查、契约没有违反测试、契约泛滥、后置条件复述实现、忘记 old() 语义、忽略契约继承。继承规则：子类型中前置条件可放宽、后置条件可加强、不变式可加强，对应 Liskov 替换原则。
与防御式编程对比：防御式用于未知调用方、遗留 API、不可信输入；DbC 用于内部 API 与正确性关键场景；现代最佳实践是边界防御、内部 DbC。
工作流：PLAN 从需求提取 PRE/POST/INV 并编号；CREATE 按层级选择验证级别并实现；VERIFY 运行静态分析与构建；TEST 为每个契约写违反测试。宪法规则要求所有契约均实现、运行时契约启用、违反可被捕获、每个契约可追溯到需求。退出码：0 全部通过，1 前置条件违例，2 后置条件违例，3 不变式违例，11 未安装契约库，13 运行时断言被禁用，14 契约 lint 失败。语言特定工具与示例见资料中 libraries 与 examples 部分，具体内容暂未提供。