Rajath Mahendrappa Kotyal

Rajath Kotyal is a software engineer at Amazon who uses formal verification to check infrastructure templates, command-line instructions and specifications produced by language models. In the automated reasoning group at Amazon Web Services (AWS), he helped build Kiro’s requirements analysis, which can catch a conflict between two rules before a coding agent tries to implement them.

Rajath worked as a backend product developer at BMC Software from 2021 to 2023. He went on to earn a master’s degree in information technology with a focus on information security at Carnegie Mellon University in December 2024. That spring, he built LucidSearch, a search engine written in Go that retrieves passages from web pages and transcripts of podcasts and videos. It supplies those passages to a language model and returns references with the answer so readers can trace a claim to its source.

Rajath identified a limit to searching by similarity. A question about how someone slept last night might retrieve relevant reading about sleep, even when the answer depends on that person’s own records. He proposed using a graph to connect the question to the right records and identify the function that could fetch them.

Checking numeric conversions in Rust

During an AWS-sponsored practicum at Carnegie Mellon in fall 2024, Rajath worked with Yen-Yun Wu, Lanfei Ma and Junfeng Jin on the safety of numeric operations in Rust’s standard library. They wrote proof harnesses for Kani, an open-source Rust verifier, to check whether unsafe methods could trigger undefined behavior even when callers met their stated preconditions. Rajath also reviews contributions to the Rust standard library verification effort.

One failed proof exposed a mistake in the team’s own precondition for converting a floating-point number to an integer. They had checked whether the input fit in its original floating-point type. The conversion required it to fit in the destination integer type. Even a comparison with the largest allowed integer could admit an out-of-range value, because converting that limit to floating point could round it up. The team requested a check for the destination type’s range. Once they used it in their precondition, their float-to-integer conversion proofs passed.

Finding ambiguity in a coding specification

On Kiro, Rajath and his teammates worked with requirements written in everyday language. Their analyzer asks a language model to translate a requirement into logic several times. A solver checks the translations for logical equivalence, grouping those that permit the same behavior. When the groups differ, the analyzer can show the developer which choice the wording leaves open. In Rajath’s example, an instruction to remove a record could mean erasing it or hiding it from users while keeping the data. The solver can distinguish those outcomes. Rajath argues that the developer who knows the application should decide whether the record survives.