/**
 * Formal Verifier — Deterministic claim verification that can't hallucinate.
 *
 * This is a local copy of api/lib/formal-verifier.ts for use within the SDK.
 * The canonical version lives at api/lib/formal-verifier.ts.
 */
export interface ForwardClaim {
    id: string;
    category: 'correctness' | 'security' | 'performance' | 'error-handling' | 'edge-case' | 'type-safety';
    severity: 'critical' | 'high' | 'medium' | 'low';
    description: string;
    assertion: string;
    testable?: boolean;
}
export interface ForwardVerification {
    claimId: string;
    verdict: 'PASS' | 'PARTIAL' | 'FAIL' | 'N/A' | 'UNVERIFIABLE';
    reasoning: string;
    evidence?: string;
    verification_method?: 'formal' | 'llm';
    formal_override?: {
        original_llm_verdict: 'PASS' | 'PARTIAL' | 'FAIL' | 'N/A' | 'UNVERIFIABLE';
        formal_verdict: 'PASS' | 'FAIL';
        reason: string;
    };
}
export interface FormalVerificationStats {
    formally_verified: number;
    llm_verified: number;
    disagreements: number;
    formal_overrides: number;
    /** Disagreements where a weak (absence-of-evidence) formal FAIL was NOT allowed to override an LLM PASS. */
    weak_overrides_suppressed?: number;
    /** Disagreements where a weak (keyword-presence) formal PASS was NOT allowed to flip an LLM FAIL/PARTIAL/UNVERIFIABLE to PASS. */
    weak_pass_overrides_suppressed?: number;
    /** Compound claims split into sub-lemmas that yielded a sound formal verdict. */
    decomposed_claims?: number;
    /** Total sub-lemmas discharged by the formal verifier across all decompositions. */
    lemmas_formally_discharged?: number;
    /** Sentinel rule ports executed against security claims (Phase C bridge). */
    sentinel_checks_run?: number;
    /** Defect instances positively found by Sentinel ports (each is a sound FAIL). */
    sentinel_defects_found?: number;
}
export type FormalCheckType = 'function_exists' | 'parameter_check' | 'error_handling' | 'null_check' | 'type_annotation' | 'sql_parameterized' | 'input_validation' | 'arithmetic_correctness' | 'api_misuse' | 'undefined_reference' | 'feature_presence' | 'data_handling' | 'configuration_check' | 'capacity_limit' | 'security_control' | 'compliance_check' | 'connectivity_check' | 'pricing_billing' | 'role_access' | 'media_processing' | 'subjective_quality' | 'requirement_constraint' | 'debug_artifact' | 'equality_check' | 'resource_leak' | 'contract_verification' | 'sentinel_rule';
export interface FormalCheckResult {
    claimId: string;
    checkType: FormalCheckType;
    verdict: 'PASS' | 'FAIL';
    evidence: string;
    confidence: 1;
    /**
     * True only when the verdict carries DECISIVE evidence, in either direction.
     *
     * FAIL: a defect POSITIVELY found (string-concat SQL, nonexistent API,
     * contradicted arithmetic, wrong parameter count, claim-named identifier
     * missing). Absence-of-evidence FAILs ("no security control patterns found")
     * leave this unset and may never override an LLM PASS: on a per-route code
     * slice, "my regexes didn't see it" is not a contradiction.
     *
     * PASS: the property POSITIVELY computed/counted (arithmetic expression
     * evaluated to the claimed value, parameter count matched the claimed count).
     * Keyword-presence PASSes ("Security controls found: authorization") and
     * absence-of-defect PASSes ("no known bad APIs detected") leave this unset
     * and may never flip an LLM FAIL/PARTIAL/UNVERIFIABLE to PASS: keyword
     * presence does not verify the claim, it launders uncertain verdicts.
     *
     * Soundness is per-RESULT, not per-checkType, because some checks
     * (sql_parameterized, arithmetic_correctness) have both decisive and weak
     * branches. Origin: islandlink dogfood 2026-07-20 — 3 of 10 reported bugs
     * were absence-FAIL overrides of correct LLM PASSes; runs B/C also carried
     * 5 and 3 weak-PASS overrides (keyword presence flipping PARTIAL/UNVERIFIABLE
     * to PASS). Capsules: formal-override-precision-fix, assay-weak-pass-overrides.
     */
    sound?: boolean;
}
interface ClassifiedClaim {
    claim: ForwardClaim;
    formallyVerifiable: boolean;
    checkType?: FormalCheckType;
    extractedTarget?: string;
}
export declare function classifyClaim(claim: ForwardClaim): ClassifiedClaim;
/** A claim split into independently-checkable atomic assertions. */
export interface ClaimDecomposition {
    parentId: string;
    subClaims: ForwardClaim[];
    method: 'rule' | 'llm';
}
/** Recomposed result for a decomposed claim. */
export interface LemmaResult {
    parentId: string;
    subResults: Array<{
        subClaim: ForwardClaim;
        classified: ClassifiedClaim;
        formal?: FormalCheckResult;
    }>;
    composedVerdict: 'PASS' | 'PARTIAL' | 'FAIL';
    /** Fraction of sub-lemmas discharged by the formal verifier (0..1). */
    formalFraction: number;
}
/**
 * Split a compound claim into atomic sub-lemmas (rule-based, zero-cost, pure).
 * Splits the assertion; if that yields <2 fragments, falls back to the description.
 * Sub-claim ids are deterministic: `${parentId}.L1`, `${parentId}.L2`, ... (resumable).
 */
export declare function decomposeClaimRuleBased(claim: ForwardClaim): ClaimDecomposition;
/**
 * Classify + formally check each sub-lemma, then compose.
 * Reuses runSingleCheck — the same dispatch the whole-claim path uses.
 */
export declare function verifyDecomposition(decomp: ClaimDecomposition, code: string, language: string): LemmaResult;
export declare function runFormalVerification(code: string, language: string, claims: ForwardClaim[], llmVerifications: ForwardVerification[], options?: {
    lemmaDecomposition?: boolean;
    sentinelRules?: boolean;
}): {
    verifications: ForwardVerification[];
    stats: FormalVerificationStats;
};
export interface ClaimlessFinding {
    checkType: FormalCheckType;
    line: number;
    evidence: string;
    severity: 'critical' | 'high' | 'medium';
}
/**
 * Scan code line-by-line for issues without requiring a claim object.
 * Suitable for development-time hooks (pre-commit, editor integration).
 */
export declare function runClaimlessChecks(code: string, language: string): ClaimlessFinding[];
export {};