Apa yang Bisa dan Tidak Bisa Dicek TLA+
Judul asli: What TLA+ can and can't check
Mengapa Ini Penting
Batasan TLA+ relevan saat industri mulai mendorong AI untuk menulis kode sistem kritis.
Inventor Claude Code menyebut Opus bisa pakai TLA+ untuk temukan race condition, memicu euforia tentang formal verification—yang dinilai berlebihan oleh pendidik TLA+ Hillel Wayne.
Boris Cherny, pencipta Claude Code, minggu lalu menyebut bahwa model Opus mampu menggunakan TLA+ untuk mendeteksi race condition dalam kode. Pernyataan itu langsung memicu gelombang diskusi: banyak yang mengklaim formal methods akan menyelesaikan masalah pengembangan perangkat lunak berbasis agen secara permanen.
Hillel Wayne, pendidik dan advokat TLA+ sejak lama, angkat bicara mendinginkan ekspektasi. Ia menegaskan bahwa TLA+ memang andal untuk merancang sistem konkuren yang kompleks—namun ada batasan mendasar yang sering diabaikan: untuk memverifikasi sebuah properti, properti tersebut harus bisa diekspresikan terlebih dahulu.
TLA+ bekerja dengan membagi sistem ke dalam rangkaian state (perilaku). Sistem ini mampu memeriksa invariant (sesuatu yang buruk tidak pernah terjadi), action properties, serta liveness properties seperti "suatu kondisi akhirnya akan terpenuhi". Operator temporal seperti []P (selalu P), <>P (suatu saat P), dan P' (P di state berikutnya) menjadi fondasi ekspresi properti tersebut.
Namun Wayne menekankan: jika sebuah properti tidak bisa dirumuskan dalam logika TLA+, alat ini tidak bisa membantu sama sekali. Desain yang benar pun tidak otomatis menghasilkan kode yang benar.