Apa yang Bisa dan Tidak Bisa Dicek TLA+: Catatan Hillel Wayne

Hillel Wayne menulis artikel berjudul "What TLA+ can and can't check" di buletin Computer Things pada 30 September 2026. Ia membuka tulisannya dengan ajakan yang cukup jelas: mari sedikit menahan diri terhadap narasi bahwa TLA+ akan menyelamatkan AI dari dirinya sendiri. Sebagai orang yang lama mengajar dan mengadvokasi TLA+, ia justru khawatir pada euforia yang muncul belakangan ini.

Pemicunya adalah pernyataan Boris Cherny, yang artikel itu sebut sebagai pencipta [CC]. Menurut Wayne, Cherny menyebut bahwa Opus mampu memakai TLA+ untuk menemukan race condition di dalam kode. Sejak itu, banyak orang di internet membicarakan formal verification seolah masalah pengembangan perangkat lunak berbasis agen akan selesai sekali dan untuk selamanya.

Wayne tidak menyangkal manfaat TLA+. Ia menyebut TLA+ memang bagus untuk merancang sistem konkuren yang kompleks dan memastikan bebas bug. Yang ia bantah adalah klaim bahwa metode formal akan menyelesaikan semua masalah. Menurutnya, sudah banyak tulisan tentang kelemahan TLA+ dalam hal apa yang bisa dijamin, misalnya bahwa desain yang benar tidak otomatis menghasilkan kode yang benar. Karena itu ia memilih fokus berbeda: properti apa yang bahkan tidak bisa dinyatakan oleh TLA+.

Dasar: State, Behavior, dan Tiga Operator Temporal

TLA+ membagi sistem menjadi sekumpulan behavior. Setiap behavior adalah urutan state, misalnya lampu satu hijau, lalu kuning, lalu merah. Di setiap state, kita bisa menyatakan ekspresi boolean biasa, seperti lampu empat hijau atau semua lampu merah.

Selain itu, ada tiga operator logika temporal yang bisa dipakai untuk memodifikasi ekspresi tersebut:

• []P atau "always P" bernilai benar bila P benar di state saat ini dan di setiap state berikutnya. Contohnya, [](at_most_one_green) benar bila di setiap state ke depan tidak pernah ada lebih dari satu lampu hijau.
• P' atau "P prime" bernilai benar bila P benar di state berikutnya. Contohnya, light sama dengan hijau dan light' sama dengan merah berarti lampu berubah dari hijau ke merah.
• <>P atau "eventually P" bernilai benar bila P benar di state saat ini atau di setidaknya satu state berikutnya.

Ketika kita menyebut P sebagai properti dari sistem, artinya P benar di state awal setiap behavior. Jadi memeriksa properti []P berarti []P benar di setiap state awal, dan karena definisi "always", P benar di setiap state berikutnya dari state awal itu. Ini yang disebut invariant, dan merupakan salah satu properti paling dasar yang diperiksa di TLA+.

Kita juga bisa menggabungkan [] dengan prime untuk mendapatkan action properties, misalnya [](x' >= x) yang benar bila nilai baru x selalu lebih besar atau sama dengan nilai lama. Contoh lain adalah [](P => P'), yang berarti begitu P benar, ia tidak akan pernah menjadi salah lagi.

Safety, Liveness, dan Refinement

Invariant dan action properties keduanya termasuk safety properties, yang secara kasar berarti sesuatu yang buruk tidak pernah terjadi. Di sisi lain ada liveness, yang berarti sesuatu yang baik selalu terjadi. Semua properti liveness dibangun dari operator <>.

<>P sendirian berarti P benar di setidaknya satu state dari setiap behavior. Menurut Wayne, ini biasanya terlalu lemah untuk jadi properti sistem yang berguna. Tetapi dengan komposisi, kita bisa membuat properti yang lebih menarik.

[]<>P benar bila di setiap state, P benar di setidaknya satu state berikutnya. Ini bisa merepresentasikan mekanisme pemulihan, misalnya bila node melakukan pemilihan pemimpin baru, mereka akan akhirnya menyepakati satu pemimpin. Sementara <>[]P benar bila pada suatu titik P menjadi benar dan tetap benar selamanya. Ini berguna untuk menunjukkan bahwa sebuah algoritma berhenti dengan hasil yang benar.

