export type FormalSpecVerificationStatus = 'passed' | 'failed' | 'error' | 'skipped';
export interface FormalSpecStageResult {
    readonly status: FormalSpecVerificationStatus;
    readonly message?: string;
    readonly checks?: readonly number[];
}
export interface FormalSpecQuintResult extends FormalSpecStageResult {
    readonly parse?: FormalSpecStageResult;
    readonly typecheck?: FormalSpecStageResult;
    readonly run?: FormalSpecStageResult;
    readonly verify?: FormalSpecStageResult;
    readonly invariants?: readonly string[];
    readonly temporal?: readonly string[];
}
export interface FormalSpecAlloyResult extends FormalSpecStageResult {
    readonly commands?: readonly AlloyParsedCommand[];
}
export interface FormalSpecVerificationResult {
    readonly verdict: 'passed' | 'failed' | 'error';
    readonly verificationStarted: boolean;
    readonly message?: string;
    readonly javaMajorVersion?: number;
    readonly quint: FormalSpecQuintResult;
    readonly alloy: FormalSpecAlloyResult;
}
export interface FormalSpecVerificationOptions {
    readonly abortSignal?: AbortSignal;
    readonly modelCheckTimeoutSeconds: number;
}
export interface FormalSpecBlocks {
    readonly quint: readonly string[];
    readonly alloy: readonly string[];
}
export interface QuintVerificationTargets {
    readonly invariants: readonly QuintVerificationTarget[];
    readonly temporal: readonly QuintVerificationTarget[];
}
export interface QuintVerificationTarget {
    readonly moduleName: string;
    readonly name: string;
}
export interface AlloyParsedCommand {
    readonly number: number;
    readonly type: string;
    readonly label: string;
}
/** Extract only closed Quint and Alloy fences from one provider response. */
export declare function extractFormalSpecBlocks(response: string): FormalSpecBlocks;
/** Parse the Java version strings emitted by common JDK distributions. */
export declare function detectJavaMajorVersion(output: string): number | undefined;
/** Select every conventionally named Quint invariant and temporal property. */
export declare function selectQuintVerificationTargets(parseResult: unknown): QuintVerificationTargets;
/** Return all parsed Alloy checks, including repeated command numbers. */
export declare function selectAlloyCheckTargets(commands: readonly AlloyParsedCommand[]): readonly number[];
/**
 * Extract and deterministically verify one newly generated provider response.
 * The conversation layer supplies only the response and resolved verifier options.
 */
export declare function runFormalSpecVerification(response: string, cwd: string, options: FormalSpecVerificationOptions): Promise<FormalSpecVerificationResult>;
//# sourceMappingURL=formalSpecVerifier.d.ts.map