Kotlean: Developing Verified Android Applications Using Lean
Kotlean enables developers to write Android app logic in Lean and verify code correctness.
1Verified 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.
2Architectural 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.
3Performance 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.
4Example 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.
5Technical 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.
6Formal 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.
7Integration 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.
8Open 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.