Fstar lang

Fstar lang 的网站。

Pulse：基于并发分离逻辑的证明导向编程（输出 C/Rust）

F 官方教程新增 Pulse 章节：Pulse 是嵌入 F 的 DSL，面向可变状态与并发编程，规格与证明基于并发分离逻辑，灵感来自 Iris，但核心逻辑 PulseCore 完全在 F* 内形式化。示例展示用 pts_to 断言描述指针指向关系，并用 par 组合子并行递增两个引用；程序在 Pulse 表层的证明对应 PulseCore 中的正确性证明。内容覆盖引用、存在量化、用户谓词、循环、数组、链表、自旋锁、原子操作、并行递增及 C/Rust 代码提取，适合想深入验证型并发编程的开发者。

收藏14 天前

智能体驱动的形式化证明编程

AI 智能体已能自动形式化验证大型算法教材和 TLS-1.3 协议，F 和 Pulse 语言上生成超过 10 万行证明代码。Claude Opus 4.5、GPT-5.2 等模型结合 Claude Code、GitHub Copilot CLI 等智能体环境，使形式化证明从实验室走向工程实践。文章来自 F 语言教程，提供人机协作形式化编程的原则与方法，核心观点是：智能体生成的代码规模远超人类审查能力，必须设计好抽象层才能让证明有意义。

收藏48 天前