实验室在 GitHub 开源了量子纠错证书库 QECCertificates：一个用 Lean 4 写成的形式化库，为量子纠错码的码参数与故障距离提供机器可复核的证书。
为什么做这件事
码参数是搜出来的，而一次搜索以某个求解器的判决收尾。公开的 qLDPC Challenge schema 把这件事的代价写在了自己的文档里：未经认证的距离只报成上界——非 CSS 码是因为 Pauli 重量认证器尚未提供，线路级距离是因为精确档列为未来的工作。出路有两条：相信打印出这个数的那个工具，或者让这个数自带一样第三方能检查的东西。QECCertificates 走第二条路：搜索问题的编码、证书检查器的可靠性，以及两者的复合，都是定理；每条承重声明都印在审计区里，读者能看到它依赖哪些公理。
库里有什么
- GF(2) 线性代数：可信行消元、核基、秩证书、对偶见证、精确距离的夹逼、超图积与提升乘积、Künneth 公式；
- Pauli 层：算符树与辛表示之间的翻译；
- 证书框架：内核复核的 LRAT/RUP 检查器及其可靠性定理，双向的编码忠实性——CNF 的一个模型就是一个轻逻辑算符——以及保持不可满足性的对称性破缺；
- 码论层：稳定子码、CSS 码与子系统码，gauging 与测量协议的表示，以及 Bacon–Shor、BB、HGP、提升乘积等共享实例族。
它保证了什么
全库共 57 个模块，审计区覆盖包里每一条非私有定理与引理——没有审计不到的角落。零 sorry、零自定义公理、零 native_decide；受审计声明不依赖 propext、Classical.choice 与 Quot.sound 之外的任何公理。证书检查器与任何求解器不共享一行代码——UNSAT 判决只由公式与证明文件重新推出。
项目以 Apache-2.0 许可发布，已归档到 Zenodo 供学术引用（DOI：10.5281/zenodo.23056679）。