/**
 * lean-agentic Verifier Implementation
 *
 * Originally wrapped `lean-agentic`'s `createDemo()` engine. The
 * published 0.3.2 tarball is missing its WASM artifact
 * (`wasm/leanr_wasm.js`), which crashes the import. We now delegate
 * to a local in-process stub (`StubLeanEngine`) that satisfies the
 * same call shape and logs a warning. See ./stub-engine.ts for
 * trade-offs and the upgrade path.
 */
import { SecurityPolicy, Action, VerificationResult, ProofCertificate, LeanAgenticConfig } from '../types';
import { Logger } from '../utils/logger';
export declare class LeanAgenticVerifier {
    private engine;
    private logger;
    private config;
    private proofCache;
    private hashConsCache;
    constructor(config: LeanAgenticConfig, logger: Logger);
    /**
     * Initialize the verification engine
     */
    initialize(): Promise<void>;
    /**
     * Verify action against security policy
     * Uses hash-consing for fast equality checks (150x faster)
     */
    verifyPolicy(action: Action, policy: SecurityPolicy): Promise<VerificationResult>;
    /**
     * Prove theorem using Lean4-style theorem proving
     * Returns formal proof certificate for audit trail
     */
    proveTheorem(theorem: string): Promise<ProofCertificate | null>;
    /**
     * Verify a proof certificate
     */
    verifyProofCertificate(certificate: ProofCertificate): Promise<boolean>;
    /**
     * Get cache statistics
     */
    getCacheStats(): {
        proofs: number;
        hashCons: number;
        hitRate: number;
    };
    /**
     * Clear caches
     */
    clearCaches(): void;
    /**
     * Shutdown verifier
     */
    shutdown(): Promise<void>;
    private loadSecurityAxioms;
    private hashConsCheck;
    private dependentTypeCheck;
    private evaluateRules;
    private checkConstraints;
    private generateProofCertificate;
    private constructSecurityTheorem;
    private evaluateCondition;
    private evaluateConstraint;
    private checkTemporalConstraint;
    private checkBehavioralConstraint;
    private checkResourceConstraint;
    private checkDependencyConstraint;
    private actionToTerm;
    private policyToTerm;
    private constraintToType;
    private hashActionPolicy;
    private hashTheorem;
    private hashProof;
    private generateProofId;
    private extractDependencies;
    private calculateCacheHitRate;
    private timeoutPromise;
}
//# sourceMappingURL=verifier.d.ts.map