{"id":"W7125896959","doi":"10.1109/ase63991.2025.00110","title":"Agentic Specification Generator for Move Programs","year":2025,"lang":"","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"","keywords":"Verifiable secret sharing; Toolchain; Key (lock); Code generation; Modular design; Specification language; Focus (optics); Generator (circuit theory); Programming language specification","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.001360856,0.0002803172,0.0002728707,0.0002408664,0.0003603127,0.0007999174,0.001369734,0.0002032721,0.00006552065],"category_scores_gemma":[0.0002768456,0.0002848215,0.0001991863,0.001393875,0.0001365579,0.0007233894,0.0002428071,0.0001532313,0.0001472838],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0002187354,"about_ca_system_score_gemma":0.0003004026,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001116926,"about_ca_topic_score_gemma":0.000003257251,"domain_scores_codex":[0.9972509,0.0001892315,0.0007776847,0.0009416672,0.0003024017,0.0005381155],"domain_scores_gemma":[0.9975009,0.00009434992,0.00025947,0.001499636,0.0005282799,0.0001173524],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00001475723,0.0001565877,0.00006312352,0.0001022809,0.00002819039,2.21711e-7,0.0001930169,0.00002011594,0.001532006,0.5204656,0.001683774,0.4757404],"study_design_scores_gemma":[0.0005490844,0.000177326,0.001935707,0.00007517716,0.00005501967,0.000001793935,0.00008663184,0.797953,0.06872571,0.01694397,0.1131507,0.0003458693],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.001749673,0.0005807266,0.9755205,0.001381432,0.004846896,0.002412723,0.000004287383,0.0002142347,0.01328956],"genre_scores_gemma":[0.07669477,0.0000885339,0.9017176,0.0005904314,0.0002560936,0.0005064039,0.00001686041,0.00001648523,0.0201128],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.7979329,"threshold_uncertainty_score":0.9999604,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.06807825008260023,"score_gpt":0.3411191454062153,"score_spread":0.2730408953236151,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}