Formalize Request Skill

Iteratively convert natural language user requests into verifiable formal specifications.

Purpose

Avoid next-word prediction in safety-critical domains (like SPARTA) by ensuring every user request is unambiguous and formally grounded BEFORE retrieval/generation.

Core Principle

KEEP ASKING until the request is ENTITY-ANCHORED and VERIFIABLE

The skill loops through /interview until the user's intent is precise enough to express as:

• Entity Spec (for retrieval queries - 99% of SPARTA)
• Lean4 Goal (for mathematical/logical proofs only)

Key Insight: Entity Specs ARE Formal Specifications