不可信作者，可信答案：一种保真度分级翻译演算

本文把程序翻译建模为语言图上的有向、可组合契约，并区分精确性、过近似、可观察量、成本与保证等级。Lean 4 形式化了核心演算，hurdy-gurdy 实现了答案生成与图谱演化分离的系统；论文还报告了双路线一致性、见证回放、不可达性复核及架构发现的缺陷。