formal methods skills

juxt/allium

Skill Claude CodeCodex

Give your AI agents something more useful than a prompt. Velocity through clarity.

juxt/allium

Skill Claude CodeCodex

Run a structured discovery session to build an Allium specification through conversation. Use when the user wants to create a new spec from scratch, elicit or gather requirements, capture domain behaviour, specify a feature or system, define what a system should do, or is describing functionality and needs help…

juxt/allium

Skill Claude CodeCodex

Generate tests from Allium specifications. Use when the user wants to propagate tests, generate test files from a spec, write tests for a specification, create property-based tests, produce state machine tests, check test coverage against spec obligations, or understand what tests a specification requires.

fizzbee-io/fizzbee

Skill Claude CodeCodex

Run the FizzBee model checker or simulator on a .fizz spec. Use when the user wants to verify a spec, run the model checker, simulate behavior, check a guided trace, or interpret model checker output.

fizzbee-io/fizzbee

Skill Claude CodeCodex

Create model-based tests (MBT) connecting a FizzBee spec to a real system under test (SUT). Use when the user has a .fizz spec and wants to generate and run tests against a TypeScript/Playwright UI, Go service, Rust library, or Java application. Also use when working with fizzbee-mbt adapter code in any of these…

fizzbee-io/fizzbee

Skill Claude CodeCodex

Write, edit, or review FizzBee (.fizz) specifications for model checking distributed systems. Use when the user asks to model a system, write a formal spec, define invariants or liveness properties, or when working with a .fizz file.

morluto/jacobian

Skill Claude CodeCodex

Audit new or existing Jacobian mathematical operations for public-domain mismatches, hidden work expansion, evidence-backed scale or backend improvements, lossy exact results, source-unbound conclusions, and producer-consumer incompatibility. Use for operation-contract reviews, mathematical performance investigations…

morluto/jacobian

Skill Claude CodeCodex

Decompose a bounded corpus of mathematical proofs, formalizations, scripts, and certificates into recurring solution techniques and the smallest reusable Jacobian postconditions. Use for repository- or corpus-level “what can Jacobian learn?” audits; do not use for one operation contract or one agent trajectory.

morluto/jacobian

Skill Claude CodeCodex

Review completed or paused mathematical agent transcripts, visible reasoning, code, searches, tool calls, corrections, and final claims to extract evidence-backed lessons for Jacobian operations, discovery, contracts, skills, evaluations, and documentation. Use for mathematical workflow retrospectives and "what should…

ymm-oss/fsl

Skill Claude CodeCodex

Operate FSL's GitLab Flow-inspired lifecycle from short-lived branches through main and production to an exact vX.Y.Z release tag. Use when adopting the branch flow, integrating post-merge quality improvements, promoting a release, cutting a release, or handling a production hotfix.

ymm-oss/fsl

Skill Claude CodeCodex

Reverse-engineer an FSL design-layer spec from existing source code. Scope the stateful subsystem, harvest state/actions/guards/effects with source-line witnesses, surface invariants and forbidden flows as confirmation questions (never fabricated), then verify, mutation-test for hollowness, and prove conformance by…

ymm-oss/fsl

Skill Claude CodeCodex

Shared FSL language and verifier reference for writing, checking, verifying, repairing, explaining, mutating, refining, replaying, generating scenarios/test scaffolds, and interpreting fslc JSON results. Use directly for FSL syntax, kernel specs, verifier errors, repair loops, and command usage. For role-specific…

younes-io/agent-skills

Skill Claude CodeCodex

Write and iteratively refine executable TLA+ specs (.tla) and TLC model configs (.cfg) from natural-language system designs; run TLC model checking; summarize pass/fail and counterexamples with explicit assumptions and bounds. Use when asked to design or validate a protocol/state machine, create or edit .tla/.cfg…

younes-io/agent-skills

Skill Claude CodeCodex

Write and iteratively refine TLA+ theorem proofs in .tla modules with TLAPS (tlapm); run proof checks and summarize proved vs failed/omitted obligations with explicit assumptions and trust boundaries. Use when asked to create or fix THEOREM or PROOF blocks, diagnose TLAPS failures, strengthen inductive invariants…

cognitive-fab/polygraph

Skill Claude CodeCodex

Write NEW stateful code that is verifiable from the moment it's written, instead of auditing code that already exists (that's the "polygraph" skill). Draft a contract from a feature description, author a SAM v2 strict-profile module against it (named intents/schemas/domains, keyed acceptors, reject(reason), sealed…

cognitive-fab/polygraph

Skill Claude CodeCodex

A polygraph for your state machine. Audit a stateful piece of code end-to-end: YOU (the agent) instrument a copy, build any test doubles needed to run it, and capture real execution traces, then derive a transition-function spec from its source with an LLM (default artifact: a SAM v2 strict-profile module — named…

cognitive-fab/polygraph

Skill Claude CodeCodex

Elicit the invariants for a state machine — the plugin takes the lead. Harvest candidate invariants from the contract's own vocabulary (terminal states, typed fields, reject rules, effect kinds), contribute the frontier model's domain knowledge as candidates, pre-check every candidate against the machine so each…

kotaroyamame/formal-agent-contracts

Skill Claude CodeCodex

A test-generation skill that turns VDM-SL specifications and protocol documents into Jest- or Vitest-compatible contract tests. VDM-SL is a formal language for describing software rules; contract tests check that code follows those rules.

kotaroyamame/formal-agent-contracts

Skill Claude CodeCodex

Refine a provisional VDM-SL specification through dialogue with the user, uncovering the true specification that exists in the user's mind. The provisional spec (from extract-spec) serves as a scaffold for questions. Triggered by: "refine the spec", "review the provisional spec"…

kotaroyamame/formal-agent-contracts

Skill Claude CodeCodex

A checker for VDM-SL, a formal language used to describe software designs precisely. It checks the file’s grammar and types, reviews related design documents, and creates proof obligations—conditions that still need to be proven.