File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change 4040 - [ Executable libraries: Vec] ( exec_lib.md )
4141- [ Spec closures] ( spec_closures.md )
4242
43- # Tutorial: Best Practices
43+ # Tutorial: Proofs and Proof Development
4444
4545- [ Developing proofs] ( develop_proofs.md )
4646 - [ Using assert and assume] ( assert_assume.md )
4747 - [ Devising loop invariants] ( invariants.md )
4848 - [ Proving absence of overflow] ( overflow.md )
49- - [ Using LLM assistants] ( llms.md )
50- - [ Using LLMs to develop proofs] ( llmforverusproof.md )
51- - [ Using LLMs to develop specifications] ( )
5249- [ Quantifiers] ( quants.md )
5350 - [ forall and triggers] ( forall.md )
5451 - [ Multiple variables, multiple triggers, matching loops] ( multitriggers.md )
7370 - [ Proof by computation] ( assert_by_compute.md )
7471 - [ Spinning off separate SMT queries] ( )
7572 - [ Breaking proofs into smaller pieces] ( breaking_proofs_into_pieces.md )
73+ - [ Using LLM assistants] ( llms.md )
74+ - [ Using LLMs to develop proofs] ( llmforverusproof.md )
75+ - [ Using LLMs to develop specifications] ( )
7676- [ Checklist: what to do when proofs go wrong] ( checklist.md )
7777
7878# Tutorial: Verification and Rust
You can’t perform that action at this time.
0 commit comments