{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.002204056,0.0006274341,0.0002758629,0.0009782667,0.0003166491,0.000939395,0.001016874,0.0006669807,0.0195896],"category_scores_gemma":[0.00902334,0.0005104151,0.0006404943,0.0003939084,0.0006493048,0.001001518,0.001412732,0.0009885484,0.005143194],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0006647307,"about_ca_system_score_gemma":0.00159417,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0009538629,"about_ca_topic_score_gemma":0.001503816,"domain_scores_codex":[0.9985933,0.0004417089,0.00009768458,0.0001975595,0.000576974,0.00009273842],"domain_scores_gemma":[0.9962644,0.001988525,0.0002177295,0.0008151167,0.0006500474,0.00006422673],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0006455463,0.0003682624,0.005640831,0.001523744,0.00012297,0.0014199,0.001403408,0.09811725,0.06614171,0.2672022,0.08773039,0.4696837],"study_design_scores_gemma":[0.0003179121,0.0002231528,0.0008511972,0.0002573929,0.0000537302,0.0008019956,0.0002065488,0.6189296,0.09948589,0.06388628,0.2149159,0.00007051825],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.009290351,0.00007630691,0.9467198,0.000237148,0.00007643145,0.0003328726,0.001959197,0.03331327,0.007994597],"genre_scores_gemma":[0.1817103,0.0002605812,0.780997,0.0003772106,0.00004172122,0.001341656,0.008865371,0.01099189,0.0154143],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.0195896,"threshold_uncertainty_score":0.06553376,"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."}}