English · 繁體中文 · 简体中文

Building verifiable agent systems, sandboxed execution runtimes, and formal mathematics tools. 致力於打造可驗證的自主 Agent 架構、內核沙盒執行環境與形式化數學證明系統。

Mathematics Division, Department of Mathematics and Information Education, National Taipei University of Education (NTUE), expected 2028. Based in Taipei, Taiwan.
國立臺北教育大學 數學暨資訊教育學系 數學組（預計 2028 年畢業）。

📑 Curriculum Vitae (CV) · 🐙 GitHub · ✉️ Email

• DSH Architecture Lab
  Production-grade autonomous agent research laboratory for DeepSeek Harness.
  Features kernel-level Lima Linux VM isolation, micro-cent token broker metering, immutable cryptographic research protocols (review-protocol.json), and factorial empirical trials across multiple memory and planning recipes (A/B/C/D). Verified 100% test pass rate with DeepSeek-V4.1-Flash.
• RuleShift
  Deterministic local testbed evaluating agent memory adaptation under dynamic rule changes.
  Encompasses 800 paired tasks with automated state verification and replayable evidence. Empirically demonstrated that foundational retrieval delivers top-tier 95.6% success rates with superior cost efficiency.
• DSH Second Agent Kit
  macOS defense-in-depth security and memory isolation suite for DeepSeek Harness.
  Combines macOS Seatbelt kernel profiles (network restrictions, local socket channels), interactive circuit breakers (anti-deadlock protection), and AsyncLocalStorage-based project memory isolation.
• MiniHarness
  Comprehensive 8-step AI Agent Harness engineering curriculum and workshop in Python.
  Provides an offline-first learning path from tool dispatch and agent loops to memory palaces and production-grade architectures, accompanied by a complete Traditional Chinese curriculum.
• Verified Search Plugin
  Source-verifiable, hallucination-resistant retrieval workflow for DeepSeek Harness.
  Backed by 250+ unit tests and 42 frozen benchmark corpora, featuring structured JSON extraction and explicit evidence-gap tracking (unresolved).

• ProofWeave Core
  Structured mathematical claim verification platform powered by Lean 4.
  Transforms natural and structured mathematical arguments into inspectable certification runs, rigorously separating formal proof validity (Lean 4 kernel checked) from semantic statement alignment.
• SAIR Proof Press
  Equational implication solver companion with heuristic search and Lean 4 certificate generation.
  Provides public companion datasets, immutable benchmark artifacts, released-input evaluation suites, and an accompanying academic paper.
• Finite Witness
  WebMCP-integrated finite-graph counterexample search tool.
  Features bounded exhaustive search, client-side data sovereignty, inspectable certificates, and an independent Python replay verifier.

• HonestCI
  Developer-first GitHub Action and CLI that makes green CI truly meaningful.
  Wraps test execution, verifies fresh and uncorrupted JUnit XML evidence, guards against test-count drops relative to trusted default branches, and detects false-green CI anti-patterns (v1.0.4 on npm & GitHub Marketplace).
• RigorGraph
  Local-first claim-evidence DAGs and deterministic audit reports.
  Enforces four-eyes review principles (separation of author and independent reviewer duties), detects DAG cycles, computes SHA-256 byte fingerprints, and outputs portable offline HTML audit dossiers.

• TokenScope
  Interactive bilingual browser laboratory for LLM causal attention, token sampling, and BPE.
  Features inspectable $5 \times 5$ self-attention matrices, temperature/top-k/top-p probability distribution controls, and a fully reversible Unicode BPE tokenizer.
• Charlie Alpha 4B
  Trilingual statistical procedure-selection model optimized for Apple Silicon MLX.
  Provides reproducible statistical decision assistance with built-in cautious clarification fallbacks (needs_clarification) for ambiguous problem formulations.
• DeepSeek Girl Pets
  16-direction animated companion plugin for DeepSeek Harness & Codex Desktop.
  Zero DOM pollution, native lifecycle hook synchronization, and 100% offline privacy preservation.

1. Keep Evidence Attached to Claims: Claims without verifiable computational evidence remain conjectures. Every conclusion must be grounded in replayable artifacts.
2. Defense-in-Depth & Fail-Closed Design: Sandbox boundaries, Token budgets, and execution timeouts must fail closed, protecting system integrity and user resources.
3. Determinism & Reproducibility: Research tools and benchmarks should operate 100% offline with pinned seeds and cryptographic hashes, eliminating dependence on external network states.
4. Constructive Open-Source Craftsmanship: Deliver robust, well-documented, and human-friendly software that empowers developers, students, and researchers alike.

_{Designed with precision in Taipei · Open to software engineering & AI research internships.}