Medium

Hideaki Takahashi

Pinned

Hideaki Takahashi

·

Oct 19

I Tried to Formally Verify Popular Rust Projects with Lean 4, but Found More Bugs Than I Expected

I tried building a benchmark for formally verifying popular Rust OSS. Along the way, I ended up finding real security vulnerabilities.

I Tried to Formally Verify Popular Rust Projects with Lean 4, but Found More Bugs Than I Expected

Pinned

Hideaki Takahashi

·

Oct 6

Proving Rust Web Application Correctness with Lean 4

AI coding agents such as Claude Code and Codex are making it possible to build surprisingly large web applications in a very short amount…

Proving Rust Web Application Correctness with Lean 4

Hideaki Takahashi

·

1d ago

Building a Mini Lean 4 from Scratch: Implementing an Interactive Theorem Prover in Rust

Everyone is talking about interactive theorem provers like Lean 4 and Coq right now. From formalizing frontier mathematics to verifying…

Building a Mini Lean 4 from Scratch: Implementing an Interactive Theorem Prover in Rust

Hideaki Takahashi

·

5d ago

I Rebuilt an AI Gateway in Rust. It Became 41× Faster.

Reimplementing LiteLLM with Rust with h5i-app, optimizing streaming and database operations, and formally verifying core logic with Lean 4.

I Rebuilt an AI Gateway in Rust. It Became 41× Faster.

Hideaki Takahashi

·

Sep 29

i5h: Build a Rust Web App and Prove Its Behavior with Lean 4

> NOTE!! i5h is now part of h5i, and the latest tutorial is available at…

i5h: Build a Rust Web App and Prove Its Behavior with Lean 4

Hideaki Takahashi

·

Sep 27

How JWT Authentication Actually Works

A tutorial guide to what a token contains, how its signature is checked, and where the trust boundary lies.

Hideaki Takahashi

·

Sep 21

Building a Browser Without V8: What Broke, and What Worked

While V8 has dominated JavaScript execution for decades, we tried building a practical browser around Boa, a JavaScript engine written in…

Building a Browser Without V8: What Broke, and What Worked

Hideaki Takahashi

·

Sep 18

Think Like an Attacker: CI/CD Security in the AI Era

How to turn a working exploit into a repeatable GitHub Actions test with h5i

Think Like an Attacker: CI/CD Security in the AI Era

Hideaki Takahashi

·

Sep 10

Top 20 AI Agent Pen-Testing Tools for 2026: The Ultimate Guide

Traditionally, we have spent a lot of effort to automate a penetration test, mostly by automating individual tools. For example, Nuclei ran…

Hideaki Takahashi

·

Sep 7

Do We Still Need Burp Suite for Web Security Testing?

Burp and ZAP were built more than ten years ago, while AI agents can solve many CTF / bug-detection benchmakrs with CLI tools.

Hideaki Takahashi

Hideaki Takahashi

PhD @ Columbia researching AI & system security | https://github.com/h5i-dev/h5i (Axum‑based Rust web framework designed for formal verification with Lean 4)

Following

Help

Status

About

Careers

Press

Blog

Store

Privacy

Rules

Terms

Text to speech