# Kotlean: Developing Verified Android Applications Using Lean Kotlean enables developers to write Android app logic in Lean and verify code correctness. - **Source:** [Hacker News: Show HN](https://news.ycombinator.com) - **Published:** 2026-11-11 - **Topic:** [technology](https://brifing.si/c/technology) - **Original article:** - **On Brifing:** https://brifing.si/s/e28a4502-06e2-44cc-aaa6-25818ec2b5df ## Verified Android Development Kotlean allows developers to write Android application state, behavior, and UI components directly in the Lean programming language. By leveraging Lean's formal verification capabilities, developers can prove properties of their code before compilation. A lightweight Kotlin host manages native Android Views and handles platform-specific effects within the application lifecycle. ## Architectural Design Patterns The framework utilizes an Elm-style model-update-view loop, ensuring a strict separation between application logic and platform effects. Lean functions compute view patches and subscription changes, which are then transmitted across a fixed byte protocol via JNI. This architecture keeps app-specific models and messages isolated within the Lean environment. ## Performance and Execution Kotlean runs Lean on the Android main thread, requiring updates and drawing to remain within the device's frame budget. Performance testing on a Pixel 11 Pro demonstrated stable 60.05 FPS during gameplay. Native JNI increment steps showed a median latency of 39.25 microseconds, indicating efficient communication between the host and Lean. ## Example Applications Provided The repository includes two primary examples: a Counter app and SnackNet, a maze-chase game. SnackNet demonstrates complex features like continuous motion, buffered turns, and multitouch input. These examples serve as templates for implementing stateful apps with timers, persistence, and lifecycle subscriptions, all while maintaining the core Lean-based logic structure. ## Technical Build Requirements Development requires a Linux x86-64 environment with specific versions of Lean 4.34.0, JDK 21, and Gradle 9.9. The build process involves configuring the Android NDK and CMake to compile the Lean runtime for arm64 targets. Developers must manage dependencies like libuv and the Lean source code to generate native libraries. ## Formal Verification Scope Kotlean includes formal proofs for wire codecs, canonical UI compilation, and scene diff correctness. App authors can extend these by proving specific update properties, such as SnackNet's token collection logic. These proofs ensure that the application's state machine remains connected and consistent throughout the user's interaction with the Android interface. ## Integration and Constraints Apps require Android 16 or later, with API 36+ support on arm64 devices. Because Android shares the process's Binder transaction buffer, developers are advised to keep saved-instance data small. The system uses named plugins with byte payloads to handle Android integrations, ensuring that platform I/O remains decoupled from the verified logic. ## Open Source Licensing Kotlean is released under the MIT license, while the underlying Lean runtime retains its Apache 2.0 license. This project represents a significant step in bringing formal methods to mobile development. By bridging Lean and Android, it provides a pathway for building high-assurance applications where the code proven is the code executed. ## Sources covering this story - https://github.com/kbr-/kotlean — --- _Summary written by Brifing from the original reporting. Copyright in the original article belongs to its publisher; read the full piece at the link above._