关于
我最强的项目通常位于证明、算法设计和实际工程之间。我会认真处理精确输入格式、失败路径、可复现命令，以及哪些内容已经验证、哪些还不能声称完成。
当前工作包括 Lean 4 形式化、Euclidean domain 与类似 PID 结构上的 normal forms、稀疏矩阵基准、面向证书的运行时监控，以及假设需要保持可见的数据流程。
精选项目
每张项目卡都说明现有内容是什么，它证明或测量了什么，以及当前 claim 的边界在哪里。
HPC 基准测试框架
一个 C++ CPU 稀疏矩阵基准框架，读取 Matrix Market 输入，把 coordinate 数据转为 CSR，运行 serial 与 OpenMP SpMV，并写出 timing、throughput 和 checksum 字段。
公开 case study 的范围很明确：Hyak job 34825519 是 96-core mem2x run，job 34852262 是 32-core Eigen comparison。
模型评估流水线
一个 Python/uv 的 pre-Hyak 本地数据工厂，用于数学 distillation 实验。它把生成、normalization、verification、SFT packing、cost log、report 和 data manifest 放进同一个 CLI 流程里。
这个仓库停在可复现的本地 gate 和 Hyak handoff runbook：会产出 JSONL artifact 与 manifest hash，但不声称已经提交或运行 GPU training jobs。
Agent 安全基础设施
一个 Rust workspace，配合 Lean 4 侧规范，围绕 certificate-oriented runtime monitor 展开。gRPC schema 表达的 decision 可以携带 allow certificate 或 deny witness，也包括用于 review 的 policy-diff evidence。
Lean-side soundness 和 FFI integration 仍按保守状态处理；可执行路径目前依赖 Rust checker machinery 与 protobuf contract。
公共议题数据分析
一个用于 Seattle transit restoration 的 Python 分析仓库，重点是 schedule-based 数据：King County Metro 官方 GTFS、Transitland 历史 GTFS、NOAA 天气数据和 ACS demographics。
这里的 optimization claim 应理解为 static-data connectivity analysis：routing modules、candidate generation 和 MIP optimization。 GTFS-RT scripts 存在，但不是这里 restoration 结果的依据。
图像工具
一个 FastAPI + React/Vite 的图像调色
MVP。后端接收上传图片，返回 schema-backed
ImageAnalysis，其中包含三个
StyleVariant presets。
它有价值的部分是可编辑性：每个 variant 都保留明确的 tone/color 参数和预览卡片。当前 analyzer 仍是 MVP/mock variants，所以不会写成 production ML grader。
IoT 案例研究
一个用于观察室内空气质量的小硬件项目：ESP32-C3、SEN55、板载 OLED、ESPHome 固件，以及接入 Home Assistant 的 PM、温湿度、VOC 和 NOx 趋势数据。
这篇 case study 记录 parts list、wiring table、firmware YAML、display 行为，以及最终定位到真实 I2C pins 的黑屏排查路径。
更多作品
这些 artifact 范围比精选项目更窄：有些是我构建过的小工具，有些是学习、实验或参考上游生态的上下文。
文章
我用这些文章记录 decision trail：尝试了什么，哪些证据算数，哪里失败了，以及哪些 claim 暂时不该写进去。
