Yoichi Hirai

Somebody asked me if I'm back. I said yes!

Julian Sutherland - FRI in ArkLib + Yoichi Hirai - Vibe FRI RBR soundness (February 9th, 2026) YouTube video by Verified zk(E)VM

what we say when we talk about formalizing FRI www.youtube.com/watch?v=tFbT...

I'm helping formal verification of arithmetic circuits (clean) and formalization of cryptography (round-by-round soundness of FRI). I want to connect these with implementations.

round-by-round soundness of FRI: blog.zksecurity.xyz/posts/simple...
clean: blog.zksecurity.xyz/posts/clean/

10th Workshop on Trusted Smart Contracts: late submission is still open: ifca.ai/fc26/wtsc/cf...

GitHub - pirapira/reasonable-manifesto: Reasonable Engineering Manifest Reasonable Engineering Manifest. Contribute to pirapira/reasonable-manifesto development by creating an account on GitHub.

3. Part of mathematics is reasonable.
github.com/pirapira/rea...

GitHub - pirapira/reasonable-manifesto: Reasonable Engineering Manifest Reasonable Engineering Manifest. Contribute to pirapira/reasonable-manifesto development by creating an account on GitHub.

1.1.1. Reasoning in this manifesto means deductive reasoning. github.com/pirapira/rea...

yoichihirai.com/b/posts/ital...

I was comparing formal verification frameworks for arithmetic circuits: blog.zksecurity.xyz/posts/formal...

yoichihirai.com/b/posts/2025...

Math is the archetype reasonable system. People are gathering statements = specifications: mathstodon.xyz/@tao/1145865...

My reasonable engineering manifesto is still changing. github.com/pirapira/rea...

sounds like it's getting there.

GitHub - pirapira/reasonable-manifesto: Reasonable Engineering Manifest Reasonable Engineering Manifest. Contribute to pirapira/reasonable-manifesto development by creating an account on GitHub.

My reasonable engineering manifesto is getting in shape. I'll edit it a bit more. github.com/pirapira/rea...

GitHub - pirapira/reasonable-manifesto: Reasonable Manifest Reasonable Manifest. Contribute to pirapira/reasonable-manifesto development by creating an account on GitHub.

I started writing reasonable manifesto for systems that can be reasoned about github.com/pirapira/rea...

Once getting QED is automated, the bottleneck is me wanting statements to be proven. I will want statements proven about things with short specifications: the reasonable systems.

ping

I ignored navigation apps and found a nice ride.

If something is described as avocado green, how are you supposed to know if that means outside or inside?

何が大事かなあ。

You can get bedsheets made with RFC printed on it

「朝のドラめもん」くらい安定した質のものを毎日書いて何十年にもわたって公表するのは、よいなと思う。公表の媒体も、テキストだけのHTMLを自分のWebサーバに置くだけで、長期的に維持するのに向いていてよいなと思う。

I'm making up a technical term called reasonable systems. A reasonable system can be reasoned about with theorem provers, SMT solvers, model checkers or such. The behavior of a reasonable system can be described with a relatively small amount of logical formulas.

Ein Tipp gegen die Hitze: Nutze den südlichen Gehweg. Dieser liegt öfter im Schatten.

昨日わざわざ北側の日が当たる歩道を使ってる人もいっぱい見た(ドイツ)。

oi!