# Kgent 初の **LLM 駆動 eBPF 合成ツール**(別名 KEN。eBPF'24、ACM DOI:10.1145/3672197.3673434、arXiv:2312.05531)。([[@2026__eunomia.dev__eBPF × AI-LLMs - The Convergence of System Observability and AI]]) - 自然言語から eBPF プログラムを生成し、**Z3 ベースの記号検査(symbolic checks)とテスト**を組み込んで信頼性を高める。テスト集合で **約 80% の意味的正しさ(semantic correctness)**。 - LLM の生成だけに頼らず、形式的検証器(Z3)で「生成 → 検査 → 修正」の閉ループを回すことで、verifier に通る正しい eBPF を安定して出す設計。**AI for eBPF** の基盤研究で、[[GPTtrace]] の背後にある。 ## 横断比較 - 「LLM 生成 + 記号/意味検査」という構図は、本ソースが挙げる SimpleBPF(LLM 生成 + 意味検査 + LLM 最適化)とも共通し、**生成系を検証器で囲む**のが AI for eBPF の定石になりつつある。本 wiki の [[agentic SRE]] が緩和で「安全に巻き戻せる反復」([[Transactional No-Regression]])を要とするのと同様、システムコード合成では「形式検証で囲んだ反復」が信頼性の源泉になる。 ## 関連 - 本ソース: [[@2026__eunomia.dev__eBPF × AI-LLMs - The Convergence of System Observability and AI]] - 実装プロジェクト: [[GPTtrace]] - 開発元: [[eunomia-bpf]] / [[Yusheng Zheng]] - 関連概念: [[eBPF]]