skills.rest
Hakkadaikon
HakkadaikonCOMMUNITY
Explore all skills by this author →
𝕏@hakkadaikonGitHub

oracle-relational

Validates implementations using metamorphic relations and formally proven predicates as test oracles.

Updated Jun 24, 2026
Search Tags:#formal verification#lean 4#property-based testing#fast-check#tla+#metamorphic testing#test oracle
One-click install
npx skills add https://github.com/Hakkadaikon/hymme --skill oracle-relational-hakkadaikon
Or copy as Structured Prompt for Agent▼
Please help me install this Agent Skill.
Skill: oracle-relational
Source: https://github.com/Hakkadaikon/hymme/tree/main/skills/oracle-relational
Command: npx skills add https://github.com/Hakkadaikon/hymme --skill oracle-relational-hakkadaikon

SYSTEM DOCUMENTATION & REQUIREMENTS

What problem does it solve? When you cannot hand-write expected values for every test case—such as search ranking, numerical computation, ML inference, or optimization—this Skill shows how to delegate correctness judgment to input-output relations and to predicates already proven by upstream formal methods (TLA+/Lean 4). ## Core Features & Use Cases - Metamorphic Testing: Systematically derive metamorphic relations (invariant, equivariant, monotonic, idempotent/invertible) from the specification and turn each into a property-based test with fast-check, avoiding numeric comparison pitfalls like -0/+0 with toBe. - Formal Verification Bridging: Map Lean 4 theorems and TLA+ safety invariants one-to-one onto property-based tests against the actual implementation, detecting divergence between proven design and code. - Use Case: After proving decode (encode x) = x in Lean, write a fast-check property asserting the same predicate against the real codec implementation, and layer multiple metamorphic relations so mutations cannot survive. ## Quick Start Ask the AI to apply the oracle-relational techniques to derive metamorphic relations and bridge proven Lean/TLA+ predicates into property-based tests for your module.

Frequently Asked Questions about oracle-relational

High-intent search queries and answers about installing and using this skill.

FAQPage Schema
How do I test code when I cannot write expected values?▼

Use metamorphic testing: derive relations from the specification such as invariance under input permutation, equivariance, monotonicity, or idempotence, then assert each relation as a property-based test. This detects contradictions without needing any concrete expected output.

How to bridge Lean or TLA+ proofs into implementation tests?▼

Enumerate all proven Lean theorems and TLA+ safety invariants, map each predicate one-to-one onto implementation inputs and state, then express them as fast-check properties or model-based test invariants. Never count theorems containing sorry as proven.

What is metamorphic testing with fast-check?▼

Metamorphic testing verifies that transforming the input produces a predictable change (or no change) in the output, such as sorting being invariant under input permutation. With fast-check you generate wide inputs, run both original and transformed inputs through the system, and assert the expected output relation.

Why do numeric metamorphic tests fail with toBe in Vitest?▼

toBe uses Object.is, which treats -0 and +0 as different values, causing flaky failures when relations like distributivity produce -0 on one side and +0 on the other. Use === or a tolerance-based comparison for numeric relation checks instead.

When should I not use metamorphic or formal-verification oracles?▼

Skip metamorphic relations when you can directly assert absolute output values, and skip formal-verification bridging when no TLA+ or Lean verification exists for the logic. Adding these layers without upstream proofs violates YAGNI.

Related Skills

Explore More Software Engineering Skills→
CybLowCybLow
1

guru-refactor-methods

Refactor complex methods using Extract Method and Inline Method techniques.

Community
Intermediate
NealschNealsch

Forge-Automated-Test-Authoring

Translates test plans and acceptance criteria into hermetic automated unit, integration, and contract tests.

Community
Advanced
jacob-balslevjacob-balslev
1

property-based-testing

Run property-based tests that generate inputs and shrink failures to minimal counterexamples.

Community
Intermediate
scute-shscute-sh
3

approval-tests

Compare complex outputs against pre-approved golden master files across multiple languages.

Official
Intermediate