ITPE * JackerLab

개요Event-B는 정형 기법(Formal Method)을 활용한 시스템 모델링 및 검증 프레임워크로, 복잡한 시스템의 정확성과 일관성을 수학적으로 보장할 수 있도록 설계된 언어 및 개발 방법론입니다. 주로 임베디드 시스템, 안전 필수 시스템, 프로토콜 설계 등 고신뢰성이 요구되는 분야에서 활용되며, 추상화(abstraction)와 정제(refinement)를 핵심 개발 흐름으로 사용합니다.1. 개념 및 정의Event-B는 Jean-Raymond Abrial이 개발한 정형 기법 언어로, **상태 기반 모델링(State-Based Modeling)**을 통해 시스템 동작을 정의합니다.B-Method의 확장: Event 중심의 상태 전이 모델링정형 명세(Formal Specification) + 수학적 증명..

개요탈중앙화 금융(DeFi)은 코드로 구현된 스마트 계약을 통해 자산 교환, 대출, 파생상품 등 복잡한 금융 로직을 자동 실행합니다. 하지만 코드 오류나 취약점은 수백억 원에 달하는 피해로 이어질 수 있습니다. 이를 해결하기 위한 핵심 기법이 바로 **Formal Verification(형식 검증)**입니다. 이는 스마트 계약을 수학적 모델로 추상화하고, 사전에 정의된 보안·기능 요구사항을 논리적으로 증명하는 과정으로, DeFi 생태계의 신뢰성과 안전성을 높이는 데 필수적인 기술입니다.1. 개념 및 정의Formal Verification은 소프트웨어나 스마트 계약의 동작을 수학적으로 모델링하고, 논리 기반의 자동화된 증명 도구를 사용해 오류 가능성을 완전히 제거하는 검증 기법입니다. 스마트 계약의 로직을..