自动完美检查AI生成代码

我的经验：应用Kani的形式验证到ChatGPT建议的 Rust 代码。

你喜欢类似ChatGPT和GitHub Copilot之类的AI编码工具吗？你讨厌它们所生成的代码不能获得信任吗？

在一些（目前仅有限的）情况下，你可以相信他们的代码！使用形式化验证工具，如针对Rust的Kani，我们有时可以自动证明AI生成的代码的正确性，并具有数学确定性。我的RangeSetBlaze库现在包含一些这样的代码。

Rust已经为内存管理提供了数学上的确定性。在本文中，您还将了解如何使用Kani来扩展这种确定性。您会发现Kani对人工和AI生成的代码都很有用。