E06证据记录
日期：2026-09-28 UTC
Python：3.12.3
Java：OpenJDK 21.0.12
TLA+ Tools：v1.7.4；TLC 2.19（2024-08-08）；pcal.trans 1.11（2020-12-31）
官方JAR SHA-1：bee4a54f3ee3d4afc347c3240ec2d9e93b075104（本地下载逐字相同）

全部TMPDIR、TMP、TEMP和java.io.tmpdir指向仓库examples/distributed-systems/.build/e06/tmp。TLA+ JAR、自动翻译产物、状态队列与日志均在.build/e06，没有把生成的翻译段写回正式源。

正式源码SHA-256：
- check.py 306cd8f7eab6db61c4af5f876010c7cc3bd17281f498aa96e1e3563fa40240f4
- LockAtomic.tla 016fb5fdf3d6fdfa51510c54369dc0346f7d0d72f6ecb6de01e4d383bbf09b65
- LockSplit.tla 9f590083191a8455efab7579db6c9bf9d9712612c18646cfbb26560adf042ae6
- Lock.cfg 47fd974c1b918a54196a93e41f739edd21f3f4b702f339ee58ebbc12253da39d

Python有限模型正式运行退出0，--help退出0，非法scenario退出2。正确模型访问15个状态且没有互斥反例；拆分检查/授予模型访问24个状态，保存6步可重放反例；无公平stutter lasso门槛通过。生成observations.json SHA-256为ccbd1e7d72e27b2955a6a5282e2db82955b07f43871bd09663eb9e8fb84e2439，与随文observations.json.txt逐字一致。

PlusCal最终运行：
- LockAtomic.tla翻译退出0；TLC单worker退出0，30个状态生成、21个不同状态、队列归零，TypeOK、MutualExclusion及弱公平下Termination均通过。
- LockSplit.tla翻译退出0；TLC单worker按预期退出12，在第7层报告MutualExclusion违例，状态中c0与c1均为held。

首轮TLC在PlusCal已翻译后仍以150退出：规格使用小于等于但没有EXTENDS Naturals，SANY无法解析运算符。正式源补齐Naturals后重新从副本翻译并取得上述最终结果。该错误说明翻译成功、语义分析成功和性质检查成功是三道不同门槛。

anti-ai-tone tech profile：2305汉字、0错误、0提醒；随后anti-persona-fabrication人工扫描第一人称叙事、拟人化和说书人腔，0命中。

Hexo构建与页面静态核验：
- 默认Node v20.18.0因Hexo依赖的strip-ansi ESM/CJS兼容错误退出2，未记为通过。
- 根目录旧db.json约104 MiB，空缓存构建前已可恢复地移入examples/distributed-systems/.build/e06/db.before-build.json；没有手改public/。
- 使用/opt/cloudcli/node/bin/node v22.16.0从空缓存执行npm run build，退出0，38秒生成5678个文件；日志保存于examples/distributed-systems/.build/e06/hexo-build-fresh.txt。
- 正式HTML的title、正文结尾、E05生成页链接、5个Mermaid源码块和3个附件链接均存在；生成的3个附件与源文件逐字一致。
- 当前云端没有可用浏览器，未验证Mermaid客户端SVG渲染、视觉尺寸、点击下载或控制台错误。

来源和反向勘误核查见writing-plans/distributed-systems/research/E06-formal-verification.md。没有运行IronFleet/Dafny代码或其性能实验。