rainoftimerainoftime/pl-skills/dafny-verifier/SKILL.md

dafny-verifier

Skill17 starsChanged 9 months agoApache-2.0View on GitHub

Use Dafny verification language for constructing verified programs with proofs.

In this repository98 other files it gives its agents.
- abstract-interpretation-engineSkill
- abstract-machineSkill
- acsl-annotation-assistantSkill
- actor-model-implementerSkill
- algebraic-effectsSkill
- alias-and-points-to-analysisSkill
- axiomatic-semanticsSkill
- bidirectional-type-checkingSkill
- bisimulation-checkerSkill
- capability-systemSkill
- closure-converterSkill
- common-subexpression-eliminatorSkill
- concurrency-verifierSkill
- constant-propagation-passSkill
- contextual-equivalenceSkill
- control-flow-analysisSkill
- coq-proof-assistantSkill
- cps-transformerSkill
- dataflow-analysis-frameworkSkill
- dead-code-eliminatorSkill
- defunctionalizationSkill
- denotational-semantics-builderSkill
- dependent-type-implementerSkill
- dsl-embeddingSkill
- effect-handlers-implementerSkill
- effect-systemSkill
- effect-type-systemSkill
- escape-analysisSkill
- existential-typesSkill
- ffi-designerSkill
- fuzzer-generatorSkill
- gadt-implementerSkill
- garbage-collector-implementerSkill
- graalvm-truffle-implementerSkill
- gradual-typing-implementerSkill
- higher-order-abstract-syntaxSkill
- hoare-logic-verifierSkill
- incremental-computationSkill
- information-flow-analyzerSkill
- inline-expanderSkill
- interprocedural-analysisSkill
- invariant-generatorSkill
- jit-compiler-builderSkill
- lambda-calculus-interpreterSkill
- language-server-protocolSkill
- lean-proverSkill
- lexer-generatorSkill
- linear-type-implementerSkill
- liveness-analysisSkill
- llvm-backend-generatorSkill
- lock-free-data-structureSkill
- loop-optimizerSkill
- loop-termination-proverSkill
- macro-expanderSkill
- memory-allocatorSkill
- message-passing-systemSkill
- mlir-dialect-designerSkill
- model-checkerSkill
- module-systemSkill
- monad-transformerSkill
- The first 60 shown.

The file

We split this skill into the rules it gives an agent

8 rules. About 0 are common, 7 are distinctive, and 1 is very specific to this project.

≈0
Common · estimate
Many files like this have a rule of this kind.
≈7
Distinctive · estimate
This author's own choices. Worth a look.
1
Very specific
Tied to their project's names, files or tools. Probably skip.

Common
Distinctive
Very specific

Distinctive:
Lemma Proving: Write and prove helper lemmas
line 27
Distinctive:
Start with strong specifications, weaken if needed
line 44
Distinctive:
Use lemmas to break complex proofs
line 45
Distinctive:
Write loop invariants before the body
line 46
Very specific:
Use calc statements for calculation proofs
line 47
Distinctive:
When proofs are not needed
line 85
Distinctive:
When performance is critical
line 87
Distinctive:
Not as expressive as Coq
line 93

≈ “Common” is an estimate: at least 1 in 5 of the 350,495 skill files we read have a rule of the same kind, not the same words. “Very specific” is our guess from the words: it names a file, a command, a setting or the project itself.

Keep what fits and drop the rest. Your version, ready for your agents.

Files

SKILL.md

Dafny Verifier

Dafny is a verification-aware programming language that supports writing specifications, programs, and proofs together. It compiles to verified code in multiple languages (C#, Java, Go, JavaScript).

When to Use This Skill

Writing verified programs
Learning formal verification
Proving algorithm correctness
Teaching program proofs
Developing certified software

What This Skill Does

Specification Writing: Define pre/post conditions and invariants
Verification: Automatically verify programs against specs
Lemma Proving: Write and prove helper lemmas
Termination: Prove program termination
Code Extraction: Generate verified code

Key Concepts

Concept	Description
Method	Executable code with specifications
Function	Mathematical function (pure, no side effects)
Lemma	Proof that can be called like a function
Invariant	Property that holds at loop header
Ensures	Postcondition specification
Requires	Precondition specification

Tips

Start with strong specifications, weaken if needed
Use lemmas to break complex proofs
Write loop invariants before the body
Use calc statements for calculation proofs
The old() function refers to pre-state

Common Use Cases

Verified algorithms
Certified libraries
Teaching formal methods
Security-critical code
Protocol verification

Related Skills

hoare-logic-verifier - Theory behind Dafny
coq-proof-assistant - More expressive proof assistant
smt-solver-interface - Z3 powers Dafny
separation-logician - For heap reasoning

Canonical References

Reference	Why It Matters
Leino, "Dafny: An Automatic Program Verifier for Functional Correctness" (LPAR 2010)	Original Dafny paper
Leino, "Program Proofs" (MIT Press, 2023)	Comprehensive Dafny book
Dafny documentation (dafny.org)	Official reference

Tradeoffs and Limitations

Approach Tradeoffs

Approach	Pros	Cons
Dafny	Automatic, usable	Limited expressiveness
Coq	Very expressive	Manual proofs
F*	More features	Steeper learning

When NOT to Use This Skill

When proofs are not needed
For low-level systems code (use Verus)
When performance is critical

Limitations

Heap reasoning can be tricky
Some proofs need explicit lemmas
Not as expressive as Coq

Assessment Criteria

A high-quality implementation should have:

Criterion	What to Look For
Verification	All proofs check
Readability	Clear specifications
Modularity	Good lemma structure
Termination	All loops/functions terminate

Quality Indicators

✅ Good: All specs verified, clear invariants, modular lemmas ⚠️ Warning: Some specs need manual hints ❌ Bad: Unverified code, missing invariants

Research Tools & Artifacts

Verification tools:

Tool	Language	What to Learn
Verus	Rust	Verified Rust
F*	F*	Verification

Research Frontiers

1. Automation

Goal: More automatic proofs

Implementation Pitfalls

Pitfall	Real Consequence	Solution
Failed proofs	Verification fails	Add lemmas

Download now (ZIP)

Does it work?

Reviews from people and from AI agents that ran it: what they used it for, and whether it worked.

Reviews can't be read right now.

Your trail

Files you open will collect here, so you can find them again.

Open two or more, and you can remix the rules you like from each into one list. Kept in this browser only.

Now do this for your own.

Bring your CLAUDE.md, AGENTS.md or skills. agentleFS shows which of your rules are common, which are yours and which only fit one project, and keeps one version your agents read everywhere.

Check your setup, free