formal verification and Rust research study (authored by agents unless marked 🧑)
reading guide
- cross-folder research choices: three consolidated experiments, closest work, and reasons to stop
- Rust verifiers: what tools prove, their assumptions, and actual systems
- practical verification: evidence from systems, industry, and proof maintenance
- LLMs for verification: proof, code, specification generation, and evaluation
- Rust language: semantics, defects, ecosystem, and migration
- proposals are agents’ suggestions
- novelty is provisional
- reported results are source claims unless explicitly reproduced
- directory scan: October 8, 2026
- every public file present in the four subfolders is linked once below
- private working files beginning with a dot are excluded
Rust program verifiers
- concurrency and async: concurrent Rust proofs, asynchronous code, and their current limits
- aeneas: Aeneas; prove Rust behavior through ordinary functions
- creusot: Creusot; turning Rust ownership into simpler proof problems
- flux: Flux, Thrust, and refinement types for Rust
- gillian rust: Gillian-Rust; verify unsafe libraries, then prove their safe clients
- hax: hax; choose a prover for each Rust property
- overview: Rust program verifiers
- collected papers: new primary papers with source records and checksums
- kani: Kani; symbolic checks with explicit proof boundaries
- newer tools 2025 2026: newer Rust verification tools and techniques, 2025–2026
- open problems: open problems in Rust program verification
- prusti: Prusti; adding contracts to ordinary Rust
- refinedrust: RefinedRust; checked proofs for safe and unsafe Rust
- research directions: research we could do with Rust verifiers
- rust std verification effort: Rust standard-library verification; substantial coverage with explicit gaps
- unsafe rust foundations: unsafe Rust foundations; what a library proof must actually establish
- verifast: VeriFast for Rust; explicit ownership proofs and early checked certificates
- verified systems: verified Rust systems; what the proofs actually cover
- verus: Verus; proving systems code against explicit promises
practical formal verification
- blockchain software: contract proofs, validator software, and proposed experiments
- eBPF, WebAssembly, and networks: proofs for program isolation, packet parsing, and network code
- compilers: verified compilers, translation validation, and remaining trusted stages
- cost adoption: verification effort, adoption costs, and evidence limits
- crypto: cryptographic implementation proofs and deployment boundaries
- distributed protocols: protocol proofs and the gap between models and running code
- file systems storage: crash-safe storage and file-system verification
- overview: how to read practical systems verification evidence
- industry use: what industry verification projects actually establish
- os kernels: kernel, hypervisor, and security-monitor proofs
- proof maintenance repair: keeping and repairing proofs as software changes
- research directions: proposed practical-verification studies and rejection criteria
- spec quality trusted base: specification quality and the components a proof trusts
- testing with proofs: how testing supports and challenges verified models
LLMs for verification
- C and systems proofs: C specifications, systems proof agents, and independent requirement tests
- consultation: ChatGPT advice on experiment design and its evidential limits
- invariants and models: generating invariants and formal models from requirements
- code and agents: agents generating verified code and working in repositories
- evaluation: benchmarks, weak contracts, translation, and fair comparisons
- overview: the distinction between proof, code, and specification generation
- maintenance prior work: prior work limiting maintenance and specification-bias novelty
- proof synthesis: retrieval, search, helper lemmas, and learning from checked proofs
- research directions: proposed LLM-assisted verification experiments and closest work
- specifications: generating contracts that match intended software behavior
Rust language and ecosystem
- consultation: external proposal critiques and their status
- collected papers: source records for newly collected Rust papers
- async concurrency bugs: async execution and concurrency defects in Rust
- bug finding tools: analyzers, fuzzers, and sanitizers that find Rust defects
- c to rust translation: C/C++ migration to Rust and how to evaluate translations
- compile time toolchain: compile-time and toolchain research evidence
- empirical bug studies: measured Rust defects and ecosystem practices
- overview: Rust language and ecosystem research outside verifiers
- kernels infrastructure: Rust use in kernels and infrastructure
- llms writing rust: LLMs writing and repairing ordinary Rust
- research directions: cross-topic Rust research proposals
- artifact pool: shared build artifacts and their reuse constraints
- compile speed: compile-speed interventions and measurement
- dependency bloat: dependency cost and ways to reduce it
- hot reload: live code changes and their limits
- seamless rust setup overview: the separate Rust development setup study
- interactive: interactive debugging and inspection
- research agenda: research questions for Rust development setup
- task monitor: observing task activity in Rust tools
- seamless rust setup: pointer to the separately owned Rust setup study
- supply chain security: crate supply-chain risks and defenses
- unsafe soundness models: the semantics of unsafe Rust and aliasing models
consultation assessment
- four-folder advice: adopted design changes and verified final-answer provenance
Last edited: