Inferaraの研究
Inferaraが研究を行うのは、厳密な基礎的正当化と理論的評価が、ともに将来の成功への鍵を握ると信じているからです。憶測ではなく、既存の文献や出版物、その他利用可能な情報源を綿密に分析することで、考えを証明します。
Inferaraの研究領域
Web3のセキュリティ
Web3のセキュリティ領域は、ブロックチェーンコード自体のセキュリティとDAppsコードのセキュリティで構成されます。(ただし、これらに限定されるものではありません。) これら2つを、Inferaraの研究成果の対象とする応用分野と考えています。
数学的定理の証明
Inferaraの研究は、自動推論システムや形式的検証手法の可能性を広げることを目指しています。主なツールとして、Rocq(Coq)とTLA+を使用しています。
コードの正確さ
Inferaraは、コードが意図したとおりに動作し、脆弱性を排除し、信頼性を向上させる方法論の開発に専念しています。Inferaraが推し進めるアプローチは、最初の開発段階から、重要なコードセグメントに対して正式な仕様と正式な証明を用いることです。
Inferaraのビジョン
Inferaraは、帰納的推論を用いて開発したモデル上で、コードの正式な特性を証明したいと考えています。
Inferaraは、抽象的なパラメーターだけでなく、それらのパラメーターのインスタンス化もサポートすることを目指しています。
Inferaraは、信頼できる小さなコードベース(機械によるコード生成は除く)を使って、ミニマルかつ明快な方法で証明を構築したいと考えています。
これらの機能を提供するだけでなく、「大規模なプログラミング」や抽象化の構築にも対応できるフレームワークを求めていきます。
これらのテーマに対する情熱を共有し、共同研究の機会を探ることに興味をお持ちの方は、ぜひご連絡ください。Inferaraのチームは、この分野を前進させるためのパートナーシップやプロジェクトに関する議論を心待ちにしています。Inferaraのソーシャルメディアの詳細は、メインページでご覧いただくか、お問い合わせページから直接お問い合わせください。