|
|
|
|
|
|
by eddsh1994
1262 days ago
|
|
|
This is pretty common in the Blockchain space to verify transactions behave correctly when arriving out of sync with tools like Agda, Coq, etc... I assume it's the same on databases & I heard Leslie Lamport give a talk at work where he mentioned AWS used TLA+ to prove some of its properties. |
|
|