Seonglae ChoMathematically 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
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
https://cacm.acm.org/practice/systems-correctness-practices-at-amazon-web-services/
