Specification Business

The recognition that as formal-verification capabilities improve, the primary bottleneck shifts from proof generation to accurately specifying what needs to be proven. As carina-hong states: "Anything that can be specified can be proven. Humans are bad at specifying everything we want."

Core Challenge

The specification business represents a fundamental limitation in the verified-ai approach:

• Technical capability: AI systems become increasingly capable of generating formal proofs
• Human bottleneck: The challenge shifts to humans accurately defining the problem space
• Specification gap: Difference between what humans think they want proven and what they actually need

Implications for Axiom Math

This challenge has significant implications for axiom-math's business model and technical roadmap:

• Market opportunity may depend more on specification tools than proof generation
• Need for human-AI collaboration interfaces for problem definition
• Potential requirement for domain-specific specification languages or frameworks
• Business model may shift toward specification consulting rather than pure proof generation

Broader Context

The specification business connects to fundamental questions in AI alignment and requirements engineering:

• Requirements elicitation: Classical software engineering problem at larger scale
• AI alignment: Ensuring systems optimize for intended rather than specified objectives
• Domain expertise: Need for deep understanding of problem domains to specify correctly
• Iterative refinement: Specification as ongoing process rather than one-time definition

Strategic Response

Recognition of the specification business suggests several potential strategic directions:

• Development of specification assistance tools and methodologies
• Focus on domains where specification is clearer (mathematics, formal systems)
• Human-in-the-loop approaches for specification refinement
• Collaboration tools for specification development and validation

See also

• specification-problem
• verified-ai
• axiom-math
• formal-verification