mbrotli 与 mzstd 用 Lean 4 形式化验证 RFC 一致性

mbrotli 和 mzstd 已用 Lean 4 对部分代码给出机器校验证明，确认其符合 RFC 7932 与 RFC 8878，但两者尚未成为完全验证的编解码器。证明通过 Charon 提取 MIR、Aeneas 翻译为 Lean，并在 CI 中检查翻译漂移；此前 mbrotli 0.5.16 曾因块计数从 u64::MAX 起算而接受 RFC 判定为非法的流，0.5.17 已修复。