Skip to article frontmatter Skip to article content

prealpha; Formal Verification Agent Recipes

Introduction

Dafny part 1: with a framework

Dafny part 2: no framework

Lean

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

RL

Outlook

Using lean-lsp-mcp

The agent/solver

Reinforcement Learning