I’ve been telling people for the last 25 years that Jane Street as an organization was just not interested in formal methods. I’m not saying that anymore. It’s not exactly that I think we were wrong all those years. To be clear, we’re strong believers in the power of tools to help us write better and more reliable code. And type systems are a kind of lightweight formal method that we’ve gotten an
このブラウザ バージョンのサポートは終了しました。サポートされているブラウザにアップグレードしてください。
Kernel/VM 探検隊@つくば No3 で使用したスライドです。
そろそろ懐が寂しいので終わりです。ご協力ありがとうございました！ Lean 4で作っている正規表現エンジンを、もっと便利で実用的なライブラリにするために、一緒に開発・証明してくれる仲間を募集しています。せっかくなので、今回はいくつかのIssueにバウンティを設定してみることにしました。 github.com Leanや形式検証に興味がある方、Unicode周りが好きな方、正規表現エンジンの内部に触れてみたい方ならどなたでも歓迎です。 取り組む Issue は自由に選べますし、実装方針の相談やレビューは気軽にどうぞ。必要なら背景説明や資料も用意します。 報酬について 対象 Issue を解決して PR がマージされたら1件につき10万円〜のバウンティをお支払いします。重めのタスクはマイルストーンに分けて途中支払いもできますし、難しい部分を突破したときの追加ボーナスもあります。 こんな方に向い
本記事はエクサウィザーズの Advent Calendar 15日目の記事です。 本記事の目標 先端技術開発グループ（WAND）の佐藤碧です。2025年12月にAWSで開催されたAWS re:Inventに参加してきました。 このChalk talkの一つに「Verifying the safety of the Rust standard library」というものがあり、ここで紹介されていたkaniというAmazonが作成しているOSSがとても面白いものでした。kaniがどのようなOSSかを解説し、使い方の一例を紹介します。 Rust standard library Rustのcoreとstdクレートには27,000以上の関数が含まれています。このうち、unsafeな関数は7,000以上あり、unsafeなコードを安全にラップしたものは2,300以上あります。 標準ライブラリのバグは
Machine Logic At the junction of computation, logic and mathematics 05 Dec 2025 [ memories LCF HOL system Isabelle Coq MJC Gordon ] Crackpots ranging from billionaire Peter Thiel to random YouTube influencers claim that science has been stagnating for the past 50 years. They admit that computing is an exception: they don’t pretend that my personal 32GB laptop is not an advance over the 16MB mainfr
Published by Martin Kleppmann on 08 Dec 2025. Much has been said about the effects that AI will have on software development, but there is an angle I haven’t seen talked about: I believe that AI will bring formal verification, which for decades has been a bit of a fringe pursuit, into the software engineering mainstream. Proof assistants and proof-oriented programming languages such as Rocq, Isabe
The Ironclad Operating System Kernel Ironclad is a (partially) formally verified, real-time capable, UNIX-like operating system kernel for general-purpose and embedded uses. It is written in SPARK and Ada, and is comprised of 100% free software. Ironclad features a familiar POSIX-compatible interface, true simultaneous preemptive multitasking, Mandatory Access Control (MAC), and support for hard r
はじめに こんにちは、2025 年新卒で ABEMA の広告配信システム開発チームに所属している戸田朋花です。 生成 AI を活用したアプリケーション開発では、「ハルシネーション」と呼ばれる問題がしばしば課題になります。これは、生成 AI がもっともらしく見える誤情報を自信満々に出力してしまう現象です。 こうした問題に対して、形式的な検証技術を応用し、ハルシネーションの発生を抑制する新しいサービス「Automated Reasoning checks」が先日 AWS 上で GA されました。 本記事では、この 「Automated Reasoning checks」を実際に試してみた内容を、検証結果とあわせてご紹介します。 Automated Reasoning checks とは Automated Reasoning checks は Amazon Bedrock Guardrails
はじめに こんにちは、2025 年新卒で ABEMA の広告配信システム開発チームに所属している戸田朋花です。 生成 AI を活用した開発が広がる中で、コードを書くこと自体のハードルは大きく下がりました。 一方で、生成 AI に「どのようなシステムを実装して欲しいのか」を正確に伝える難しさを日々感じています。 2 週間ほど前には spec-driven development を掲げた AI 統合開発環境の Kiro が AWS からリリースされ、話題となりました。 Kiro ではユーザーとの対話を通じて Requirements, Design, Task list を順に作成することで、まずシステムの設計を明確にしてからコーディングに入るプロセスが取られています。この方法は冒頭で述べた課題に対する 1 つのアプローチになるでしょう。しかし、依然として生成 AI と自然言語で設計の微妙な
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Formal or not formal? That is the question in AI for theorem proving.
