制約条件下での記述体験 — Claude Code が Lean 4 でリソース制約を検証
Hiroba による自動要約
Claude Code が無制限のリソース消費を前提とした実装を生成し、本番環境で OOM やファイルディスクリプタ枯渇に至る問題を解決するため、Lean 4 の型システムでメモリ使用量やオープンファイル数の上限を型に埋め込み、コンパイラが自動検証する手法を実装。型制約を緩い状態で AI に渡し、制約を有効化すると実装が自動的に最適化される。
読んで良かったら、シェアしてみてください。
同じタグの記事が他に 1937 件あります。
関連する記事
同じタグの記事
Claude Code だけで要件定義から本番デプロイまで完走した話 - サモエドカフェのファンサイトを実働10時間で作った
Zenn個人開発者が Claude Code を要件定義から本番デプロイまで使い、サモエドカフェのファンサイト「アルファン」を実働10時間未満で完成させた。並列エージェントで7件の Issue を同時処理し、本番バグとデータ消失も AI の支援で復旧。開発のプロセスが「コード実装」から「仕様判断と品質確認」にシフトした実例
Claude「Computer Use」を本番環境で安定稼働させるための実践ガイド
ZennAnthropic公式がComputer Use機能を本番環境で信頼性高く動作させるためのノウハウを公開。クリック精度改善、Thinking Effortの選択、コンテキスト管理、デモンストレーション記録など4つのポイントを通じ、UIを自律操作するエージェントの実装と運用方法を解説している。
Codex CLIは年640TBをSSDに書き込み、Claude CodeはKYC要件で中国ユーザーを排除
QiitaOpenAI Codex CLIが2週間で37TBをSSDに書き込み、年間640TBの異常な書き込み量が判明。一方、Claude Codeへの移行も、2026年4月のKYC（身分確認）強制化により、中国本土ユーザーはアカウント即無効化リスクに直面。どちらのツールも実用性に重大な問題を抱えている。
AI の主導権争い、3 つの戦線が動いた
ZennOpenAI が Broadcom と共同開発した推論チップ「Jalapeño」を発表し NVIDIA からの脱却を宣言。同時に Anthropic は Claude Code のオープンソースリポジトリを公開し、エージェント構築を数分で実現可能にした。さらに OpenAI は「Daybreak」で AI による脆弱性の自動発見・検証・修正を発表し、セキュリティの AI 化が加速している。