Show HN: Lasm – Leanで形式検証されたWebアプリをNode/serverless/edge向けに記述
Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge (github.com)
要約
Lasmは、Lean言語を使用して形式検証されたWebアプリケーションを開発するためのフレームワークです。Leanは、汎用プログラミング言語でありながら形式検証機能を内蔵しており、フロントエンドからバックエンドまで、あらゆるWebアプリをLeanで記述し、その正しさを検証できます。このプロジェクトは、AIアシスタントClaude Opus 5.5の協力を得て開発されました。
全文翻訳
Lasmは、2026年の大半を費やして私の夢としてきました。形式検証はソフトウェアエンジニアリングとプログラミング言語の次の進化形であると確信しています。この次の波は、形式検証とそのプログラミング言語を理解する信じられないほど知的なLLMによって、大部分が実現されるでしょう。
Leanは形式検証を可能にする最も人気のある言語の一つであり、私にとっては、形式検証が直接組み込まれた汎用プログラミング言語であるため、信じられないほど強力です。
Leanで汎用ソフトウェアを構築し、Leanで形式検証することができます。素晴らしいです。
LasmはLeanをブラウザ、Node、serverless、およびedge環境（その他多数）にもたらします。そのアイデアは、仕様の形式検証を備えたExpressサーバーやHonoサーバーをCloudflare Workers上で実行できるということです。
私はソフトウェアエンジニアリングに重点を置くエージェンティックエンジニアであり、Lasmは主にClaude Opus 5.5が私のハイレベルな指示に基づいて構築したものです。