거버넌스 제안 상세
제안서 상세 내용과 투표 현황을 확인하세요.
한글 버전
- 첫 번째 작업은 IO의 오픈 소스 자동 형식 검증 도구인 Blaster를 단일 스크립트에서 DApp 수준의 전체 검증으로 확장하는 것임 .
- Blaster는 Aiken, Pebble, Scalus, Futura 언어와 통합되어 개발 도구 체인에서 직접 검증을 수행할 수 있도록 지원함 .
- 시각적 반례 탐색을 지원하는 VS Code 확장 프로그램과 보안 템플릿을 포함한 공통 취약점 라이브러리, UPLC 최적화를 위한 등가성 확인 도구를 제공함 .
- 두 번째 작업은 고신뢰 도구 모음을 단일 명령으로 설정할 수 있는 CBDE를 구축하여 환경 설정 시간을 단축함 .
- DeFi 사용자는 수학적으로 검증된 DApp을 사용하게 되며, 개발자는 실용적인 고신뢰 엔지니어링 기반을 갖추게 됨 .
- IO, Lantr, Harmonic Labs, SAIB, Midgard Labs, TxPipe, No.Witness Labs가 협력하여 개발 및 유지보수를 분담함 .
- Intersect가 마일스톤에 따라 자금을 집행하며, 총 예산 요청액은 ₳13.08M임 .
- 3. Glossary (주석): ■ 주석 *Formal Verification: 프로그램의 정확성을 수학적으로 증명하는 기술 **Blaster: IO에서 개발한 오픈 소스 자동 형식 검증 도구 ***DApp: 탈중앙화 애플리케이션 ****UPLC: 에이다 스마트 계약의 하위 수준 실행 언어 *****CBDE: 컨테이너 기반 개발 환경 ******DeFi: 탈중앙화 금융
- 현재 개발자는 계약 코드 작성 전 환경 설정에 많은 시간을 소비하며, 이는 협업 시 일관성 없는 결과로 이어질 수 있음 .
- 형식 검증 도구인 Blaster는 현재 내부 전문가 위주로 사용되나, 이를 전체 생태계로 확장할 필요가 있음 .
- 첫 번째 작업은 Blaster를 공개 도구로 전환하여 전체 DApp 수준의 검증과 4개의 신규 언어를 지원하는 것임 .
- 여기에는 VS Code 확장 프로그램, 취약점 라이브러리, UPLC 프로그램 간의 의미적 동일성을 증명하는 도구가 포함됨 .
- 두 번째 작업은 Plinth 툴체인이 포함된 컨테이너 기반 개발 환경(CBDE)을 구축하여 단일 명령으로 설정을 완료하는 것임 .
- Blaster는 모든 언어의 공통 컴파일 대상인 UPLC에서 작동하므로 생태계 전반에 걸친 투자의 효율성이 높음 .
- Lantr, Harmonic Labs, SAIB 등 여러 파트너와의 협업을 통해 도구의 개발과 장기적인 유지보수를 수행함 .
- ■ 주석 *Formal Verification: 수학적 명세를 통해 소프트웨어의 오류 없음을 증명하는 방법임 **Nix: 재현 가능한 빌드 환경을 구축하기 위한 패키지 관리 도구임 ***DApp: 블록체인 기반의 탈중앙화 애플리케이션임 ****UPLC: 에이다 스마트 계약의 최종 실행 형태인 Untyped Plutus Core임 *****CLI: 명령어를 직접 입력하여 프로그램을 제어하는 인터페이스임 ******Plinth: 에이다 스마트 계약 개발 및 검증을 지원하는 통합 프레임워크임
- 자동화된 형식 검증 도구와 보안 속성 라이브러리를 통해 모든 DApp이 높은 수준의 보증을 달성하게 했음 .
- CBDE는 복잡한 Nix 설정을 60초 초기화로 단축하여 개발자 진입 장벽을 낮췄음 .
- 이 제안은 TVL 증가, 월간 트랜잭션 확대, 활성 사용자 수(MAU) 성장을 목표로 했음 .
- Blaster 도구는 Lean4 기반의 자동 형식 검증 백엔드로 연구 우수성에 기여했음 .
- 2026년 3분기부터 2027년 2분기까지 단계별 로드맵을 통해 도구와 프레임워크를 출시했음 .
- 총 예산은 ₳13.07M이며, Blaster와 CBDE 두 가지 작업 스트림으로 나뉨 .
- Intersect와 법적 계약을 체결하고 스마트 계약 기반의 투명한 자금 관리를 수행했음 .
- ■ 주석 *DeFi: 탈중앙화 금융 **DApp: 탈중앙화 애플리케이션 ***Formal Verification: 형식 검증 (수학적 증명을 통한 소프트웨어 검증) ****UPLC: Untyped Plutus Core (에이다 스마트 계약 실행 언어) *****TVL: 총 예치 자산 ******MAU: 월간 활성 사용자 수 *******Nix: 패키지 관리 및 빌드 시스템 ********CBDE: Cardano Blockchain Development Environment (에이다 블록체인 개발 환경) *********TRSC: Treasury Reserve Smart Contract (재무 예비비 스마트 계약) **********PSSC: Project-Specific Smart Contract (프로젝트 전용 스마트 계약)
English
부가 정보
| 트랜잭션 해시 | 73e171a4c0730b4b59ecae271ab89f12a9d56360b02920e1f95107dbdc1d6762 |
|---|---|
| 블록 타임 | 1776863461 |
| Proposal ID | gov_action1w0shrfxqwv95kk0v4cn34wylz25a2cmqkq5jpc0e2yrahhqava3q2yd5rxu |
| Proposal Index | 5 |
IO: 카르다노 고신뢰 기술 협업에 대한 제안
현재 어디까지 왔나
📊 제안서 투표현황
DRep 투표현황
SPO 투표현황
헌법위원회 투표현황
📝 상세 설명
🇰🇷 한글 버전
- 첫 번째 작업은 IO의 오픈 소스 자동 형식 검증 도구인 Blaster를 단일 스크립트에서 DApp 수준의 전체 검증으로 확장하는 것임 .
- Blaster는 Aiken, Pebble, Scalus, Futura 언어와 통합되어 개발 도구 체인에서 직접 검증을 수행할 수 있도록 지원함 .
- 시각적 반례 탐색을 지원하는 VS Code 확장 프로그램과 보안 템플릿을 포함한 공통 취약점 라이브러리, UPLC 최적화를 위한 등가성 확인 도구를 제공함 .
- 두 번째 작업은 고신뢰 도구 모음을 단일 명령으로 설정할 수 있는 CBDE를 구축하여 환경 설정 시간을 단축함 .
- DeFi 사용자는 수학적으로 검증된 DApp을 사용하게 되며, 개발자는 실용적인 고신뢰 엔지니어링 기반을 갖추게 됨 .
- IO, Lantr, Harmonic Labs, SAIB, Midgard Labs, TxPipe, No.Witness Labs가 협력하여 개발 및 유지보수를 분담함 .
- Intersect가 마일스톤에 따라 자금을 집행하며, 총 예산 요청액은 ₳13.08M임 .
- 3. Glossary (주석): ■ 주석 *Formal Verification: 프로그램의 정확성을 수학적으로 증명하는 기술 **Blaster: IO에서 개발한 오픈 소스 자동 형식 검증 도구 ***DApp: 탈중앙화 애플리케이션 ****UPLC: 에이다 스마트 계약의 하위 수준 실행 언어 *****CBDE: 컨테이너 기반 개발 환경 ******DeFi: 탈중앙화 금융
- 현재 개발자는 계약 코드 작성 전 환경 설정에 많은 시간을 소비하며, 이는 협업 시 일관성 없는 결과로 이어질 수 있음 .
- 형식 검증 도구인 Blaster는 현재 내부 전문가 위주로 사용되나, 이를 전체 생태계로 확장할 필요가 있음 .
- 첫 번째 작업은 Blaster를 공개 도구로 전환하여 전체 DApp 수준의 검증과 4개의 신규 언어를 지원하는 것임 .
- 여기에는 VS Code 확장 프로그램, 취약점 라이브러리, UPLC 프로그램 간의 의미적 동일성을 증명하는 도구가 포함됨 .
- 두 번째 작업은 Plinth 툴체인이 포함된 컨테이너 기반 개발 환경(CBDE)을 구축하여 단일 명령으로 설정을 완료하는 것임 .
- Blaster는 모든 언어의 공통 컴파일 대상인 UPLC에서 작동하므로 생태계 전반에 걸친 투자의 효율성이 높음 .
- Lantr, Harmonic Labs, SAIB 등 여러 파트너와의 협업을 통해 도구의 개발과 장기적인 유지보수를 수행함 .
- ■ 주석 *Formal Verification: 수학적 명세를 통해 소프트웨어의 오류 없음을 증명하는 방법임 **Nix: 재현 가능한 빌드 환경을 구축하기 위한 패키지 관리 도구임 ***DApp: 블록체인 기반의 탈중앙화 애플리케이션임 ****UPLC: 에이다 스마트 계약의 최종 실행 형태인 Untyped Plutus Core임 *****CLI: 명령어를 직접 입력하여 프로그램을 제어하는 인터페이스임 ******Plinth: 에이다 스마트 계약 개발 및 검증을 지원하는 통합 프레임워크임
- 자동화된 형식 검증 도구와 보안 속성 라이브러리를 통해 모든 DApp이 높은 수준의 보증을 달성하게 했음 .
- CBDE는 복잡한 Nix 설정을 60초 초기화로 단축하여 개발자 진입 장벽을 낮췄음 .
- 이 제안은 TVL 증가, 월간 트랜잭션 확대, 활성 사용자 수(MAU) 성장을 목표로 했음 .
- Blaster 도구는 Lean4 기반의 자동 형식 검증 백엔드로 연구 우수성에 기여했음 .
- 2026년 3분기부터 2027년 2분기까지 단계별 로드맵을 통해 도구와 프레임워크를 출시했음 .
- 총 예산은 ₳13.07M이며, Blaster와 CBDE 두 가지 작업 스트림으로 나뉨 .
- Intersect와 법적 계약을 체결하고 스마트 계약 기반의 투명한 자금 관리를 수행했음 .
- ■ 주석 *DeFi: 탈중앙화 금융 **DApp: 탈중앙화 애플리케이션 ***Formal Verification: 형식 검증 (수학적 증명을 통한 소프트웨어 검증) ****UPLC: Untyped Plutus Core (에이다 스마트 계약 실행 언어) *****TVL: 총 예치 자산 ******MAU: 월간 활성 사용자 수 *******Nix: 패키지 관리 및 빌드 시스템 ********CBDE: Cardano Blockchain Development Environment (에이다 블록체인 개발 환경) *********TRSC: Treasury Reserve Smart Contract (재무 예비비 스마트 계약) **********PSSC: Project-Specific Smart Contract (프로젝트 전용 스마트 계약)