Skip to article frontmatter Skip to article content

prealpha; Formal Verification Agent Recipes

Introduction

Dafny part 1: with a framework

Dafny part 2: plain Python

Lean

FVAPPS with pydantic-ai Lean FVAPPS Pydantic-AI The agent/solver Using lean-lsp-mcp

DalekGitBench

RL

Outlook

Using lean-lsp-mcp

The agent/solver

Mining Git History for Proof Repair