Ashley Chen

Security bugs and trapdoors in smart contracts have been impacting the Ethereum community since its inception. Conceptually, the 1.45-million Ethereum’s contracts form a single "gigantic program" whose behaviors are determined by the complex compositions of contracts. Can programmers be assured that this gigantic program conforms to high-level safety specifications, despite unforeseeable code-level intricacies? Static code verification cannot be faithful to this gigantic program due to its scale and high polymorphism. In this paper, we present a viable approach to achieve this goal. Our technology, called Theorem-Carrying Transactions (TCT), combines the benefits of concrete execution and symbolic proofs. Under the TCT protocol, every transaction carries a theorem that proves its adherence to the specified properties in the invoked contracts, and the runtime system checks the theorem before executing the transaction. Once a theorem is proven, it will be reused for future transactions, so TCT’s runtime overhead is minimal. As case studies, we demonstrate that TCT secures token contracts without foreseeing code-level intricacies, such as integer overflow and reentrancy. TCT is also successfully applied to a Uniswap codebase, showcasing a complex decentralized finance (DeFi) scenario. Our evaluation shows a negligible runtime overhead, two orders of magnitude lower than a state-of-the-art approach for runtime checking of contract code safety.

The emergence of large language models has enabled vibe coding, a natural language approach to programming in which users describe intent and AI generates or revises code, potentially broadening access to programming while preserving meaningful learning outcomes. We investigate its educational value through a month-long online hackathon that welcomed participants from multiple countries, ranging from complete beginners to experienced developers. The hackathon offered three tracks with increasing technical demands. Spark emphasized basic frontend functionality and dynamic features such as buttons, forms, and API calls. Build required backend or database integration. Launch targeted production ready web applications, including deployment. Participants were required to develop projects using only LLM generated code without manual edits and submitted complete chat histories, source code, demo videos, and functionality reports. We assessed educational effectiveness with a mixed methods design that combined standardized project evaluations across functionality, user interface and user experience design, impact, prompt quality, and code readability, along with post-hackathon surveys of perceived learning outcomes and thematic analysis of open-ended feedback. Our findings describe how participants with different backgrounds engage with vibe coding as task complexity increases, how the no manual editing constraint shapes prompting and debugging practices, and what these patterns imply for integrating AI assisted development into programming education and competitive learning environments.