~/keiya
Keiya profile icon

keiya

Low-Level System Developer / Full Cycle Engineer

Rust、Lean 4、インフラ、Web をまたぎながら、低レイヤーの設計とプロダクト実装を同じ連続面として扱う。

>_ 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
Open repository

Wasm-Num

Formally verified WebAssembly numeric semantics

WebAssembly の数値セマンティクス、128-bit SIMD、線形メモリを Lean 4 上で検証。実装・証明・定理化を一体で進める数理寄りプロジェクト。

WebAssemblyLean 4SIMDSemantics
Definition Modules 70
Proof Modules 14
Sorry 0
Open repository

#Awards & Connect

U-22

U-22 Programming Contest 2025 Director-General of the Commerce and Information Bureau, Ministry of Economy, Trade and Industry Award

形式検証、システムエンジニアリング、そして実装から運用まで閉じるフルサイクル開発が現在の重心です。

>_ Connect

公開している導線。

Contact

© 2026 keiya.