>_ cat src/main.rs
今の自分を Rust で要約したもの。
rust25 lines
//! Profile: Keiya//!//! A low-level system engineer capable of handling everything//! from bare metal to web frontends. struct Engineer { name: &'static str, role: &'static str, attributes: &'static [&'static str],} const KEIYA: Engineer = Engineer { name: "Keiya", role: "Full Cycle Developer", attributes: &[ "Low-Level Programming", "Compiler Infrastructure", "Formal Verification", "Cloud Native DevOps", ],}; fn main() { println!("Building proprietary core systems...");}現在地
いまの重心だけを短く置く。
Core
Low-level programming, compiler infrastructure, formal verification, cloud native DevOps.
Approach
仕様、実装、検証、運用を分けず、一つの設計問題として扱う。
Current Focus
Radix と Wasm-Num を軸に、検証可能な低レイヤー基盤を積み上げる。
#Technical Focus
system_and_low_level/
- ├──Rust
- ├──Go
- ├──C / C++
- ├──LLVM
- ├──WebAssembly
- ├──Compiler Design
- ├──Wasm Runtime
- ├──JS Engine
formal_methods/
- ├──TLA+
- ├──SPARK
- ├──Lean 4
web_stack/
- ├──TypeScript
- ├──React / Next.js
- ├──Tailwind CSS
- ├──Node.js
- ├──GraphQL
- ├──PostgreSQL / MySQL
- ├──Redis
- ├──Discord Bot API
infrastructure/
- ├──Kubernetes
- ├──Docker
- ├──Terraform
- ├──Nginx / Caddy
- ├──GitHub Actions / GitLab CI
- ├──Prometheus / Grafana
- ├──Linux (Arch / Ubuntu)
- ├──Windows Server
#Selected Works
Radix
Formally verified foundation library for Lean 4 systems programming
Word、Bit、Bytes、Memory、Binary、Concurrency、BareMetal までを Lean 4 で形式検証する基盤ライブラリ。zero sorry と proof-erased abstractions を中核に据える。
Lean 4Formal VerificationSystemsLibrary Design
Theorems 1856
Definitions 1521
Trust assumptions 20
Wasm-Num
Formally verified WebAssembly numeric semantics
WebAssembly の数値セマンティクス、128-bit SIMD、線形メモリを Lean 4 上で検証。実装・証明・定理化を一体で進める数理寄りプロジェクト。
WebAssemblyLean 4SIMDSemantics
Definition Modules 70
Proof Modules 14
Sorry 0
Contact
© 2026 keiya.