Formal Correctness

Formal Correctness

Problem shape: correctness-critical code (concurrency, distribution, protocol, contract) whose failure modes tests cannot exercise. The move: specification before code, invariants before traces, contracts before implementations, decidability before optimization.

Relevant geniuses

| Agent | Use when | |---|---| | [lamport](../../agents/genius/lamport.md) | distributed design uses wall-clock ordering; no written spec; correctness argued by example executions; partial failure ignored | | [dijkstra](../../agents/genius/dijkstra.md) | code and correctness argument must be developed together; a construct defeats local reasoning; tests can't cover the failure mode | | [liskov](../../agents/genius/liskov.md) | swapping an implementation breaks callers; interfaces with types but no behavioral contract; composition breaks what components pass alone | | [turing](../../agents/genius/turing.md) | problem drowning in detail — reduce to the simplest machine; check decidability/complexity class before investing; vague concept needs an operational test | | [godel](../../agents/genius/godel.md) | the system reasons about itself (self-hosting, self-validating, self-referential rules) — find the incompleteness before it finds you | | [alkhwarizmi](../../agents/genius/alkhwarizmi.md) | messy problem needs a canonical form and an exhaustive case classification before an algorithm exists | | [panini](../../agents/genius/panini.md) | a sprawling rule set needs a compact generative specification with explicit conflict-resolution ordering |

Invocation

1. Pick the best-fit agent above. If two or more fit, run

tools/genius-invoker.sh route "" and take the top ranked match.

1. Load it: tools/genius-invoker.sh invoke "", then read

agents/genius/.md in full.

1. Apply the agent's `` step by step and answer in its

``. The deliverable is a spec, invariant, or contract the code refines — not a narrative that it "looks right".

1. Typical chain: turing bounds what is decidable → lamport writes the spec →

dijkstra derives the code → liskov contracts the interfaces. Run pairs via tools/genius-invoker.sh compose lamport dijkstra -- "".

1. If no shape above matches, use a standard team agent instead.

Refuse when

• The requester wants a proof-shaped blessing for unspecified behavior —

write the spec first or decline.

• Tests are offered as the sole correctness argument for concurrent,

numerical, or adversarial code.

Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

• Author: cdeust
• Source: cdeust/zetetic-team-subagents
• License: MIT
• Homepage: https://ai-architect.tools

Install and usage instructions live in the source repository linked above.