MAGS：为 AI 代码特定安全属性提供机器检查保证

研究人员推出多智能体框架 MAGS，利用 Dafny 作为中间表示，为 AI 生成的代码提供可由机器检查的形式化安全保证。该框架将生成代码转化为 Dafny 并依据验证器反馈修复违规，最终编译回可执行程序。在 100 个 CUDA 内核、100 个终端脚本和 20 个机械臂任务共 220 个测试示例中，其生成成功率达 100%。