cdeust 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 | distributed design uses wall-clock ordering; no written spec; correctness argued by example executions; partial failure ignored |
| dijkstra | code and correctness argument must be developed together; a construct defeats local reasoning; tests can't cover the failure mode |
| liskov | swapping an implementation breaks callers; interfaces with types but no behavioral contract; composition breaks what components pass alone |
| turing | problem drowning in detail — reduce to the simplest machine; check decidability/complexity class before investing; vague concept needs an operational test |
| godel | the system reasons about itself (self-hosting, self-validating, self-referential rules) — find the incompleteness before it finds you |
| alkhwarizmi | messy problem needs a canonical form and an exhaustive case classification before an algorithm exists |
| panini | a sprawling rule set needs a compact generative specification with explicit conflict-resolution ordering |
Invocation
- Pick the best-fit agent above. If two or more fit, run
tools/genius-invoker.sh route "<problem>"and take the top ranked match. - Load it:
tools/genius-invoker.sh invoke <agent> "<problem>", then readagents/genius/<agent>.mdin full. - Apply the agent's
<workflow>step by step and answer in its<output-format>. The deliverable is a spec, invariant, or contract the code refines — not a narrative that it "looks right". - 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 -- "<problem>". - 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.