태그로 보기

정형 검증

글 2편

Cedar는 누가 접근할 수 있는지를 증명합니다. 어떤 결정이 내려질지는 누가 증명하나요?

Cedar는 Lean과 automated reasoning으로 권한 정책에 formal verification을 붙였습니다. 같은 일을 비즈니스 결정에 해낸 상용 룰 엔진은 아직 없습니다. 가격과 자격 판정과 사기 규칙을 증명하는 쪽이 왜 더 어려운 문제인지, 그리고 LexQ가 지금 어디에 서 있는지 적습니다.

2026년 8월 7일10분 읽기

비즈니스 결정에 형식 검증이 필요한 이유

테스트와 시뮬레이션은 이미 받아본 입력만 놓고 답합니다. 아직 아무도 보내지 않은 입력은 답의 범위 밖입니다. 도달 불가능한 규칙, 조용한 충돌, 아무 규칙도 덮지 않는 공백이 그 차이 안에 있습니다. 이 차이는 표본이 아니라 증명으로만 메워집니다.

2026년 8월 7일11분 읽기