Ada juga [](P => <>Q), yang benar bila untuk setiap state di mana P benar, ada state berikutnya di mana Q benar. Ini bisa menunjukkan bahwa P akhirnya menyebabkan Q, atau bahwa semua pesan yang masuk ke antrean akhirnya ada di riwayat pembaca. Karena formulanya agak membingungkan saat dibaca, tersedia bentuk ringkasnya, yaitu P ~> Q, dibaca "P leads to Q".

Selain itu ada operator lain seperti ENABLED dan <<A>>_v yang membuka trik tambahan, tetapi Wayne menyebut mayoritas hal yang diperiksa adalah invariant, action properties, dan liveness. Ada juga refinement, yang merupakan kombinasi safety dan liveness, dan menurutnya topik tersendiri.

Yang Tidak Bisa Dilakukan TLA+

Wayne memulai dari yang paling jelas. Bila Anda tidak tahu bagaimana merepresentasikan properti Anda sebagai formula logika, maka TLA+ tidak bisa membantu. Metode formal lain pun sama. Ia memberi contoh yang gamblang: kalau Anda tidak bisa memformalkan pengertian manusia tentang burung, Anda tidak bisa membuktikan aplikasi Anda mengenali burung. Sayangnya, banyak properti penting yang kita pedulikan masuk ke kategori ini.

Kategori berikutnya adalah hal yang terlalu spesifik. Safety properties di TLA+ bekerja pada level state individual atau pada satu langkah tunggal. Anda tidak bisa mendefinisikan properti yang mencakup dua langkah atau lebih secara native. Contohnya, properti seperti "menekan delete lalu undo mengembalikan state semula", atau "setelah tombol power ditekan, komputer menyala dalam sepuluh langkah".

Selain itu, TLA+ juga tidak bisa mendefinisikan properti pada operasi floating point atau pada waktu nyata. Yang bisa dipakai hanyalah waktu logis, bukan waktu sungguhan. Untuk sistem yang punya tenggat berbasis jam dinding, keterbatasan ini penting untuk disadari sejak awal.

Keterbatasan yang Paling Menarik: Kuantifikasi atas Semua Behavior

Bagian yang paling Wayne soroti adalah soal kuantifikasi implisit. Properti TLA+ secara implisit dikuantifikasi atas semua behavior. Ketika dikatakan bahwa memeriksa []P berarti P benar di setiap state, makna sebenarnya adalah untuk semua behavior, []P benar pada state awal behavior tersebut. Artinya, properti apa pun yang bisa diperiksa TLA+ haruslah properti yang benar untuk setiap behavior individual.

Yang tersisa dari batasan itu ternyata jauh lebih banyak dari dugaan. Salah satu contohnya, kita tidak bisa menyatakan "ada behavior di mana P benar". Kita tidak bisa menyatakan bahwa P mungkin terjadi, meskipun kita tidak benar-benar mencapainya. Contoh konkretnya adalah membuktikan bahwa sebuah game bisa dimenangkan. Wayne menyebutnya reachability properties. Versi yang lebih maju termasuk "P bisa dicapai dari setiap state awal" atau "P bisa dicapai dari state mana pun di mana Q benar".

Kita juga tidak bisa mendefinisikan properti atas sekumpulan behavior. Ini disebut hyperproperty. Wayne memberi contoh pemodelan perangkat keras ponsel, di mana tujuannya adalah memverifikasi bahwa mode hemat energi selalu memakai daya lebih sedikit daripada mode normal. Untuk membantah properti itu, Anda perlu menunjukkan dua behavior yang identik kecuali satu dimulai dalam mode hemat energi dan satu tidak, dan mode normal ternyata memakai daya lebih sedikit. Satu behavior saja tidak cukup, sehingga properti ini tidak bisa diperiksa secara natural di TLA+.

Menurut Wayne, hyperproperty mungkin terdengar niche, tetapi ia mencakup banyak properti keamanan dan semua properti statistik, misalnya pernyataan bahwa persentil 95 dari waktu respons adalah 5 milidetik. Bagi tim yang mengurus SLA, poin ini layak dicatat.

Terakhir, ada keterbatasan yang Wayne sebut lebih akademis, yaitu tidak bisa mendefinisikan properti atas ruang state secara keseluruhan. Kita tidak bisa menyatakan, misalnya, bahwa hanya ada satu jalur dari state X ke state Y. Ia mengaku belum tahu seberapa berguna ini dalam praktik, tetapi menurutnya metaproperti semacam ini punya potensi untuk bermakna.

