Experience
3d Vision Engineer
Brütsch Technology Beringen, Switzerland Okt 2025 – present Deep learning, Python, Computer Vision
I work on an intraoral scanner (IOS) to scan teeth to get a 3d model. I am developping and improving deep learning models. Evaluate which problems might be solvable by deep learning and develop strategies how to realize this. I also improve coding guidelines.
PhD Student
Constructor Institute of Technology (Academia)
Schaffhausen, Switzerland
Dec 2023 – Sep 2025
Formal Verification, Eiffel, Automated Proofs (Isabelle HOL), LLMs, AI
- Mathematical Proof Engine: Developing an engine for validating mathematical proofs in an object-oriented programming language. Developed a first proof of concept for a simple proof.
- Formalization of Programming: Creating a formalization of programming, including many definitions and theorems, all separately verified in Isabelle HOL. (Link)
- AI for Formal Verification: Planning, executing, and analyzing a study on the effectiveness of LLMs in fixing bugs. (Link)
- Proof of Concepts: Developed CodeForge, a tool for compiling, executing, and verifying programs online without the need for local installation. Also developed AI-Proof, a tool using LLMs, Sledgehammer, and Isabelle HOL to automatically generate proofs. (Link)
- Teaching Assistant: Assisted in the courses Advances in Software Engineering and Software Construction, Architecture and Engineering. Responsibilities included teaching exercise sessions, writing and grading exams, and mentoring students.
Data Scientist
ti&m (Banking, Government, FinTech)
Zürich, Switzerland
Aug 2020 – Nov 2023
Machine Learning, Python, JavaScript, Docker, Data Science, AI, Computer Vision, Blockchain, Recommender Systems
- eID: Evaluated multiple SSI technologies for the Swiss electronic ID. Deployed them on a public cloud with blockchain technology. Constructed a frontend, backend, and mobile app. (Link)
- Fit&Proper: Extended an existing solution for automatically checking the background of people for the financial market supervisor using NLP and machine learning. (Link)
- Sustainability Assessment: Developed an MVP to help a team of sustainability experts find answers to their questions in their data, especially PDFs. The tool streamlines the process of extracting and analyzing information from large document collections. (Link)
- Construction Standard Management: Planned, developed, and deployed a solution for managing the most used construction standards in Switzerland (eBKP/NPK). This system improved efficiency and accessibility for industry professionals. (Link)
- Proof of Concepts: Built prototypes for a travel recommender system, as well as identity card and passport detection and parsing tools, showcasing the application of AI in diverse domains.
Software Engineer (Machine Learning, Computer Vision)
Kitris GmbH (Sports)
Zürich, Switzerland
Jan 2020 – Jul 2020
Python, Docker, R&D, Computer Vision, Visual Computing
- Video Tracking: Implemented a proof of concept for a video tracking system to analyze player movements and actions in sports videos. Utilized computer vision techniques to extract relevant features and provide actionable insights for coaches and analysts.
Junior Security Researcher & Software Engineer
Exeon Analytics (Cybersecurity)
Zürich, Switzerland
Apr 2018 – Jun 2019
Python, Docker, Scala, React
- Exeon Trace: Improved the main product by implementing a new feature for tracking and visualizing network traffic, enhancing the platform's security monitoring capabilities.
- Tridyo: Created an MVP for a new product analyzing the future viability of companies using sentiment analysis and fit and proper techniques. This project combined data science and software engineering to deliver actionable business intelligence.
Projects
Parallelismus
GitHub, Web Demo
Parallelismus is a web application for studying biblical parallelism in Hebrew and Greek texts. It allows users to navigate through biblical books, chapters, and verses, viewing words with their Strong's concordance numbers, original language texts, and translations. Users can create and manage semantic relationships between words (such as similar meaning, opposite meaning, subcategories, and composition). The tool uses IndexedDB for local storage and includes visualization features for exploring word relationships through interactive graphs. All data processing happens client-side, making it a fully functional static web application.
Background Generator
GitHub, Web Demo
Background Generator is a procedural art suite that creates stunning SVG backgrounds using TypeScript. It includes five distinct generators: gradient abstractions with blobs and ribbons, polygalaxy scenes with geometric shards and orbital systems, terrain landscapes with mountains and fog, urban skylines with parallax layers, and botanical gardens with leaves and vines. The tool offers both a web playground for real-time experimentation and CLI tools for batch rendering. All generators support customizable themes, seeded randomization for reproducibility, and optional PNG export.
Python Blocks
GitHub, Web Demo
Python Blocks is a block-based Python editor built with Vue 3 and Pinia. It lets users assemble Python programs from visual blocks, inspect the generated Python live, import Python back into the canvas, and run the result directly in the browser with PyScript.
Buchfaltstudio
GitHub, Web Demo
Buchfaltstudio is a book folding pattern generator that creates precision folding instructions for book art (Orimoto). Users can either enter text (which is automatically rendered using Google Fonts) or upload images (SVG, PNG, JPEG, GIF, WebP). The tool analyzes the artwork, scales it to physical book dimensions, detects dark regions, and generates detailed PDF instructions with millimeter-precise fold positions. Features include automatic book preview rendering, customizable page count and book height, and fully client-side processing for instant results.
Hoare Logic Proof Verifier
GitHub, Web Demo
This is a web technology based hoare logic verifier. The user can create programs and their proofs using drag and drop. The proofs of the hoare logic have to be explicit to the end. The logical and arithmetical proof obligations are fed to the SMT solver Z3. The tool is fully frontend based. No server is needed. That is why the application also works on this static website.
CodeForge
CodeForge on GitHub
CodeForge is a platform designed to compile, run, and verify code across multiple programming languages. Using Docker containers to ensure that code execution is both secure. The platform is useful for educational environments, coding demos. Its containerized architecture allows for easy integration of new languages and verification tools. It was completely vibe coded. It is sometimes online at eiffel.org.
PDF Scan
PDF Scan Automation on GitHub
PDF Scan is a project that streamlines the organization of physical mail and documents. It processes batches of scanned documents, automatically detecting where to split them into individual files, straightening pages, and performing OCR to extract text. This tool reduces manual effort in digitizing and archiving paperwork. It is especially helpful for personal and small office use. It was partially vibe coded.
Autoproof Docker
Autoproof Docker on GitHub
This project provides a Docker image for running AutoProof, a static verifier for Eiffel programs. By containerizing AutoProof, the setup process becomes straightforward and platform-independent. Users can quickly verify Eiffel programs without worrying about complex dependencies. The Docker image is ideal for researchers and educators working with formal verification.
Evolution Showcase
Evolution Showcase on GitHub
Evolution Showcase is a small Python game that visually demonstrates the principles of evolution and natural selection. In the game, agents exhibit random behaviors, but over time, those best suited to the environment are selected, resulting in non-random strategies. The project serves as an educational tool for illustrating evolutionary algorithms and emergent behavior.
OpenSCAD Phone Stand
OpenSCAD Phone Stand on GitHub
This project features a customizable 3D model of a phone stand, created using OpenSCAD. The design is fully parameterized, allowing users to adjust dimensions to fit any mobile phone model. It is ideal for 3D printing enthusiasts.
This website
This website on GitHub This website was done using mkdocs with a custom template and styling. It is automatically deployed to retoweber.info.
Publications
Do AI models help produce verified bug fixes?
ICSE 2026. (published)
Authors: Reto Weber, Li Huang, Bertrand Meyer, Ilgiz Mustafin, Marco Piccioni, Alessandro Schena
PRISM: Programming Really Is Simple Mathematics
YuriFest 2025. (accepted – to be published)
Authors: Reto Weber, Bertrand Meyer
Loop unrolling: formal definition and application to testing
ICTSS 2025. (published)
Authors: Reto Weber, Li Huang, Bertrand Meyer
Conferences
Programming Really Is Simple Mathematics
YuriFest 2025, Ludwig Maximilian University of Munich, Munich, Germany
Program verification using AutoProof
AVM 2024, University of Freiburg, Freiburg, Germany
Education
Constructor Institute of Technology
Doctor of Philosophy (PhD), Computer Science (2023 – now)
Thesis: Programming really is simple Mathematics and vice versa
Focus: Static verification of object oriented programming languages for example Eiffel. I formalized programming mathematically and embed mathematics into Eiffel. Which tries to narrow the gap between programming and mathematics.
ETH Zurich
Master of Science (MSc), Computer Science (2017 – 2020)
Master Thesis: Inaudible Audio Adversarial Perturbations via Psychoacoustic Clipping
Lecutres taken: Machine Learning, Web Engineering, Deep Learning, Probabilistic Artificial Intelligence, Advanced Topics in Machine Learning, Einführung in die Quanteninformatik, Models of Computation, Principles of Distributed Computing, Algorithms Lab, Computational Intelligence Lab, Introduction to Social Networks: Theory, Methods and Applications
Bachelor of Science (BSc), Computer Science (2013 – 2017)
Bachelor Thesis: Solving Constraint-Satisfaction Problems with Spike-Based Neural Attractor Winner-Take-All under Oscillatory Inhibition
Lecutres taken: Analysis I, Analysis II, Einführung in die Programmierung, Datenstrukturen & Algorithmen, Parallele Programmierung, Lineare Algebra, Diskrete Mathematik, Physik, Digitaltechnik, Data Modelling and Databases, Formal Methods and Functional Programming, Operating Systems and Networks, Systems Programming and Computer Architecture, Tehoretische Informatik, Wahrscheinlichkeit und Statistik, Learning and Intelligent Systems, Algorithms, Probability, and Computing, Information Security, Visual Computing, Software Architecture and Engineering, Angewandte Computer Architektur, Embedded Systems, Introduction to Neuroinformatics, Wie funktioniert Froschung? Algorithmen und Kombinatorik, Einführung in die Spieltheorie, Introduction to Cognitive Neuroscience
