Loading...
Loading...
Apply Model-First Reasoning (MFR) to code generation tasks. Use when the user requests "model-first", "MFR", "formal modeling before coding", "model then implement", or when tasks involve complex logic, state machines, constraint systems, or any implementation requiring formal correctness guarantees. Enforces strict separation between modeling and implementation phases.
npx skill4agent add petekp/agent-skills model-first-reasoningBased on Kumar & Rana (2025), "Model-First Reasoning LLM Agents: Reducing Hallucinations through Explicit Problem Modeling" (arXiv:2512.14474)
MODEL INCOMPLETESTUB| Check | Description |
|---|---|
| Coverage | Every user requirement is represented in exactly one of: a constraint, the goal/acceptance criteria, or an action precondition/effect |
| Operability | Every operation your plan would require is present as an action |
| Consistency | Constraints don't contradict each other; action effects don't violate invariants |
| Testability | Every constraint has ≥1 test oracle |
MODEL PATCHmodel.jsonpython scripts/validate-model.py model.json012{
"deliverable": {
"description": "What we're building",
"files_expected": ["path/to/file.ts", ...]
},
"entities": [
{"name": "EntityName", "description": "...", "properties": [...]}
],
"state_variables": [
{"name": "varName", "type": "...", "initial": "...", "description": "..."}
],
"actions": [
{
"name": "actionName",
"description": "...",
"preconditions": ["..."],
"effects": ["..."],
"parameters": [...]
}
],
"constraints": [
{"id": "C1", "statement": "...", "type": "invariant|precondition|postcondition"}
],
"initial_state": ["description of starting conditions"],
"goal": ["acceptance criteria"],
"assumptions": ["things we assume to be true"],
"unknowns": ["questions that must be answered before proceeding"],
"requirement_trace": [
{
"requirement": "<verbatim from user>",
"represented_as": "goal|constraint|action",
"ref": "C1|action_name|goal_item"
}
],
"test_oracles": [
{"id": "T1", "maps_to": ["C1"], "description": "how to verify constraint"}
]
}unknowns{
"audit_pass": true|false,
"issues": [
{"type": "coverage|operability|consistency|testability", "detail": "..."}
]
}audit_passStep 1: [action_name]
- Preconditions check: [list which preconditions are satisfied]
- Effects applied: [what state changes]
- Constraints check: [C1, C2, ...]deliverable.files_expected| Model Element | Code Translation |
|---|---|
| entities / state_variables | Types, interfaces, data models |
| actions | Functions/modules with validation + explicit failure modes |
| constraints | Runtime checks, defensive parsing, invariants |
test_oraclesUser: Build a shopping cart that enforces: max 10 items, no duplicate SKUs,
total can't exceed $1000
You: [PHASE 1: MODEL]
{
"entities": [
{"name": "CartItem", "properties": ["sku", "price", "quantity"]}
],
"constraints": [
{"id": "C1", "statement": "cart.items.length <= 10", "type": "invariant"},
{"id": "C2", "statement": "all SKUs in cart are unique", "type": "invariant"},
{"id": "C3", "statement": "sum(items.price * items.quantity) <= 1000", "type": "invariant"}
],
"actions": [
{
"name": "addItem",
"preconditions": ["cart.items.length < 10", "sku not in cart", "new total <= 1000"],
"effects": ["item added to cart"]
}
],
...
}
[PHASE 1.5: MODEL AUDIT]
{
"audit_pass": true,
"issues": []
}
[PHASE 2: IMPLEMENTATION]
// Now implementing strictly from the model...