Lasmは、開発者が関数型プログラミング言語および定理証明機であるLean 4でアプリケーションを記述し、それをWebAssembly（Wasm）にコンパイルすることを可能にすることで、形式的検証と現代的なWebデプロイの架け橋を提供します。ロジックが主にユニットテストを通じて検証される標準的なWeb開発とは異なり、Lasmは特定のルールに従ってコードが正しく動作することを保証するために形式的証明の使用を可能にします。このアプローチにより、開発者はコードをデプロイする前に、認可ロジック、データバリデーション、ページネーションの一貫性などのプロパティを証明することができます。
この画像は、Lean 4およびWebAssemblyのためのLasmツールチェーンのコア機能を表しています。
このツールチェーンは、Node.js、AWS Lambda、Vercel、Cloudflare Workersを含む幅広いデプロイターゲットをサポートしています。各環境に対して特定のビルドターゲットを提供することで、異なるランタイムの複雑さを処理します。例えば、Node.jsビルドではスレッドやソケットなどのLeanのフルランタイム機能を活用できる一方で、エッジおよびブラウザビルドは、それらの特定の機能を備えずにシングルスレッドで動作するように最適化されています。また、Lasmは、基礎となるロジックを検証可能な状態に保ちつつフルスタックアプリケーションの構築を容易にするために、HTTPリクエスト用のLasm.Fetchやブラウザ操作用のLasm.UIといった一連のライブラリを提供します。
Lasmの主要な機能の一つは、検証済みのロジックをクライアントとサーバーの間で共有できることです。共有のLeanファイルでルールを一度定義するだけで、開発者はブラウザアプリケーションが無効なリクエストを送信しないこと、およびサーバーが同じルールを満たすリクエストのみを処理することを証明できます。これにより、フロントエンドとバックエンドでバリデーションロジックに不一致が生じる一般的なバグのクラスを排除できます。ただし、このシステムには定義された境界があります。アプリケーションのロジックは形式的に検証されますが、基礎となるJavaScriptランタイム、SQLデータベースの実行、およびJSONシリアル化レイヤーは形式的証明の範囲外となります。これは、システムがインフラスタック全体の絶対的な信頼性ではなく、アプリケーションの内部ロジックの正当性を保証することを意味します。