보안 업체들은 에이전트 코드 검토를 넘어 AI를 점점 더 활용해 보안 감사를 강화하고, 실제 코드 검사 전에 맞춤형 도구와 공식 모델을 구축합니다. 예를 들어, 개발자 도구가 부족한 Miden VM을 검토할 때, 에이전트들은 6개월간 LSP 서버, 디컴파일러, 정적 분석 엔진, VM 실행기의 린 모델을 만들었습니다. 이 도구들은 Falcon 서명 위조와 자금 도난을 가능하게 할 수 있는 검증되지 않은 검증 제공자 입력과 같은 심각한 보안 취약점을 식별했습니다. Lean 모델은 또한 Miden 핵심 라이브러리의 상당 부분에 대해 95개의 기계 검사 정확성 증명을 생성했습니다. 자체 어셈블리 언어(MASM)를 가진 새로운 제로지식 VM인 Miden VM은 스택 머신 아키텍처와 개발자 도구 부재로 인해 독특한 검토 과제를 안겨주었습니다. 이를 해결하기 위해 팀은 문법 강조, 코드 탐색, 명령어 문서화를 위한 LSP 서버와 VS Code 확장 등 필수 도구 구축을 우선시했습니다. 다음으로, 암묵적 스택 연산과 선언되지 않은 서명 같은 복잡성에도 불구하고 고수준 의미 정보를 제공하는 MASM 프로시저용 디컴파일러가 개발되었습니다. 이 디컴파일러는 수개월에 걸친 노력으로 귀중한 내부 분석 프레임워크와 정적 분석을 위한 중간 표현을 제공했습니다. 이 중간 표현을 활용해 팀은 정적 분석을 위한 추상 해석 엔진을 구축했으며, 검증자가 제공한 값을 검증하고, 타입 제약을 강제하며, 로컬 변수 초기화를 보장하는 패스를 구현했습니다. 이로 인해 400개 이상의 잠재적 타입 검증 개선과 mod_12289 절차에서 언제약 조언 값이라는 고강도 버그가 발견되었습니다. 이 취약점은 악의적인 증명자가 나머지 값을 조작하여 팔콘 서명을 위조하고 미덴 계정을 소모할 수 있게 했습니다. 버그 발견을 넘어, 에이전트들은 Lean을 이용한 형식 검증, Miden VM 실행기 모델링, MASM 절차를 자동으로 Lean으로 변환하는 등 다양한 방식을 탐구했습니다. 이 에이전트 기반 형식 모델링은 이진 산술 구성 요소에 대해 95개의 정확성 증명을 가능하게 했으며, 기존 단위 테스트에서 놓친 두 가지 미묘한 버그, 즉 64비트 우회전(rotr)의 예외 사례와 256비트 곱셈(wrapping_mul)의 문제를 발견했습니다. 이러한 첨단 도구 및 형식적 모델링 노력은 최근 AI 에이전트의 발전으로 가능해졌으며, 시간과 자원 제약으로 이전에는 달성할 수 없었던 보안 검토의 깊이와 품질을 크게 향상시켰습니다.