Texonom
Texonom
/
Engineering
Engineering
/Service Engineering/Service Management/Service Management Step/Service Planning/System Architecture/
Systems Correctness
Search

Systems Correctness

Creator
Creator
Seonglae Cho
Created
Created
2025 Jun 2 15:2
Editor
Editor
Seonglae Cho
Edited
Edited
2025 Jun 2 15:4
Refs
Refs
Mathematically prove or verify the formal correctness of systems and code
  • Distributed system design, security boundaries, protocol stability, data integrity
  • TLA+ (specification and model checking), P (state machine modeling), Dafny (static verification), Kani (Rust verification)
Systems Correctness Tools
TLA+
P Language
Dafny
HOL Light
Kani
 
 
 
 
Systems Correctness Practices at Amazon Web Services
Amazon Web Services (AWS) strives to deliver reliable services that customers can trust completely. This requires maintaining the highest standards of security, durability, integrity, and availability—with systems correctness serving as the cornerstone for achieving these priorities. An April 2015 article published in Communications of the ACM, titled “How Amazon Web Services Uses Formal Methods,” highlighted the approach for ensuring the correctness of critical services that have since become among the most widely used by AWS customers.21
Systems Correctness Practices at Amazon Web Services
https://cacm.acm.org/practice/systems-correctness-practices-at-amazon-web-services/
Systems Correctness Practices at Amazon Web Services
 
 

Recommendations

Texonom
Texonom
/
Engineering
Engineering
/Service Engineering/Service Management/Service Management Step/Service Planning/System Architecture/
Systems Correctness
Copyright Seonglae Cho