design-by-contractlisted
Install: claude install-skill OutlineDriven/odin-claude-plugin
# Design-by-Contract development
Contracts (PRE/POST/INV) define behavioral specification -- design from requirements before code exists. Formalized as Hoare Triples: `{P} C {Q}` where P=precondition, C=code, Q=postcondition.
**Modern insight (2025)**: DbC complements LLM-generated code by serving as safety guardrails -- contracts clarify intent and prevent AI from breaking integrations. Spec-driven development (2025) positions contracts as "executable specifications."
See [libraries](references/libraries.md) for language-specific contract tools.
See [examples](references/examples.md) for brief contract patterns per language.
---
## Verification Hierarchy
Use compile-time verification before runtime contracts. If a property can be verified statically, do NOT add a runtime contract.
```
Static Assertions (compile-time) > Test/Debug Contracts > Runtime Contracts
```
| Property | Static | Test | Debug | Runtime |
|----------|--------|------|-------|---------|
| Type size/alignment | `static_assert` | - | - | - |
| Null/type safety | Type checker | - | - | - |
| Exhaustiveness | Pattern match | - | - | - |
| Expensive O(n)+ | - | test_ensures | - | - |
| Internal invariants | - | - | debug_invariant | - |
| Public API input | - | - | - | requires |
| External/untrusted | - | - | - | Always required |
---
## When to Apply
- Public API boundaries -- callers need clear contracts
- Complex state invariants -- balance >= 0, capacity limits
- Financial/business rule enforcem