From odin
Implements Design-by-Contract with formal preconditions, postconditions, and invariants across any language. Helps enforce behavioral specifications at public API boundaries and complex state invariants. Best paired with static verification before runtime checks.
How this skill is triggered — by the user, by Claude, or both
Slash command
/odin:design-by-contractThe summary Claude sees in its skill listing — used to decide when to auto-load this skill
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.
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 for language-specific contract tools. See examples for brief contract patterns per language.
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 |
ensures(result == x - y) for subtract(x, y) adds nothing| Approach | Philosophy | When |
|---|---|---|
| Defensive | Don't trust caller; always check | Unknown callers, legacy APIs, untrusted input |
| DbC | Clear contract; caller handles pre, method handles post | Internal APIs, well-scoped teams, correctness-critical |
| Hybrid | Defensive at boundary; DbC internally | Best practice for modern systems |
Operation: withdraw(amount)
Preconditions:
PRE-1: amount > 0
PRE-2: amount <= balance
PRE-3: account.status == Active
Postconditions:
POST-1: balance == old(balance) - amount
POST-2: result == amount
Invariants:
INV-1: balance >= 0
| Code | Meaning |
|---|---|
| 0 | All contracts enforced and tested |
| 1 | Precondition violation in production code |
| 2 | Postcondition violation in production code |
| 3 | Invariant violation in production code |
| 11 | Contract library not installed |
| 13 | Runtime assertions disabled |
| 14 | Contract lint failed |
npx claudepluginhub outlinedriven/odin-claude-plugin --plugin odinRuns a contract-first development pipeline for verifiable correctness: define contracts, implement, audit, and pack proof artifacts.
Designs and manages API contracts before implementation using OpenAPI and AsyncAPI specs for contract-first development workflows and best practices.
Generates OpenAPI 3.0/3.1 specs and Pact consumer contracts from API code, designs, or schemas for documentation, testing, and code gen.