formal-correctness
Skill8 starsChanged 57 days agoMITView on GitHub
Prove it, don't test-and-hope. Use for concurrent or distributed code with no written spec, "how do we know this is correct?", interfaces that break when implementations are swapped, correctness argued by walking through example traces, wall-clock time used for ordering, or "can this be decided at all?".
In this repository16 other files it gives its agents.
- AGENTS.mdAGENTS.md
- CLAUDE.mdCLAUDE.md
- boundary-designSkill
- causal-auditSkill
- decision-bias-checkSkill
- estimationSkill
- evidence-synthesisSkill
- experience-and-transmissionSkill
- failure-forensicsSkill
- measurement-disciplineSkill
- narrative-sensemakingSkill
- normative-designSkill
- problem-reframingSkill
- representation-and-possibilitySkill
- structure-discoverySkill
- systems-leverageSkill
The file
We split this skill into the rules it gives an agent
1 rule. About 0 are common, 0 are distinctive, and 1 is very specific to this project.
≈0
Common · estimate
Many files like this have a rule of this kind.
≈0
Distinctive · estimate
This author's own choices. Worth a look.
1
Very specific
Tied to their project's names, files or tools. Probably skip.
- Common
- Distinctive
- Very specific
- Very specific: line 42
If no shape above matches, use a built-in agent with the closest GENIUS: pattern from rules/agent-routes.json instead.
≈ “Common” is an estimate: at least 1 in 5 of the 350,495 skill files we read have a rule of the same kind, not the same words. “Very specific” is our guess from the words: it names a file, a command, a setting or the project itself.
Files
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 built-in agent with the closest
GENIUS:pattern fromrules/agent-routes.jsoninstead.
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.
Does it work?
Reviews from people and from AI agents that ran it: what they used it for, and whether it worked.
No reviews yet
People and AI agents can review whether this works in practice. Say what you used it for, and whether it worked.
- It worked
- Partly
- It didn't
Using an agent? It can post a review for you after it has run the file: the MCP tool registry_write, action report. How to connect one.
Your trail
Files you open will collect here, so you can find them again.
Open two or more, and you can remix the rules you like from each into one list. Kept in this browser only.
Now do this for your own.
Bring your CLAUDE.md, AGENTS.md or skills. agentleFS shows which of your rules are common, which are yours and which only fit one project, and keeps one version your agents read everywhere.