Comments (2)
wilcoxjay
commented on June 18, 2024
1
Hi,
Thanks for your interest!
We have some sources of high-level documentation linked from the website. I'd start by reading the blog posts, and then the PLDI '15 paper. If you want to know more about our verification of the Raft consensus protocol, then check out the CPP '16 paper as well.
We're also happy to answer specific questions you might have. You can file further issues here, send an email to [email protected], or chat with us in #uwverdi on freenode.
Unfortunately, the code itself is not particularly well documented. I'd be happy to add documentation to specific parts in response to your questions, or merge PRs that add documentation. (Perhaps that's wishful thinking on my part
from verdi.
langston-barrett
commented on June 18, 2024
@wilcoxjay Thanks, I think I figured out what I needed from the blog post!
from verdi.
Related Issues (20)
- Modelling multithreaded applications HOT 2
- Proposal: verify Verdi handlers down to machine code for example system
- Proposal: verify Verdi shim functions down to machine code
- Proposal: connect Verdi with verified crash-safe filesystem
- Please do not depend on autogenerated names of `destruct` that are sensitive to the file in which records are defined HOT 2
- What version of coq-verdi does one need for coq 8.10
- What commit works for verdi with coq 8.12? HOT 2
- Transfer-based correctness theorem for Raft is missing HOT 1
- Do not pun Inp/Out in trace_mutual exclusion
- Make extraction work without building all the raft proofs HOT 1
- Small typo in README.md HOT 1
- Print better error message when trying to build on 8.4
- Server crashes when trying to produce large packets because of buffer overflow HOT 1
- Server is unable to recover when disk log is incomplete due to a crash while writing an entry HOT 1
- Crash during update of snapshot causes loss of data HOT 1
- Transient system call errors during recovery cause inconsistent re-initialization HOT 1
- Server assumes that it can read the entire client request with a single recv call HOT 1
- Client-server marshaling allows users to inject commands and to crash the server HOT 1
- proof-sizes.awk missing "Proposition" HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from verdi.