All posts
hacl-pulse: Re-verifying HACL* in Pulse, with Agents
A from-scratch reimplementation of the HACL* verified crypto library in F* and Pulse, built with AI agents in six weeks, at feature parity and close to HACL*'s performance.
A Verified Generational GC for OCaml
Software development with agents & proofs
DeepTest: Systematic Testing Grounded in Specification Knowledge Bases
Early results from DeepTest, a framework for specification-driven testing and bug discovery backed by symbolic tools, deployed across thousands of Microsoft components and open-source projects.
Spotting Specification Gaps with Small Proof-Oriented Tests
Using small proof-oriented tests to identify gaps in specifications
Formalizing Data Structures and Algorithms with Agents
Agents formalize imperative algorithms from natural language
Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents
The key challenge for reliable AI-generated code is intent formalization—automatically turning vague human intent into precise, checkable specifications.
How to train your program verifier
Development of a symbolic program analysis engine from prompts to functioning system
Agentic Proof-Oriented Programming
Exploring AI-assisted proof-oriented programming with Copilot CLI and F*.