---
title: 形式化仕様 ↔ 実装 co-design —— Quint × Malachite パラダイム
aliases: [formal-implementation co-design, Quint Malachite codesign, TLA+ MBT codesign, spec-impl convergent design]
domain: systems
kind: knowledge
topic: formal-spec-implementation-codesign
created: 2026-05-16
last_updated: 2026-05-26
last_tended: 2026-06-24
review_by: 2026-09-22
confidence: certain
tags: [systems, formal-methods, consensus, tla, quint, malachite, bft]
status: active
sources:
  - https://github.com/informalsystems/quint
  - https://github.com/informalsystems/malachite
---

# 形式化仕様 ↔ 実装 co-design


## Wiki route

This entry sits under [[systems/INDEX|systems index]]. Read it against [[systems/threshold-bft-consensus-rust-implementations|Threshold BFT コンセンサス Rust 化トレンド（Tempo Simplex / Arc Malachite）]] for peer / contrast context and [[fintech/INDEX|fintech index]] for the broader system / regulatory boundary.

## Related
<!-- wiki-links:managed -->
- [[INDEX|Wiki Index]]
- [[systems/threshold-bft-consensus-rust-implementations|Threshold BFT Rust 実装]]
- [[systems/dag-bft-vs-chain-bft-architecture|DAG vs Chain BFT]]
- [[systems/post-quantum-blockchain-day1-integration|耐量子 day-1 統合]]
<!-- /wiki-links:managed -->

## Sources

- Quint — TLA ベースの実行可能仕様言語（model-based testing / co-design）— https://github.com/informalsystems/quint
- Malachite — Flexible BFT consensus engine in Rust（仕様 ↔ 実装 co-design の対象）— https://github.com/informalsystems/malachite