Aeneas translates Rust programs to pure Lean code for formal verification.
All detailed instructions for AI agents live in documentation/skills/. These are
the source of truth — they are symlinked to .github/instructions/ (for GitHub
Copilot) and .claude/skills/ (for Claude Code). Always edit files in
documentation/skills/; changes propagate automatically through the symlinks.
| Skill file | Covers |
|---|---|
aeneas-compiler-dev |
Dev workflow, formatting, tests, error macros, skill file structure, build rules |
aeneas-lean-core |
Translation model, spec patterns, tactic reference, pitfalls |
aeneas-tactics-quickref |
Tactic decision tree, banned tactics, combinations |
lean-lsp-mcp |
lean-lsp-mcp MCP tools for interactive proof development |
launching-proof-agents |
Multi-agent proof orchestration, review gates |
verification-campaigns |
Planning and executing large verification campaigns |
proof-patterns |
Worked proof examples (loops, dot products, comparisons) |
aeneas-crypto-verification |
Crypto-specific proof strategies (Montgomery, NTT, etc.) |
documentation/getting-started.md— Start here: Rust → LLBC → Lean → first proofdocumentation/aeneas-overview.md— How Aeneas works, translation model, workflowdocumentation/proof-strategies.md— Proof strategies (step, loops, decomposition, specs)documentation/tactics-reference.md— All tactics with docstrings and examplesdocumentation/crypto-verification.md— Crypto verification guide (ML-KEM/Kyber patterns)documentation/tips-and-tricks.md— Pitfalls, tips, and tricksdocumentation/glossary.md— Glossary of Aeneas-specific terms