Akrobat: Cara Meniru Properti yang Tidak Didukung

Wayne mengakui bahwa pernyataan "TLA+ tidak bisa" agak terlalu disederhanakan. Yang ia maksud adalah bila Anda menulis spec yang langsung berkorespondensi dengan sistem yang ingin dibangun, maka TLA+ tidak bisa menyatakan properti-properti tadi sebagai properti sistem Anda. Tetapi ada cara menirunya.

Properti dua langkah bisa ditiru dengan auxiliary variables, misalnya menyimpan semua perubahan state ke dalam sebuah urutan riwayat state, lalu mendefinisikan propertinya sebagai invariant atas urutan tersebut. Sebagian hyperproperty bisa ditiru dengan self-composition, di mana setiap behavior dari spec yang dikomposisikan sendiri sebenarnya adalah dua behavior dari sistem aslinya.

Model checker utama TLA+, yaitu TLC, bisa memeriksa properti reachability paling dasar dengan kata kunci REACHABLE yang baru, serta sebagian properti ruang state dengan TLCGet. Wayne juga menyebut Andrew Helwer punya tulisan menarik soal meniru "always reachable" memakai fairness dan machine closure.

Namun ia menegaskan, semua ini hanyalah akrobat. Masing-masing menuntut kecerdikan untuk dirancang dan membawa kelemahan serius. Auxiliary variables merusak refinement, self-composition melipatgandakan ruang state secara eksponensial. Akrobat semacam ini tidak terkomposisi dengan baik bersama fitur TLA+ lainnya dan tidak mencakup semua seluk-beluk properti yang ingin dinyatakan. Yang paling buruk, menurut Wayne, model Anda jadi terlihat aneh dan berantakan, serta tidak lagi berkorespondensi dengan sistem sebenarnya.

Ada juga pilihan memakai alat lain dengan fokus berbeda. CTL bisa menangani properti reachability, PRISM menangani properti probabilistik. Trade-off-nya, masing-masing lebih lemah pada hal-hal yang justru dikuasai TLA+, dan tentu saja tidak ada yang bisa menangani properti yang memang tidak bisa dinyatakan secara logis.

Kesimpulan dan Sikap yang Wajar

Wayne menutup dengan penilaian yang seimbang. Menurutnya, TLA+ cukup baik untuk memetik banyak buah yang tergantung rendah. Invariant dan liveness mencakup banyak hal yang kita pedulikan, dan TLA+ cukup mahir menyatakan serta memeriksanya. Ia juga mengakui ada banyak potensi sekaligus banyak jebakan dalam memakai TLA+ untuk memeriksa kode hasil vibe coding.

Tetapi ada pula banyak hal yang bahkan tidak bisa dinyatakan, apalagi diperiksa. Itulah inti keberatannya terhadap narasi bahwa formal verification akan menyelesaikan masalah pengembangan perangkat lunak berbasis agen.

Bagi developer di Indonesia yang mulai melirik verifikasi formal, artikel ini berguna sebagai peta batas. TLA+ adalah alat yang kuat untuk sistem konkuren dengan properti keselamatan dan liveness yang bisa dinyatakan sebagai formula. Ia bukan obat mujarab untuk semua kelas bug, dan ia tidak bisa memverifikasi properti yang belum Anda formulasi dengan jelas.

Langkah praktis yang masuk akal adalah memulai dari properti yang paling penting dan paling mudah dinyatakan, biasanya invariant sederhana seperti "paling banyak satu pemimpin aktif" atau "saldo tidak pernah negatif". Dari sana, batas yang dijelaskan Wayne akan terasa sendiri, dan Anda bisa memutuskan kapan perlu berpindah alat atau kapan cukup mengandalkan pengujian biasa.

Sumber resmi: Hillel Wayne, "What TLA+ can and can't check", Computer Things, 30 September 2026. Wayne juga menulis artikel terkait berjudul "LLMs are bad at vibing specifications" dan "Three ways formally verified code can go wrong in practice".

Rekomendasi Tools & Layanan

Kalau lo mau langsung praktikkan panduan di atas, dua layanan yang gue pake sehari-hari: free trial Alibaba Cloud buat coba-coba tanpa biaya di awal, dan ECS instance 9th-gen kalau udah siap naik ke VPS production.