import type { ResolvedMachineDef } from "../core/dsl.js";
import type { StateGraph } from "../core/interpreter.js";
import type { ParsedTlcGraph } from "./parseDot.js";
export interface GraphComparisonResult {
    graphHash: string;
    tsStateCount: number;
    tlcStateCount: number;
    tsEdgeCount: number;
    tlcEdgeCount: number;
    equivalent: boolean;
}
export interface VerificationCertificate {
    certificateVersion: 2;
    machine: string;
    tier: string;
    machineSha256: string;
    checkedAt: string;
    proofPassed: boolean;
    proofSpecification: "Spec";
    graphEquivalenceAttempted: boolean;
    graphEquivalenceSpecification?: "EquivalenceSpec";
    invariantsChecked: readonly string[];
    propertiesChecked: readonly string[];
    deadlockChecked: boolean;
    symmetryUsedInProof: boolean;
    equivalent: boolean | null;
    graphHash?: string;
    tsStateCount?: number;
    tlcStateCount?: number;
    tsEdgeCount?: number;
    tlcEdgeCount?: number;
    proofOutput?: string;
    equivalenceOutput?: string;
}
export declare const compareGraphs: (tsGraph: StateGraph, tlcGraph: ParsedTlcGraph) => GraphComparisonResult;
interface BuildVerificationCertificateOptions {
    machine: ResolvedMachineDef;
    proofPassed: boolean;
    graphEquivalenceAttempted: boolean;
    graphComparison?: GraphComparisonResult;
    proofOutput?: string;
    equivalenceOutput?: string;
}
export declare const buildVerificationCertificate: ({ machine, proofPassed, graphEquivalenceAttempted, graphComparison, proofOutput, equivalenceOutput }: BuildVerificationCertificateOptions) => VerificationCertificate;
export {};