Show HN: Arcstone-Airlock-Blueprint – Offline Charon/Aeneas/Coq for Rust

AI 摘要

开发者发布了一个名为 Arcstone-Airlock-Blueprint 的开源模板，用于对裸机 #![no_std] Rust 代码进行离线形式化验证。该方案在不修改目标 crate 源码、不引入验证宏的前提下，通过 Charon 提取 LLBC、Aeneas 合成 Coq 代码，再用 Coq 8.18.0 证明生成代码与规范等价；整个验证在断网、只读、降权的容器中运行，并输出审计文件确认没有额外公理假设。