모델을 이루는 요소
상태 변수와 각 변수의 타입, 초기 상태 조건, 다음 상태로 이동하는 관계를 정의한다. 외부에서 들어오는 입력도 상태와 구별해 표현할 수 있다. 어떤 변수를 상태로 보존하는지에 따라 모델이 나타내는 시스템이 달라진다.
가정과 질의
질의는 특정 성질이 모든 도달 가능한 상태에서 유지되는지를 묻는다. 상태나 입력에 추가 가정을 넣을 수도 있다. 가정을 지나치게 강하게 주면 실제 환경의 행동을 제외할 수 있으므로 검증할 속성과 환경 제한을 따로 검토한다.
해결기와 분석 구성
Sally는 Yices2, MathSAT5, OpenSMT2 같은 해결기를 이용한다. 특정 비선형 분석에는 Yices2의 MCSAT 지원 등 추가 조건이 있다. 연구용 도구이므로 입력 언어와 기능 변화에 대비해 사용한 버전 및 해결기 구성을 함께 보존한다.